/sci/ - Science & Math

>>15411834
- Firstly, there are several theorems.
- Secondly, it's a metalogical theorem, so we operate on two levels. You typically view the metalogical level as the normal level, and you study some axiom system as if it's algebra. As some mathematical tool you might want to adopt to be a little bit more clear and sure about your formal proofs etc.

- So on the one hand, they concern theories T recursively enumerable set of axiom (meaning you can write a program that lists the axioms - there might be countably infinite of them, such as when you adopt an axiom schema, such as a Indcution in Peano arithmetic of Separation in set theory.)
- On the other hand, they concern T-independent propositions. Those are some statements 'P' such that the theory T neither proves nor 'Not P'.
- The main tool invented for the proof is, in essence, programming language theory. For the proof of the first theorem, we don't need the Gödel's full language, however. We just need to know about primitive recursive (p.r.) functions. In effect, they correspond to fixed size for-loops. E.g. you can code function taken an n and then you're allowed to do arithmetic operations with n, say map it to n^7, and then do a for-loop of depth n^7.
- The theories T we consider aren't merely required to have axioms we can run through, they also need to be able to encode arithmetic. Particularly, the arithmetic axioms they need to be able to encode are those of Peano arithmetic (rules about how zero, equality, addition and multiplication relate to each other) and the predecessor existence claim. Call those axioms Q

>>11672730
>The tweak would need to make the diagonal argument invalid.
No, sets such as [math] {\mathbb R} [/math] would still be uncountable for the same reasons.

>ZFC
ZF
Since
https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
spoils all the fun models

>>11625419
the thing that animates you