Let's consider a logical system where all predicates can take only one argument: $A(x), B(x), \cdots$. Let us also assume that we can use all available logical (boolean) operators to combine those "atomic" predicates and, in this way, construct new predicates. For example:
$F(x) := [A(x) \wedge B(x)] \lor [\lnot C(x)]$
Finally, in each formula, we will have unbound variable $x$ and we can bind it by $\forall$ and $\exists$ quantifiers. For example:
$\forall x : [[A(x) \wedge B(x)] \lor [\lnot C(x)]]$
or
$\exists x : [\lnot A(x) \lor B(x)]$
So, one can say that this system is somewhat between proposition logic and predicate logic. Or, more precisely, it is a reduced version of predicate logic since any formula in this system is a valid formula of predicate logic.
So, my question is: What are the "transformation rules" for this system apart from boolean formulas for logical operations. For example, I can think of those rules:
$\lnot \forall x : [C(x)] = \exists x : [\lnot C(x)]$
$\lnot \exists x : [C(x)] = \forall x : [\lnot C(x)]$
$\forall x : [A(x) \wedge B(x)] = \forall x : [A(x)] \wedge \forall [B(x)]$
By the way, can it be that the described logical system has a special name?
Best Answer
This is called monadic predicate calculus or monadic first-order logic. See this article on deductive systems for first-order logic for the transformation rules that apply to predicate calculus in general and to monadic predicate calculus in particular. However, monadic predicate calculus is particularly simple: an interpretation for a sentence involving $n$ monadic predicate symbols $A_1, \ldots A_n$ is essentially just a set $X$ with $n$ chosen subsets $X_1, \ldots, X_n$, where $x \in X_i$ iff $A_i(x)$ holds. Monadic predicate calculus can be shown to be decidable: a sentence involving $m$ monadic predicate symbols is valid iff it holds under every interpretation in a set $X$ with $2^n$ elements (and it is a finite process to enumerate and check all such interpretations).