[FOM] Consistency of first-order logic

[Richard Heck]

> 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?
>
I'll speculate that Q does not prove Con(). If Q does prove Con(), then
I further speculate that R does not prove Con(). The lack of induction,
in both cases, makes it hard to see how the proof would go.

Of course, there are issues about whether Q can really make sense of
consistency statements, but perhaps we can set those aside momentarily.

Richard


-- 
-----------------------
Richard G Heck Jr
Romeo Elton Professor of Natural Theology
Brown University