[FOM] Consistency of first-order logic

[meskew at math.uci.edu]

I think a better approach the original question of where the complexity
lies is to try to construct a universal program over all computable
theories.  That is, make a program that has a parameter an axiom system
(i.e. number for a recursive set), which halts iff the theory is
consistent.  This makes the question of coding FOL inference rules
independent of the theory, so seems to better address the question of
whence comes the complexity.  It also avoids the thorny issue of trying to
work in an extremely weak theory where somehow talking about consistency
still makes sense.  So then one can ask, how long is the shortest program
with this property?  (Of course don't expect the program to be able to
tell good inputs from bad, just to do the right thing on all the codes for
recursive sets.)

Monroe


> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>