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!