Gödel’s theorems can be formalized. Here’s a formal proof of the first one in Coq. Also, paragraph 8.4 there explains how the second incompleteness theorem can be proved by formalizing the proof of the first one within the system in question.
Model theory is not “platonic”, it lives within an ambient set theory. There are different axiomatizations of set theory, e.g. ZFC, which give rise to different “model theories”. An example from Wikipedia:
There is a finite second-order theory whose only model is the real numbers if the continuum hypothesis holds and which has no model if the continuum hypothesis does not hold. This theory consists of a finite theory characterizing the real numbers as a complete Archimedean ordered field plus an axiom saying that the domain is of the first uncountable cardinality.
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.
Gödel’s theorems can be formalized. Here’s a formal proof of the first one in Coq. Also, paragraph 8.4 there explains how the second incompleteness theorem can be proved by formalizing the proof of the first one within the system in question.
Model theory is not “platonic”, it lives within an ambient set theory. There are different axiomatizations of set theory, e.g. ZFC, which give rise to different “model theories”. An example from Wikipedia:
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.