Re:Proving false in Coq using an implementation bug
by ttctciyf on Tuesday March 24, 2015 @10:00PM
(#9260856)
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.
[ Parent
| on HN ]
Re:Proving false in Coq using an implementation bug
by ObviousScience on Wednesday March 25, 2015 @12:26AM
(#9261287)
Only 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.
Re:Proving false in Coq using an implementation bug
by eli_gottlieb on Wednesday March 25, 2015 @01:23PM
(#9264391)
Weirdly 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.