[FOM] Re: Consistent logics with non-well-founded definitions?

[Timothy Y. Chow]

Bryan Ford wrote:
>On a similar note, can anyone give me pointers to any studies of formal
>logic systems (however weird or contrived) that can prove themselves
>consistent, but are nevertheless consistent (e.g., their consistency is
>provable in ZFC)?

This isn't exactly what you asked for, but you might also be interested in 
certain "near-misses."  For example, the theory T = ZFC + ~Con(ZFC) is 
omega-inconsistent and has the property that T proves the existence of a 
set S such that for every axiom phi of T, T proves "phi is true in S."
Note that this isn't quite the same as T proving itself consistent, which 
would be something like "T proves that for every phi in T, phi is true in 
S."  Intuitively, omega-inconsistency means that T thinks that there are 
nonstandard axioms, and T can only prove the consistency of its standard
axioms.

One can also play games with the consistency predicate itself.  Exercise 
36 of Chapter 4 of Kunen's book "Set Theory" says:

  Show that there is a formula chi(x), such that
  (a) chi represents ZF; i.e.,
       if phi is in ZF then ZF |- chi("phi"), and
       if phi is not in ZF then ZF |- ~chi("phi"), and
   (b) if "ZF" is added via the definition "ZF" = {x : chi(x)},
       then ZF |- CON("ZF").

Here ZF denotes the axioms of ZF, not their closure under consequence.  
One solution is to let chi say something like, "phi is an axiom of ZF
and is consistent with the chi-axioms that precede it."  There has been
some discussion in the literature about whether this kind of consistency
predicate provides any hope of reviving Hilbert's program.  The majority
view, which I agree with, is that these consistency predicates don't
correctly express the concept of consistency; as Roger Bishop Jones
put it once, chi(x) doesn't mean "x is an axiom of ZF" but just happens
to have the same extension if ZF is consistent.  So Hilbert's second
problem is still dead.

Tim