[FOM] Consistency of first-order logic
Timothy Y. Chow
tchow at alum.mit.edu
Wed Apr 27 16:13:45 EDT 2011
There was a recent question by Scott Aaronson on MathOverflow---
http://mathoverflow.net/questions/62859/simpler-statements-equivalent-to-conpa-or-conzfc
---that is similar to a problem mentioned by Harvey Friedman some years
ago here on FOM, namely of finding equivalents of Con(ZFC) or Con(PA),
where by an "equivalent" is meant a small (= low quadruple count) Turing
machine whose halting is provably equivalent to Con(ZFC) or Con(PA) in a
very weak system.
Aaronson implicitly raised the further question of how much of the
difficulty of compressing the Turing machine is due to the axioms and how
much is due to the calculus of first-order logic itself. My question is,
is there any way to make this further question precise? My first instinct
was to let "Con()" denote the statement that first-order logic is
consistent, and repeat the question with Con() in place of Con(ZFC), but
I'm not sure this makes any sense. It would seem that we would need to
work in a system so weak that it doesn't prove Con(). Is there any such
system in which we can formalize enough reasoning to make this an
interesting question?
Tim
More information about the FOM
mailing list