Why we cannot coin a logical system without this dicotomy of predicate and terms, that is to say a single sorted logic. So we only have term symbols that at the same time act as predicate symbols. So upper and lower cases resepsent the same sort. So can we have the following high order logic based on simulating set theory.
So the logical rules would be:
variable symbol $x,y,z, ,...$ all are terms of the language
constants $a,b,c,....$ all are terms of the language
Formula formation rules:
- If $x,y$ are terms of the language then $x(y)$ is a formula.
- closure of formulation under logical connectives and quantification as usual
substitution and distribution rules as usual for first and high order logic
For convinience we'll write all cases of a variable in a formula to mean the same variable in a formula under the respective quantifier, so for example $\exists xyz (Xy \land Yz)$ here $X$ is the same variable as $x$, and the same applies to $Y$. A variable is written in lower case when its in object role (being predicated upon), while its written in upper case when its in predicate role. However this is just a convinience.
also the inference rules are the same as that of first order logic.
Definitional symbols can be added as usual but only definable after unary predicates.
Add all rules of propositional logic.
The only thing that is different is the comprehension axioms, here we replace the ones in high order logic by the following ones which would be MK like ones for example:
We start with existence of predicates that are held by some predicates:
$\exists P \exists x: Px$
Now a we'll use the notation $x^*$ to signify that $x$ is held by some predicate.
Now we add our modified comprehension axioms simulating MK class comprehension scheme.
$(\exists P \forall x^* [Px^* \iff \phi(x^*)])$ is an axiom, for any formula $\phi$ in which $P$ is not free.
Then we write foundation in terms of absence of infinite descending predication that is:
$\forall x \neg \exists P (Px \land \forall y (Py \to \exists z(Pz \land Yz)))$
What is called as a transitive closure of a set, we'll call it a HISTORY of a predicate, denoted as $H$, so for any predicate $X$ we have $HX$ as a predicate also.
Then add the axiom
$(\forall Y^* \exists P^* \forall x(P^*x \iff \forall z (Xz \to HY^*z) \land \phi))$ for each formula $\phi$ in which $P^*$ is not free.
Then we add an axiom of infinity, that is there is a predicate with infinite output
$\exists P^* \forall x (P^*x \to \exists y (P^*y \land Yx))$
Also we add an axiom for replacement:
$\forall Y^* \exists P^* \forall x (Y^*x \to P^*f(x))$
where $f$ is a definable function not using $Y^*$.
We can add choice axioms as well.
This way we get a theory like MK but in a logical dress! So there is no dicotomy between a theory and its underlying logic. Its all in one parcel. We can label such logic as: Mono-sorted strictly monadic high order logic "MSSMHOL".
If that can work then this shows that classes can be thought of high order unary predicates and even logic can be reformulated to be only of those predicates. It certainly looks more of a logical game. But afterall mathematics itself looks like a logical game.