Differentiating First/Second order logic

Question

I am trying to get a grasp about the mechanicly difference between First order logic (FOL) and Second order logic (SOL). From my understanding objects within them can be divided into these parts

• Constants
• Variables
• Predicates
• Functions

At which formula/terms are constructed recursively. My understanding is that FOL allows the quantifiers, $\exists,\forall$, can range over variables, while in SOL it can range over predicates too, is that correct? I don't want to understand it as "ranging over sets" because that is when we go for a set theoretical intepretation of it but I want to understand it mechanicly.

Onto set theory though as it baffles me.

Two simple sentences $$\forall x\forall y\exists z(x\in z\land y\in z)$$ $$\forall P\forall x(x\in P\lor x\notin P)$$

The former is a FOL statement, the latter a SOL statement. The first is axiom of pairing in ZFC and the latter is an example from wikipedia. If my previous understanding is correct, then how is the latter SOL but not the former, or vice versa? They both talk about objects being in sets that they range over and in ZFC all objects are sets.

A hypothesis I had for it is that the predicate $\in$ is usually seen as binary but you can technically have it as an unary by having it be $\in P$ instead, at which it would range over a form of predicate to be SOL, but then we get the same intepritation for the former as well.

I have tried rewriting it as

$$\forall x\forall y\exists z(P(x,z) \land P(y,z))$$ $$\forall z\forall x(P(x,z)\lor \neg P(x,z))$$

to get rid of the set theoretical view of it, and quite frankly it only makes them look even more the same.

Any clearification on this would be most appriciated!

Answer 1

Quantifiers don't "range over variables", they range over individuals of the domain. (In a standard set-theoretic semantics, these will be elements of the domain class.) Variables refer to those individuals in formulas. In Second-order Logic, variables can additionally refer to predicates. (In a standard set-theoretic semantics, these will be subsets of the domain class or more generally $n$-ary relations on the domain class.) It may be clearer to separate quantification ranging over individuals from quantification ranging over predicates, and similarly separate variables that refer to individuals from variables that refer to predicates, but this is often left implicit since it is clear whether a variable refers to an individual or a predicate depending on how its used (and it's disallowed to use it in an inconsistent manner).

For a variety of reasons, I don't recommend using set-theoretic notation for second-order logic formulas. I would write your SOL example as: $$\forall P.\forall x.P(x)\lor\neg P(x)$$ This unambiguously places this formula in (at least) second-order logic as first-order logic does not allow variables as names of predicates. ZF(C), on the other hand, is a theory of first-order logic and your original rendition of that formula is indeed a formula of (the first-order theory of) ZF(C).

If you want to use set-theoretic notation rather than logical notation for SOL, then $\in$ is now not an arbitrary relation between any terms. Instead, you can think of it as being "typed", something like ${\in} \subseteq D\times\mathcal{P}D$ where $D$ is the sort of the domain and $\mathcal{P}D$ is the sort of predicates on the domain. This makes something like $P\in P$ and ill-formed formula (while in the first-order theory of ZF(C), it's a completely legitimate formula). Again, I don't recommend using this notation for SOL. The set-theoretic notation, besides being ambiguous, carries a lot of connotations that don't necessarily hold for SOL.

Answer 2

Let's forget the first statement for a while and consider another one:

$$\tag{1} (\forall x)(\forall y)(\exists z)(x \leqslant z \wedge y \leqslant z).$$

Here $x, y, z$ are variables that stand for elements of the universe and $\leqslant$ is a fixed binary relation, which we think of as some partial order. The above is a first order statement, since it only quantifies over first order variables $x, y, z$ - elements of the universe.

That statement also has some meaning for us - it states that every pair in the order has an upper bound. It is about some property of our partial order.

Now back to the original statement:

$$\tag{1'} (\forall x)(\forall y)(\exists z)(x \in z \wedge y \in z).$$

Here again $x, y, z$ are meant for elements of the universe and $\in$ is a binary relation, which we think of as set membership. It is also in the first order logic for the exact same reason as in $(1)$.

I assume there is no problem with understanding why $(1)$ is in first order. The confusion may arise in $(1')$ because of our understanding of the relation $\in$ in ZFC as a membership relation, which implies that we think of $z$ as a set containing elements $x, y$. But formally it's not so; $\in$ is just a binary relation, satisfying some axioms which we would expect from a membership relation. To summarize: the membership quality of $\in$ is a meaning we attach to the relation, which is not reflected in any way in the underlying formalism.

As to your second statement, I would write it differently:

$$(\forall P)(\forall x)( P(x) \vee \neg P(x) ).$$

Here $P$ stand for a subset of the universe and $x$ is an element of the universe. Now the notion of membership is embedded into the logic: $P(x)$ formally means "element $x$ belongs to the set $P$". Since the subset $P$ is quantified over, the statement is in second order logic.