Why are we using first-order logic and how to fix PA?

Question

First-order logic (FOL) is pretty bad at pinning down specific structures for which we have no problem to think about intuitively. The classical example for me is $\Bbb N$, for which the first-order theory PA failes to pin down the standard natural numbers $\mathcal N$.

That this is impossible for most sufficiently useful structures is a classical result of Gödel $-$ his incompleteness theorem. As for me, the mathematical language is a way to formalize my thinking, it is natural to ask if there is anything better than FOL. Seemingly FOL cannot express everything I can think about in a unique way.

Of course, FOL has nice syntactic properties that we want to keep in one or another way. One than usually hears about Lindström's theorem, which states that one cannot extend on FOL without loosing some seemingly importand and wantable results $-$ namely, the compactness theorem and the Löwenheim-Skolem theorem.

This is for me a quite strange statment. What exactly is so desirable about these theorems that we prefer them so badly, that we give up on the chance of a more powerful way to express our thinking. Even worse, it seems that these results even lessen the expressability of our language:

• The compactness theorem prevents us from describing exclusively finite structures.
• The Löwenheim-Skolem theorem prevents us from fixing the cardinality of an infinite structure we want to describe.

Actually I have some specific extension in mind $-$ $L_{\omega_1\omega}$. If I have not misunderstood this notation, this is a logic allowing for countable infinite disjunction and conjunction. As far as I understand, the non-standard models of PA contain "numbers" bigger than $S\cdots S0$ for any finite number of occurences of the succesor function $S$. So couldn't this be fixed by adding the axiom

$$x=0\;\vee\; x=S0\;\vee\; x=SS0\;\vee\; x=SSS0 \;\vee\; \cdots $$

This is a computable infinite disjunction. I have no problem accepting it, as axiom schemas are also just infinite conjunctions in disguise (aren't they).

So, there are two question contained above, let's collect them:

Tl;dr

• What exactly is so desirable about compactness and Löwenheim-Skolem that we do not want to extend FOL?
• Does this infinite disjunction axiom give me anything, or is it just introducing new problems (the logic is not complete, still not excluding all non-standard models, ...)?

Answer 1

The boundaries of our ability to "fix" things are set by Gödel's incompleteness theorem. Contrary to what you seem to be assuming, this theorem is not really specific to first-order logic -- it tells us that no reasonable proof system where one can computably distinguish valid proofs from invalid ones, can possibly prove all (first-order) truths about the natural numbers without also proving some untruths.

This means that neither moving to higher-order logic nor allowing some limited infinitary constructions can get us out of the situation that there will always be true statements about the integers that any given system cannot prove.

Rather than futilely trying to push the boundaries of our system towards proving more and more truths for its own sake, our aim is therefore to understand what the limits of provability in particular systems are.

For that purpose, first-order logic has very convenient properties. The real jewel here is not in itself compactness or Löwenheim-Skolem, but Gödel's completeness theorem, which tells us that every consistent theory has a model. Or, in a perspective more relevant here: for each formula that cannot be proved, there's a model where that formula is false.

This makes models available as a very powerful tool for thinking about unprovability -- in contrast to the situation for higher-order logic, where there are both logical consequences of the axioms we can prove, and logical consequences of the axioms we cannot prove, but no useful semantic way of thinking about the difference between those two classes.

So the existence of non-standard models in first-order logic is a feature rather than a bug. Those non-standard models are useful as objects that certify the non-provability of some true claims about the integers.

---

For your second question: An axiom schema could be seen an infinite conjunction, in contrast to your infinite disjunction.

It is simple enough to conclude something from an "infinite conjunction" -- namely, each of the conjuncts is a consequence -- but it's unclear how one can actually conclude anything useful from the infinite disjunction, at least as part of a proof of finite length.

You might object that since the parts of your infinite disjunction are generated by a uniform, computable, rule, so we could use it by supplying a similarly uniform rule that generates proofs for each of an infinity of premises. But in practice, most of the cases where there is such a uniform proof generator (that we can convince ourselves will always work) can already be handled by first-order induction in PA. And the ones that can't can be formalized in ZFC anyway, so instead of extending PA with new forms of logic we might as well say that we're going to prove things about the integers in first-order ZFC instead -- which is indeed what everyday mathematics does!