[FOM] Re. Is ConQ provable in Q?

[mdetlef1@nd.edu]

In addition to the work of Bezboruah and Shepherdson already noted by several
people in connection with Arnon's original note, I think it worth mentioning a
too-little known paper of the late Robert Jeroslow's. This is: "Consistency
Statements in Formal Theories", Fundamenta Mathematicae 72 (1971): 17--40.
Theorem 1.5 in that paper gives a (weak) theory V that is a subsystem of PA,
that strongly represents all pr fncs and weakly represents all re sets and
which proves a consistency sentence Con(V) constructed in the usual way from an
axiomhood predicate that weakly represents the set of axioms of V and which has
this form:  (x)(Prov_V(x) ---> neq(x, [o=1 & not 0=1])), where neq(x, y) is the
standard encoding of the pr relation 'not x=y'.

Best (from a sunny Florence),

Mic Detlefsen