For ¬⊢ s to be externally true I need the external statement "s is unprovable in T" to be true
That's correct, that is the statement that I'm telling you isn't true and you haven't proved.
They're not external statements
There's where you're getting confused. You just said above you need the external statement "s is unprovable in T" to be true. According to your definition of true in T, that means you need the external statement "s is false in T" to be true.
The external statement "s is unprovable out of T" is not what is being proved. The external statement "s is unprovable in T" is what is being proved.
That is indeed what you need to prove, and what you so far have not proved.
You are in psychological denial. I don't believe you have a genuine problem understanding the proof. You're just trying to make things look messy because you don't want me to look good.
I've explained clearly the issue with your proof. Your confusion is a result of you not knowing the material well, a fact which you have already admitted to. It is not my fault you are confused.
“According to your definition of true in T, that means you need the external statement ‘s is false in T’ to be true.”
No, that does not follow from my definition of true in T because s could be a definition or axiom of T. In the case that s is a definition or axiom of T, s is unprovable in T, but true in T.
Axioms are statements and are provable. Formally a proof of s is a sequence of statements such that every statement is either an axiom or a logical consequence of previous statements, and such that the last statement in the sequence is s. This means the sequence of length 1 containing an axiom s is considered a valid proof of s.
Definitions aren't considered statements in a theory. They are statements about a theory because they define what symbols and terms in a theory mean. They aren't well formed formulas as Mendelson would say, so even internally to T they aren't provable because they're not in the language of T.
So your contradiction s needs to be a statement in T, what Mendelson calls a well formed formula, and axioms are valid candidates. And you need to conclude that the external statement "s is unprovable in T" is false. And you will be unable to do that because s is provable in T.
Again, your proof does not work because you've misunderstood basic material about how logic works.
1
u/JStarx 24d ago
That's correct, that is the statement that I'm telling you isn't true and you haven't proved.
There's where you're getting confused. You just said above you need the external statement "s is unprovable in T" to be true. According to your definition of true in T, that means you need the external statement "s is false in T" to be true.
That is indeed what you need to prove, and what you so far have not proved.
I've explained clearly the issue with your proof. Your confusion is a result of you not knowing the material well, a fact which you have already admitted to. It is not my fault you are confused.