Nor is it obvious how multiplication of apples should work. Apples might be considered an infinite cyclic abelian monoid, if you like, but it’s beside the point—the point is that once you know what axioms they satisfy, you now know a whole bunch of stuff.
Bakkot
Karma: 874
No, not quite. The distinction is subtle, but I’ll try to lay it out.
there are statements that are true (semantically valid) but unprovable, and hence they provide a counterexample to “If X |=Y then X |- Y”
This is not the case. The problem is with the ‘and hence’: ‘X ⊨ Y’ should not be read as ‘Y is true in X’ but rather ‘Y is true in every model of X’. There are statements which are true in the standard model of Peano arithmetic which are not entailed by it—that is, ‘Y is true in the standard model of Peano arithmetic’ is not the same as ‘PA ⊨ Y’. So this is not a counterexample.
Rather, the notion of ‘complete’ in the incompleteness theorem is that a model is complete if for every statement, either the statement or its negation is entailed by the model (and hence provable by semantic completeness). Gödel’s incompleteness theorem shows that no theory T containing PA is complete in this sense; that is, there statements S which are true in T but not entailed by it (and so not provable). This is because there are models of T in which S is not true: that is, systems in which every statement in T holds, but S does not. (These systems have some additional structure beyond that required by T.)
Wikipedia may do a better job of explaining this than I can at the moment.
I happen to be studying model theory at the moment. For anyone curious, when Eliezer say ‘If X ⊢ Y, then X ⊨ Y’ (that is, if a model proves a statement, that statement is true in the model), this is known as soundness. The converse is completeness, or more specifically semantic completeness, which says that if a statement is true in every model of a theory (in other words, in every possible world where that theory is true), then there is a finite proof of the statement. In symbols this is ‘If X ⊨ Y, then X ⊢ Y’. Note that this notion of ‘completeness’ is not the one used in Gödel’s incompleteness theorems.
I think it’s worth mentioning explicitly that the second-order axiom introduced is induction.