@LeakyNun Yes we can't, and that's the ideal case unless we don't believe there is a model of PA.
We do have empirical evidence that PA has a very good approximate real-world interpretation, and so conceptually it seems that ACA is not only consistent but sound. It gets hairy beyond that, because it is not so clear how quantifying over subsets of N should be interpreted.
@LeakyNun: If you star the above, it won't fall down the pinboard so quickly. =)
Note that if you look carefully at the proof that Q' is independent, you will see that it relies on soundness for program halting only to show that the system does not prove Q. That assumption is not needed to ascertain the truth value of Q'. Hence in the later section I stated the relation between Q' and consistency for classical systems without mentioning soundness for program halting.
Well I shouldn't say "same", because it's much clearer using programs than wading through representability of recursive sets in PA.
That's why I say you need to read it to understand the incompleteness stuff, unless you want to try the standard route. Godel basically constructed Q' but expressed in arithmetic.
He first encoded a program interpreter in arithmetic and then encoded the formal system as a program and then constructed a formula corresponding to provability and then diagonalized in the same manner as C against H.
Because of using arithmetic, there are some technical issues as well, so the underlying idea is thoroughly obscured.
I think Godel didn't find the clean way because he came before Turing.
We can take the simplest example of the existence of a basis of any given vector space V. By transfinite induction V can be well-ordered. Initialize S = {}, then enumerate the vectors in V in that order and at each stage add the current vector v to S iff S⋃{v} is linearly independent. At the end, clearly every vector in V is in span(S), and we just have to check that S is linearly independent, which you should be able to prove.
If S is not linearly independent, then there is a finite non-trivial linear combination of vectors in S that sums to the zero vector in V. Thus one of those vectors was added to S after all the rest (because finitely many of them). That one would not be added because at that point it is in the span of the previously added vectors.
That's why I said earlier that I think any non-set-theoretic use of transfinite induction should not have to split cases between the successor and limit stages, and should not even have to care about ordinals. Otherwise it's very likely that the proof has taken an unnecessary detour.
@MatheinBoulomenos The induction axiom you may have been taught may not be the right one.
There is second-order induction, namely any set that has 0 and is closed under successors contains the natural numbers.
The problem with that is that it is simply useless, unless you also have set construction axioms. In particular, it seems that Peano's axioms have exactly this flaw; they were never sufficient to begin with.
The correct induction is an axiom schema (list), not a single axiom. This is why nowadays PA refers to this first-order system and not Peano's original. You have one axiom for each predicate over the language of arithmetic.
How do the mathematicians that write standard natural numbers have formal consensus on what they are talking about?
Mathematicians work in a meta-system (which is usually ZFC unless otherwise stated). ZFC has a collection of natural numbers that is automagically provided for by the axiom of ...
In short: The so-called definition of natural numbers as those that can be obtained from 0 by adding 1 repeatedly is circular, but there is no viable alternative, which already makes it impossible to uniquely pin down natural numbers mathematically. Worse still, there does not seem to be ontologi...
If ZFC is consistent then ZFC has a countable model.
ZFC never proved that it has a model.
Do you get it? You need to be careful of which system you are working in. Suppose we work in a relatively simple meta-system MS that only knows the basic properties of strings and natural numbers and programs, and can define the halting problem and define sets based on the solution to the halting problem.
You can think of this as MS being able to construct programs that can call an oracle that gives the answer to the halting problem for any program and input.
@LeakyNun: I'll elaborate on my point that we can in fact perform that process using the first Turing jump H(1), also known as the halting oracle. There are many programs using H(1) that are proof verifiers for a complete consistent extension of any consistent formal system. You just use any computable enumeration of all sentences, and at each step you use H(1) to find out whether that current sentence is consistent with the previous ones and if so then add it but otherwise add its negation.
NL: To be really precise, I sometimes label everything I say with the system I'm talking in, such as NL for natural language.
@MatheinBoulomenos I am not actually familiar with the derived series, but it appears that at each stage you can simply take the commutator subgroup of the intersection of the preceding groups. Like with the vector space basis construction, this creates a monotonic sequence, so it will work out.
In algorithmic terms, at each stage you shrink the group to its commutator subgroup. At limit stages, the earlier shrinking steps would have ended up producing the intersection already, and in the original definition you stop there while in my definition you would take the commutator subgroup again.
To paint a more complete picture, you are right in that an axiomatization may very well have no model. An axiomatization is meaningless if nothing satisfies it. But if we can prove that there is a model, and the axioms are the only properties we care about, then we can happily work within the axi...
Compactness here means ( finitely satisfiable implies satisfiable ).
It is still true that for second-order logic we have ( finitely consistent implies consistent ).
@LeakyNun Just extend second-order PA by a constant c and add axioms stating that c is greater than each standard numeral. Then the resulting theory is finitely satisfiable, but has no model in full second-order semantics.
Because we already proved (we are in MS remember?) that there is only one model of PA and it doesn't have any element that is greater than each standard numeral...
@LeakyNun Take the language of graphs with the edge relation and the second order theory of connected graphs, which can be axiomatized by simply ( every connection-maximal set contains everything ).
Just to finish the earlier example, since there is no model of the extended theory in full second-order semantics, it fails completeness because there is no proof of a contradiction (since it is actually consistent).
To continue the example of the theory of connected graphs, we can do the same trick, I think.
Then these examples fit the bill. I have explicitly described two second-order theories in which you cannot prove something that is true about all models (because there are no full semantics models).
@MatheinBoulomenos @LeakyNun: Okay okay I satisfy you both at one go. Let PA2 be PA plus the second-order induction axiom. PA2 has essentially one full-semantics model, but PA2 does not prove Con(PA), since PA2 is conservative over PA. This is trivial to see because PA2 cannot use the induction axiom since it has no set-construction axioms! But of course every model isomorphic to N satisfies Con(PA).
Happy now? =D
I changed PA− to PA but it actually doesn't make a difference to the resulting theory. Just easier to justify my claims later.
@LeakyNun You could use fields to get another example that has nothing to do with the incompleteness theorems. Take the first-order theory F of fields with characteristic 0. Then every model of F has an infinite subfield. This can be stated as an existential second-order sentence, but of course cannot be proven by F since F has no set-existence axioms.
Your confusing stems from the way many articles about Godel's incompleteness theorems are extremely imprecise. Here is a proper definition.
$\def\nn{\mathbb{N}}$
We say that a sentence $φ$ over a language $L$ is true in an $L$-structure $M$ iff $M \vDash φ$.
For convenience, when $L$ is ...
