FOM: a question re. completeness

[Stephen G Simpson]

Michael Detlefsen 3 Feb 1998 10:54:27 writes:
 > T is consistency-complete iff for every sentence s of the language
 > of T that is not provable in T, if s were provable in T, T would be
 > inconsistent.

I would say that this isn't a very precise definition, one of the
difficulties being that it contains a counterfactual conditional.  Let
me try to make it a little more precise, as follows.

Background: We know of many "mathematically natural" statements in the
language of PA that are independent of PA.  The first such
independence result was due to Paris-Harrington.  But all of these
independent sentences that we know of seem to satisfy (*)

   (*)  either PA |- S -> Con(PA), or PA |- (not S) -> Con(PA) .

(Here Con(T) means "T is consistent".)  Of course we can diagonalize
to make up artificial sentences S in the language of PA which do not
obey (*), but they aren't "mathematically natural", at least I don't
know of any that are.  So this seems to be an interesting property of
PA.  Furthermore, it's a property that is not shared by ZFC, because
for example neither the continuum hypothesis nor its negation implies
Con(ZFC), and ditto for a host of other independence results proved by
forcing.

The property in question, which T = PA has and T = ZFC doesn't have,
is:

   Property C:

   For every "mathematically natural" proposition S in the language of
   T, either T |- S -> Con(T) or T |- (not S) -> Con(T). 

This seems to be a foundationally interesting property of T = PA and
possibly other important f.o.m. systems.

Questions: Can we state property C in a more correct and/or more
comprehensive and/or more precise way?  Am I overlooking something?
What's going on here?  

I'm sure that many people here on the FOM list can do better than I
did above.  I wouldn't be surprised if property C is already well
known to many people, in some precise version.

I guess this ties in somehow with the recent Friedman/Steel discussion
of "pictures" and CH.  Can anyone spell out this connection?

-- Steve