[FOM] systems that prove their own consistency

[Michael Detlefsen]

>On Sep 5, 2004, at 3:02, 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)?
>I'm pretty sure I've heard of such things being studied somewhere, but can't
remember where and can't find the references..

In "Consistency statements in formal theories", 
Fundamental Mathematicae 72 (1971): 17--40, 
Robert Jeroslow described (Theorem 1.5) a 
subtheory V of PA such that (i) V has an RE (in 
Feferman's sense) axiomhood predicate v(x), (ii) 
V strongly represents all recursive functions and 
weakly represents all r.e. sets, and (iii) V 
proves Con*_V, where Con*_V is a formula 
'(x)(Prov_v(x) --> Neq(x, [0=1 & ~ 0=1]))', in 
which 'Prov_v(x)' is a provability formula for V 
formed in any of the usual ways from the RE 
axiomhood predicate mentioned above, '[F]' stands 
for the numeral for the Gödel number of 'F', and 
'Neq(x, y)' is a formula expressing the standard 
encoding of 'x‚y'.

>From a hot and humid South Bend,

Mic Detlefsen