[FOM] systems that prove their own consistency
Michael Detlefsen
Detlefsen.1 at nd.edu
Mon Sep 6 17:04:20 EDT 2004
>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
More information about the FOM
mailing list