"Consistent" means that there is no proposition P such that both P and not-P have proofs within the theory. If F itself is consistent, then F+Not(Con(F)) will also be consistent, since Con(F) will have no proof in this theory. (Conversely, if F itself is inconsistent, then Con(F) will have a proof in this theory (since any proposition will have a proof in an inconsistent theory), so F+Not(Con(F)) will also be inconsistent.)
"Sound" means that there exists some semantic model of the theory that the theorems of the theory accurately describe. This cannot true of the theory F+Not(Con(F)), since there are only two possibilities:
(1) F itself is consistent--which means that, while F+Not(Con(F)) is also consistent, it can't be sound, because the theorem (by virtue of being an axiom) Not(Con(F)) cannot accurately describe any semantic model of the theory; or
(2) F itself is inconsistent--which means that the theory F+Not(Con(F)) has no possible semantic model at all (since F, a subset of the theory, cannot--no inconsistent theory can have any semantic model), and therefore cannot be sound (since to be sound a theory must have some semantic model).
1. is not true. There are semantic models of `F + Not(Con(F))` that accurately describe the theory. The difference is that these models contain nonstandard natural numbers (these nonstandard numbers become the Godel numberings of the proofs of `Not(Con(F))`) if `F` is "truly" consistent (according to the standard model of PA).
The fact that there must be semantic models of any consistent theory is a cornerstone of first-order logic and is e.g. not true of second-order logic. This follows from Godel's Completeness Theorem (not Incompleteness Theorems).
> There are semantic models of `F + Not(Con(F))` that accurately describe the theory.
That depends on what you allow to count as "accurately describing" the theory. See below.
> The difference is that these models contain nonstandard natural numbers (these nonstandard numbers become the Godel numberings of the proofs of `Not(Con(F))`) if `F` is "truly" consistent (according to the standard model of PA).
These "proofs" are only "proofs" if you accept "proofs" with an infinite number of steps. In the post I originally responded to in this subthread, there is a quote from the Aaronson article that describes it this way:
"it has a model (involving “nonstandard integers,” formal artifacts that effectively promise a proof of F’s inconsistency without ever actually delivering it)"
Aaronson doesn't accept these "proofs" as being valid, which is why he takes the position that F + Not(Con(F)) is unsound--or, to put it the way I was putting it, that Not(Con(F)) does not accurately describe the theory since F is consistent but Not(Con(F)) says it isn't. That is also the position I have been taking.
The position you are taking is that Not(Con(F)) does accurately describe the theory--and therefore that the theory F + Not(Con(F)) is in fact sound--because we can reinterpret the formula Not(Con(F)) to mean, not "there is some standard natural number that gives a proof that F is inconsistent", but "there is some non-standard natural number that gives a proof that F is inconsistent". Then, as noted, you would also have to reinterpret the notion of "proof" to allow "proofs" that contain an infinite number of steps and never actually end, since that is what a proof whose Godel number is a non-standard natural number would look like. And since such a proof never actually ends, it never actually delivers a formula that says "F is not consistent", so it never actually makes the formal system inconsistent.
In the end this is not really a dispute about the math--we agree on what the formal theory is, what its possible semantic models are, and what properties those models have--but on the use of words like "proof" and "accurately describe". So there isn't really a way to resolve such a dispute; we just have to be aware that there are two different viewpoints on how such ordinary language words can be used to describe the math.
> The fact that there must be semantic models of any consistent theory is a cornerstone of first-order logic and is e.g. not true of second-order logic. This follows from Godel's Completeness Theorem (not Incompleteness Theorems).
No. They are numbers that cannot be reached from zero by applying the successor operation. In other words, they are part of a separate infinite "chain" of numbers that "looks like" the integers (negative, zero, and positive), but is not the same as the chain of numbers that starts from zero and is the "standard" natural numbers. The first-order axioms of arithmetic cannot rule out the existence of such chains; those axioms imply that there is a chain that starts from zero (the "standard" natural numbers), but they cannot prove that it is the only chain that exists.
Yes, that's how I remember it being explained. But what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange, but if non-standard numbers aren't infinite, how can the proof be infinite?
> what sort of proof could correspond to a non-standard number? It seems like it would have to be rather strange
Yes.
> if non-standard numbers aren't infinite, how can the proof be infinite?
I am not an expert on this, but as I understand it, it has to do with how Godel numbering would have to work if non-standard numbers can be Godel numbers. Basically, only a standard natural number can be the Godel number of a finite proof; any proof that has a non-standard number as its Godel number must be infinite (i.e., it must have an infinite number of steps). But unfortunately I cannot explain why that is true. Maybe another poster here can, or can correct me if my understanding is wrong.
My usual interpretation of this is not that we have strange proofs, but rather to interpret this as a failure of Godel encodings to completely capture the notion of proof.
That is the statement Con(T) isn't really a statement about the consistency of T, but rather a statement that is "close enough" to suffice for many, but not all purposes.
"Consistent" means that there is no proposition P such that both P and not-P have proofs within the theory. If F itself is consistent, then F+Not(Con(F)) will also be consistent, since Con(F) will have no proof in this theory. (Conversely, if F itself is inconsistent, then Con(F) will have a proof in this theory (since any proposition will have a proof in an inconsistent theory), so F+Not(Con(F)) will also be inconsistent.)
"Sound" means that there exists some semantic model of the theory that the theorems of the theory accurately describe. This cannot true of the theory F+Not(Con(F)), since there are only two possibilities:
(1) F itself is consistent--which means that, while F+Not(Con(F)) is also consistent, it can't be sound, because the theorem (by virtue of being an axiom) Not(Con(F)) cannot accurately describe any semantic model of the theory; or
(2) F itself is inconsistent--which means that the theory F+Not(Con(F)) has no possible semantic model at all (since F, a subset of the theory, cannot--no inconsistent theory can have any semantic model), and therefore cannot be sound (since to be sound a theory must have some semantic model).
Possibility #1 above answers your question.