I know that you can formalize Godel’s incompleteness theorems, but they were not formalized originally, nor did they need to be formalized to be valid deductive arguments.
Now, you can’t really formalize Godel’s proof without abbreviation, this I know. The godel number of sentence G is a huge number that none of us could ever write down and that a computer would probably have a hard time holding as a value. Have you ever seen a proof of Euclid’s prime theorem in PA? Euclid gave a 6 step proof, in PA there are over 50 steps because every single peice of reasoning gets written down. To actually directly reference every peice of reasoning in godel’s proof is something Godel never does in undecidable props of PM and something that he has no need to do.
To be a valid deductive argument, a theorem must be formalizable. That doesn’t depend on accidental facts like whether its original presentation was formalized or not.
I know that you can formalize Godel’s incompleteness theorems, but they were not formalized originally, nor did they need to be formalized to be valid deductive arguments.
Now, you can’t really formalize Godel’s proof without abbreviation, this I know. The godel number of sentence G is a huge number that none of us could ever write down and that a computer would probably have a hard time holding as a value. Have you ever seen a proof of Euclid’s prime theorem in PA? Euclid gave a 6 step proof, in PA there are over 50 steps because every single peice of reasoning gets written down. To actually directly reference every peice of reasoning in godel’s proof is something Godel never does in undecidable props of PM and something that he has no need to do.
To be a valid deductive argument, a theorem must be formalizable. That doesn’t depend on accidental facts like whether its original presentation was formalized or not.