In the lecture last week, in the chapter about logics, we touched upon proof systems. We mentioned them also in connection with first-order logics, without actually presenting such a system.
In that discussion, I asked the question
Do there exist sound and complete proof-systems for first-order logics? Does anyone know?
Most or even all hands went up in favor of the pessimistic view ``nope, no such thing,’’ where my answer was, that such system exist.
Indeed, for validity there exist different formulations of sound and complete systems, like Hilbert-style or natural deduction, styles we shortly mentioned in the lecture, and there are more.
The existance of such systems does not mean that proving first-order formulas as valid is a solved problem in that one has a method to figure out whether a formula is valid or not. If the formula is valid, the proof system, being complete, can derive that. It may take quite some time, even longer that one cares to wait, but still. The system will find a proof when presented with a valid formula.
It’s only that one cannot decide whether formulas are valid or else not. For formulas, that happen to be invalid, there exists no proof, of course, thanks to correctness (aka soundness). But to establish that is a process that may not terminate; the proof search to see whether one can derive the formula valid just goes on and on, without terminating with a definite negative answer.
There is nothing one can do about it; it’s known that first-order logic is undecidable. So the situation concerning proof systems for first-order logic is: correctnes
yes, completeness, yes, decidability: no.
The fact that there is no decision procedure should not be seen as a weakness or defect of first-order logic and first order logic validity. If there’s something not right with the logics, it’s something else. We come to that later.
But what about incompletenes in connection with first-order logics? Why does one vaguely remember that this-and-that logic theory involving first-order terms and quantifiers has no complete proof system?
Well, indeed, there is some famous result(s) there. Let’s first remind us what is meant by a ``theory’’. A theory in our context is a set of formulas, typically an infinite one. So a first-order theory is a set of first-order formulas. Often one adds additional conditions on it, like if one has a set of formulas and the set contains A and B as formulas, it’s necessary that it also contains the conjunction A and B. Let’s ignore such closure conditions for the discussion here.
As far as theories goes, one can distinguish between syntactical theories and semantical ones. Syntactical ones refer to a proof system, and it’s the set of all formulas that can be derived starting from the axioms using the given proof rules. A semantical theory or model-theoretic theory is the set of formulas that are true in a given model or set of models.
For instance, assume one is interested in the natural numbers and operations and functions on those, so one has fixed on some first-order signature supporting standard functions (addition, multiplication, or maybe some less standard ones) and some relations. Then the first-order theory of the natural numbers (and the given signature) is the set of all the first-order formulas that happen to be true in the natural numbers.
Now, for this theory (and similar ones), there is no sound and complete first-order derivation system. This is a consequence of one of Gödel’s famous incompleteness theorems.
Of course one can take one first-order proof system and try to axiomatise ``the’’ natural numbers or some form of arithmetic: one writes down an appropriate set of axioms for the intended numbers, and with the given derivation rules, that gives a syntact first-order theory of numbers. That one is sound and complete for all models of that axiomatization of the numbers.
Isn’t that a contradiction? No, it just means that the axiomatization based on a first-order derivation system which has the natural numbers as one possible model and otherwise captures models that resemble the natural numbers. The models resemeble the usual natural numbers because, after all, the axioms capture crucial properties that hold in the natural numbers.
And, completeness of the proof system means that all formulas that a true for all models of that axiomatization are derivable. Only that there are also models that depart from what is commonly understood as the natural numbers. One could call them un-natural numbers, but more common terminology would call them a non-standard model of arithmetic or of the natural numbers.
So, the first-order axiomatization has not just conventional standard natural numbers as model, but also un-natural models, and there are formulas in first-order syntax that hold for the natural numbers, but not for the un-natural ones, i.e., they are not valid for all models of the axiomatization, which includes the unatural as well as the un-natural ones.
How do un-natural numbers look like and what’s missing in the axiomatizion?
The fact that there are non-standard models of the first-order axiomatization means first-order logic is not strong enough to characterize the natural numbers, at least not the ones one is used to. That can be seen a a weakness of first-order logic.
Having mentioned un-natural numbers resp. non-standard models of first-order axiomatizations, perhaps we should also say, how those look like. That also sheds light on the second question of this paragraph, namely what is missing in the first-order axiomatization.
Now, the non-standard models don’t look radically different from the standard ones. That should not be a surprise: after all, the axiomatization specifies properties of the numbers, that then all models have to obey, the conventional one or otherwise. For instance, that zero is not the successor of any natural numbers, that the successor of an even number is odd, the addition is commutative, and infinitely other facts, as well.
As it turns out, all models of the axiomatization ``contain’’ the standard numbers as part. The contain all numbers 0, succ(0), succ(succ(0)) etc., but they contain additional elements as well. They are numbers that can not be described like that. Those are numbers in the model for which there is this no syntactic counterpart, unamed elements, so to say, and since one cannot concretely speak about them in the syntax, they are thus pretty useless. In the area of algebraic data types, elements of a that cannot be named in the syntax are also called junk: elements that cannot be constructed using the constructors of the data type. For the natural numbers, 0 and succ are the constructors, but the same phenomenon occurs also for other data structures one could try to capture in first-order logic.
We said, there is no syntax to refer to the unreachable junk elements. Maybe that should be made more precise: it’s true that there no ground terms to represent junk elements concretely. But one can non-concretely speak about junk, using quantifiers. A formula specifying Forall x. P(x) talks about all emements in the model, including the junk. So also to junk elements, universally quantified axioms apply, so one can also add up junk elements and the addition works commutatively for them as well.
The way to prove unsversally quantified properties is via induction over the natural numbers, that is over natural numbers, and it works as follows. Prove that the property of interest holds for zero, and prove that it’s preserved under successor, i.e., prove that if it holds for some number n that it also holds for n+1. Establishing this proves that the property holds for all natural numbers.
The induction of this form prove a property for all numbers reachable from zero using successor. And that’s exactly all natural numbers, at least in the onventional model.
The non-natural numbers, however, contain junk and that’s the elements unreachable starting from zero. Induction does not speak about them and in the presence of non-standard models of natual numbers, induction simply is not a sound proof rule: doing induction on un-natural numbers would allow to prove things that are not true.
But one probably is not interested in weird unnatural numbers, and one likewise desperately needs induction to do any meaningful proofs. So, better postulate it as one of the axioms
For all P: If P(0) and if, for all n, P(n) implies P(n+1), then that implies P(n) for all n.
If one adds this axiom, the axiom of natural induction, two things happen. The fact that one has put the foot down and requires induction to work. that rules out the un-natural models. Requiring induction now really characterizes the natural numbers. Induction is not simply something useful in connection with natural number, natural induction is in a way a constituent part of the natural numbers, resp. their theory.
Secondly, the above formulation of natural induction is not a first-order axiom! The problem is that it involves a quantification over all predicates P. First-order logics can quantify only over elements of the model, here the natural numbers, but not about predicates over the elements. The induction formulated as above corresponds to a second-order formula, not first-order. And for second-order logics, resp. for the described situation, where we allowed ourselves a single second-order axiom of induction in an otherwise first-order setting, the completeness for first-order proof system is out of the window. Induction in that form is strong enough to characterize the natural numbers, ruling out junk, but results like one of Gödel’s incompleteness theorems tells that there’s not hope for a complete proof theory for that.
(First-order) Peano arithmetic
If on adds induction as above as Peano did, then things change radically. The logic is no longer first-order, one cannot get a complete proof system (which is at the same time sound of course). On the up-side, one has rule out un-natural numbers as possible model and, related to that, one can use induction as proof problem. Something one really needs when proving things about natural numbers…
The exposition here presents Peano arithmetic as a second-order formalization. To avoid confusion, perhaps when reading related material. One can find presentations called Peano arithmetic which are first-order. Peano came up with his axiomatization quite early, when logical treatments like proof systems, etc. were actually not yet established or understood. So he did not call it second-order system, but the induction principle he proposed was second-order.
Later, when more mathematicians worked on logical foundations and formalizations of math, trying to clarify fundamental questions about (limitations of) formalizations, things became more clear. People came then up with first-order version of Peano’s axioms. One can exchange the second order quantification capturing induction in a first-order way!
How is that possible, how can I have induction for all properties without having an axiom that says ``for all predicates…’’? That second-order induction axiom cannot be represented by some first-order equivalent formula, obviously. But who said, we need one formula as replacement.
What one can do is to add infinitely many induction schemas: for each predicate one can formulate in the given signature, one add or assume the corresponging induction principle. Having infinitely many such axioms or axiom schemas is unproblematic. What one a bit sloppily calls axioms is anyway axiom schemas, representing infinitely many axioms; we mentioned that in connection with proof systems.
If one use this infinitely many induction principle instead of a single catch-all second-order axiom, we are back to first-order logics! That means, this axiomatization still has un-natural models with junk, one really needs the power of second-order to exclude them. But one has induction for all predicates we can formulate and all number where it matters, namely the non-junk ones, the natural natural numbers. An no looses sleep over that fact that one cannot reason about junk.
This is sometimes called first-order Peano arithmetic and I added this last paragraph to avoid confusion if one stumbles upon the term ``Peano axioms’’. The original formulation, as said, are second-order, and when speaking just about Peano arithmetic, most would refer to the second-order version. The slightly restricted one is first-order Peano arithmetic.