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!

  • $\begingroup$ "while in SOL it can range over predicates too" is correct. $\endgroup$ – Jean Marie Oct 22 '17 at 6:46
  • $\begingroup$ @JeanMarie That makes my latter question all the more so, why is it that the second sentence is ranging over predicates but the former is not? $\endgroup$ – Zelos Malum Oct 22 '17 at 6:48
  • $\begingroup$ $∀x∀y∃z(x∈z ∧ y∈z)$ is a formula in FOL set theory. And also $∀P∀x(x∈P ∨ x∉P)$ is. A correct SOL formula will be $∀P∀x(Px ∨ \lnot Px)$ $\endgroup$ – Mauro ALLEGRANZA Oct 22 '17 at 8:17
  • $\begingroup$ In SOL we quantify predicate symbols (i.e. "properties and relations"). In FOL we quantify only individual variables (i.e. "objects"). In FOL set theory, sets are objects, i.e. represented by individual variables and constans. $\endgroup$ – Mauro ALLEGRANZA Oct 22 '17 at 8:18
  • $\begingroup$ See Second-order and Higher-order Logic. $\endgroup$ – Mauro ALLEGRANZA Oct 22 '17 at 8:20

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.

  • $\begingroup$ Your rendition makes it very clear it is second order. So just so I get it straight, in ZFC axioms $\in\subseteq D\times D$ but in the example it would be $\in\subseteq D\times PD$, just that they use both t once as from context, the exact meaning can be salvaged? $\endgroup$ – Zelos Malum Oct 22 '17 at 7:02
  • $\begingroup$ With respect to the first part of your second sentence, yes except $\in$ in the SOL example would not be just some relation symbol like $\in$ is in ZF(C), but part of the syntax of the logic itself like the logical connectives. I'm not saying $\in$ has that sort in that particular example, but that it would be that way in every second-order theory using that notation. This means $D$ is free to be interpreted as anything, e.g $\mathbb{N}$ while the interpretation of the domain for ZF(C) is a model of set theory. The meaning of $\in$ for ZF(C) comes from the axioms, not from the notion of model. $\endgroup$ – Derek Elkins Oct 22 '17 at 7:51
  • $\begingroup$ I don't understand the latter part of your sentence beginning "just that..." $\endgroup$ – Derek Elkins Oct 22 '17 at 7:51
  • $\begingroup$ What I meant with "just that" was that it is in a way "abuse of notation", using the same thing for vastely different concepts in mathematics in a formalized way, but out of linguistic and psychological needs it is ignored for general ease of reading. So $\in$ in both cases are very different relations/predicates, but because they are usually conceptually very close in peoples minds, the two things are symbolized identicly. $\endgroup$ – Zelos Malum Oct 22 '17 at 8:12
  • $\begingroup$ In this case, I think the motivation for using $\in$ in SOL is related to the standard semantics where predicates will be modeled by subsets (or, equivalently, characteristic functions which is more in-line with the logical notation). Relatedly, set theory is essentially an implementation of higher-order logic, so if we were working within set theory we would model those those predicates as subsets (which, of course, is exactly what the standard semantics of SOL is doing). Personally, I think an extremely clear separation between logic and set theory should be maintained. $\endgroup$ – Derek Elkins Oct 22 '17 at 8:47

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.

  • $\begingroup$ But what does "subset of the universe" even mean when we remove set theory? $\endgroup$ – Zelos Malum Oct 22 '17 at 7:07
  • $\begingroup$ I understand that the first statement is FOL, it makes perfect sense to me, but with the understanding of second order being quantifiers over predicates I lose how the latter statement is second order but the first one is not. There is something in the translation there that eludes me. $\endgroup$ – Zelos Malum Oct 22 '17 at 7:12
  • $\begingroup$ @ZelosMalum Why would we remove set theory? We always have this set theoretical foundation when speaking of mathematics, like functional analysis, topology, differential geometry and finally - logic. And within set theory we can speak of predicates & first order or second order formulas, define what it means that a formula is satisfied in a model, etc. Sometimes we happen to study set theory itself. But studying some other theory, like the theory of partial orders or some second order theory, only makes us remove the set theory as the object of study, but not as the tool with which we study. $\endgroup$ – Adayah Oct 22 '17 at 8:04
  • $\begingroup$ If you're a bit into computer science, let me make an analogy. Compilers can process every correct source code in a particular programming language. When the compiler itself is written in that programming language, the compiler can even compile it's own source code. But while it's compiling something else, it doesn't mean the compiler isn't there: it's just not the source of it being compiled. P.S. Please let me know if I completely missed the point you were making. :p $\endgroup$ – Adayah Oct 22 '17 at 8:07
  • $\begingroup$ Yeah that analogy went way past my head.As for removing set theory, if set theory is founded in first order logic, then using set theory to describe first order logic makes it circular. I m interested in logic here as foundation, before set theory has even been constructed with the axioms. $\endgroup$ – Zelos Malum Oct 22 '17 at 8:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.