[FOM] inconsistency of P and extreme formalism

[Richard Heck]

On 10/10/2011 12:12 PM, Robert Rynasiewicz wrote:
>
> On Sat 08.10.11, at 10:17 PM, Brian White wrote:
>
>> The notions of formula, proof, consistency can be defined
>> in systems that are much weaker than P.  
>>
>
> For my edification, what is the weakest system needed?  (N.B. I'm
> interested in a robust sense of consistency, viz., that a theory is
> consistent iff it is not the case that some sentence and its negation
> are both theorems, not the weaker sense that not everything is a
> derivable [as is the case, e.g., with lambda calculus].) 
>
Well, in some sense, all these notions are definable in Q, and Q, being
Sigma-1 complete, will (e.g.) prove the inconsistency of every
inconsistent theory. But of course Q will not prove many of the
interesting and important properties of these notions. So the
interesting form of the question is something like: What's the weakest
natural theory in which you can "do syntax" to a reasonable degree? And
here, so far as I understand, the consensus answer is something like:
I\Delta_0 + \omega_1 or Buss's S^1_2. Both of these are adequate for
talk about interpretations (in the syntactic sense) of one theory in
another and to prove things like: If B can be interpreted in T, then, if
Con(T), then Con(B)---assuming T and B have "nice" axiomatizations, at
least. In particular, I\Delta_0 + \omega_1 proves that it can itself be
interpreted in Q and so is consistent if Q is (and so it does not prove
Con(Q), unless...).

Of course, as often in these sorts of settings, there are subtle issues
about how exactly things are formalized. See, e.g., Visser's paper "The
Formalization of Interpretability". Everything gets alot neater and
easier if you have exponentiation, and if you have superexponentiation
then you can even prove the cut elimination theorem (restricted forms of
which are available lower.) So, not surprisingly, you get more the
farther you go up the hierarchy of primitive recursive functions. But
you can certainly do enough syntax to claim to understand the notion of
consistency already in theories interpretable in Q.

Richard Heck

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



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20111010/3d29658c/attachment.html>