I've been asked to teach an intro to logic and computation course. This is not a field that I am particularly familiar with, but I am happy to have the chance to learn it - hopefully - properly.
Since I don't have anyone else to bounce ideas off around here, I've taken to this forum for help. Let me know if there is a better place I can go.
My question is about "true (in some model) but not provable sentences" in first order languages/theories.
In the first order language/theory of groups, we can write down first order sentences that are true in some groups and false in others. For example, commutativity of the group operation
$$ \forall x,y \quad xy = yx $$
My understanding is that particular groups (for example, the symmetric group on 5 elements) are the models for the first order language of groups. If the sentence is true in some groups (i.e. models) and false in other groups (i.e. models), the completeness theorem says we can't prove (pick your favourite proof theory) the sentence in this first order language of groups.
Assuming that is all correct, then my question is this: is the sentence (above) describing the commutativity of multiplication the same type of "Godelian" sentence as the one Godel came up with in Peano Arithmetic? Is it "true but not provable" in the same sense? Or am I getting at something else here with this example?
Other examples that feel like this are (i) the parallel postulate: true in the Euclidean model of the other four axioms, but false in any non-Euclidean model of the other four postulates and (ii) the axiom of choice in ZFC.
Historical question: At the time Godel published his incompleteness result, was it known whether or not the Peano Axioms had non-standard models? Or was his result one of the steps in that direction? His sentence showed that there are things true (in the "usual model") but not provable, thus (at least to me, with the benefit of hindsight) hinting at other models?
Any comments and clarification would be great for me... and the class!
It's mostly correct, with the exception that unprovability of statement that is false in some models is implies by correctness theorem, not completeness.
Correctness: if it can be proved, it is true in all models. Completeness: if it is true in all models, it can be proved.
What's most interesting in Godel theorem is not that it says incompleteness of say $PA$ - there are a lot of non complete theories, may be we just miss one or two simple properties, like Pasch's axiom. It says that there is no ("good") extension of $PA$ which is complete.
It's not the same case for group theory: for example, adding axiom $$\exists x, y((\forall z (z = x \vee z = y))\wedge(xx = yy = x \wedge xy = yx = y))$$ make the theory complete (the only model is $\mathbb Z_2$). And the Eucliden geometry is already complete.
About history - while existence of non-standard models is by now day standards trivial consequence from compactness theorem, which was published by Godel in 1930, it seems like it was not understood at this point. The incompleteness theorem was published by Godel in 1931, while existence of non-standard model was published by Skolem in 1934.
However, existence of non-standard models is probably much less interesting than incompleteness. For example, there is countable model of Euclidean geometry, and there is model of it with cardinality greater than continuum, but that doesn't seem to bother anyone.