[FOM] Consistency of first-order logic

[Timothy Y. Chow]

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