3 ms·
I think it's something like this: you can't prove the consistency of a formal system using that same formal system, unless it is in fact inconsistent, but you c
by ttctciyf 12y ago
I think it's something like this: you can't prove the consistency of a formal system using that same formal system, unless it is in fact inconsistent, but you can model a formal system from inside a larger formal system and then prove things like consistency about the smaller system from inside the larger one. But then the consistency of the larger system is unproven and you're stuck with an endless regress into ever larger FS's as you pursue the chimera.
- ObviousScience 12y agoOnly for sufficiently powerful systems, I believe. Things like first order logic are too simple to introduce the kinds of statements Godel used to prove the incompleteness theorem about arithmetic.
- eli_gottlieb 12y agoWeirdly enough, as Gentzen showed, you can use a theory that is "sideways" to first-order logic, neither strictly more powerful nor weaker nor equivalent in power, to demonstrate the consistency of first-order logic. Strong normalization theorems are used for typed lambda calculi like the Calculus of Inductive Constructions to show consistency, as well.