What about Godel’s first and second incompleteness theorems? They were not proven using any axiom system. Godel’s proof worked by substituting certain characters in PM with abbreviations, and then abbreviating those abbreviations, etc. He did so in a way that created a string of PM which stated that “this string’s Godel number is not a PM number.” He then used reasoning as old as the famous Cretan to show that that statement could never be consistently decided upon.
These results were shown about axiomatic systems of sufficient strength, but not inside of anyone system. Godel’s completeness theorem of first order logic functions in a similar way (reasoning about a formal system rather than within it). All of these results are achieved by model theoretic methods; if you want to know how you prove something outside of a proof theory look at model theory.
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.
What about Godel’s first and second incompleteness theorems? They were not proven using any axiom system. Godel’s proof worked by substituting certain characters in PM with abbreviations, and then abbreviating those abbreviations, etc. He did so in a way that created a string of PM which stated that “this string’s Godel number is not a PM number.” He then used reasoning as old as the famous Cretan to show that that statement could never be consistently decided upon.
These results were shown about axiomatic systems of sufficient strength, but not inside of anyone system. Godel’s completeness theorem of first order logic functions in a similar way (reasoning about a formal system rather than within it). All of these results are achieved by model theoretic methods; if you want to know how you prove something outside of a proof theory look at model theory.
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.