But there is something I didn’t get : what does Con() mean in PA+Con(PA) ? Maybe it’s stupid question and everyone is supposed to know, but I don’t remember ever encountering that symbol, and I can’t find it’s meaning, neither on Wikipedia nor on mathworld...
It means consistent. PA + Con(PA) means PA together with the axiom that PA is consistent (which can be expressed in PA because PA can express “PA proves X,” so “PA is consistent” can be expressed as “PA does not prove a contradiction”).
Actually, “not proving a falsehood” is not the same as being consistent; assuming that PA is consistent, the theory PA+~Con(PA) is also consistent, but proves the false statement ~Con(PA). Consistency is the weaker condition of not proving both a formula and its negation.
Sounds awesome, great job !
But there is something I didn’t get : what does Con() mean in PA+Con(PA) ? Maybe it’s stupid question and everyone is supposed to know, but I don’t remember ever encountering that symbol, and I can’t find it’s meaning, neither on Wikipedia nor on mathworld...
It means consistent. PA + Con(PA) means PA together with the axiom that PA is consistent (which can be expressed in PA because PA can express “PA proves X,” so “PA is consistent” can be expressed as “PA does not prove a contradiction”).
More concretely, “PA is consistent” can be as expressed “PA does not prove 1 = 2″.
Actually, “not proving a falsehood” is not the same as being consistent; assuming that PA is consistent, the theory PA+~Con(PA) is also consistent, but proves the false statement ~Con(PA). Consistency is the weaker condition of not proving both a formula and its negation.
I should have said “contradiction”; edited. I intended “falsehood” to mean “false in all models,” not “false in the standard model.”
If I understand this correctly, Con(PA) is: “(PA proves X) implies !(PA proves !X)”. Did I get that right?