What is the difference between first order logic on a power set, and second order logic on the base set?

Question

The question title doesn't fully capture my question, so I will clarify:

Assume we have the structure of natural numbers: $$(\mathbb N, +,0,1)$$

We know from theorems in mathematical logic, that we cannot use first order predicate logic to fully characterize this structure with a set of axioms. Yet second order logic is incomplete (not all true statements can be proven).

As far as I understand it, in axiomatic set theory we use first order logic, which is complete, but we quantify over a domain that contains both sets and urelements, thereby allowing us to state things in first order logic that would normally require second order logic (I am not saying that this is the purpose of axiomatic set-theory, but merely that it is true).

But to simplify, we don't need to study the domain of all mathematical objects as set theory does. We can also formulate the structure:

$$(\mathbb N,\mathcal P(\mathbb N), +,0,1,\in)$$

and then use first order logic on this structure. I assume that the standard proof calculus for this is complete, as it has been shown to be complete for first order logic?

If so, then my question is:

What is the difference between $$ \begin{align} \text{applying second-order logic to } \quad &(\mathbb N, +,0,1) &\quad \text{ and}\\ \text{applying first-order logic to } \quad &(\mathbb N,\mathcal P(\mathbb N), +,0,1,\in)& \end{align} $$

• Is there a difference?
• How do we make sense of first-order-logic-completeness, and second-order-logic-incompleteness, if there is no difference?

Answer 1

This question is predicated on a misunderstanding of the meaning of completeness. That first-order logic is complete means that given a set of axioms, every sentence that is true in every model of those axioms has a proof (in each of the usual proof systems for first-order logic).

Your question has only a single particular model and no specification of any axioms at all, so completeness does not bear on it.

But there's more: That first-order logic is complete does not mean that a particular first-order theory is also complete. Completeness means something different for theories than for logics: A complete theory is one that is strong enough to either prove or disprove every sentence in its language.

It is perfectly possible to have such a theory in a complete logic. For example, take the first-order theory of groups: it neither proves or disproves $\forall a\forall b(ab=ba)$, so it is incomplete. This does not contradict the logic being complete, because neither $\forall a\forall b(ab=ba)$ not its negation is true in all models: there exist both abelian as well as non-abelian groups.

It is possible to write down a two-sorted first-order theory in the language $\{0,1,{+},{\cdot},\in\}$ whose theorems are the same as the ones second-order arithmetic proves. This theory will be an incomplete theory, meaning that it has models that are essentially different from $(\mathbb N,\mathcal P(\mathbb N))$.

---

Finally, note that your particular structure $(\mathbb N,+,0,1)$ can be completely (and effectively) axiomatized in first-order logic: Presburger arithmetic does that. The famous essential incompleteness of theories of the natural numbers only arises if you want a theory that speaks about both addition and multiplication.

Answer 2

There is an entire family of theories of "second order arithmetic" that are explicitly intended to study the structure $(\mathbb{N}, P(\mathbb{N}), +, \times, 0, 1, =, \in)$. Second-order arithmetic was first studied by Weyl, later by Feferman, and developed into a field known as "reverse mathematics". It uses multisorted, first-order theories of arithmetic that have a sort of the naturals and a sort for sets of naturals.

These theories of second-order arithmetic are exactly what we would mean by "using first-order logic to study the structure" - we choose axiom systems that are true in the structure, and use these systems to prove things.

One reason there is a hierarchy of these axiom system is that the set of true sentences of that model is extremely complicated. No computable set of axioms that are true in the model is able to prove every true sentence in the model. Standard results in logic show that in fact no second-order formula (quantifying over $\mathbb{N}$ and its powerset) can define the set of sentences that are true in that model. But we want to look at axiom systems where we can tell whether a given statement is an axiom. So each of these axiom systems only gives us an approximation to the set of true formulas of the intended model.

The other issue with the structure above is that the set of true formulas in it is not even determined by ZFC set theory, in the sense that there are formulas in the language of second-order arithmetic that are neither provable nor disprovable in ZFC. One example is "$V \cap P(\mathbb{N}) = L \cap P(\mathbb{N})$", an analogue of the axiom of constructibility $V = L$. It is not obvious that the quoted formula is expressible in the language of second-order arithmetic, but it is expressible using techniques standard in the area. So the phenomenon on independence results in set theory already appears in second-order arithmetic, so when we start to look at very strong axiom systems for second-order arithmetic, our work becomes closely related to set theory, particularly descriptive set theory.