[FOM] Re. Is ConQ provable in Q?

[Andrew Boucher]

The example in that paper has V as a certain fixed point extension of S 
v (x)(y)(x = y), where S is the conjunct of all the axioms of 
Robinson's Q.  As I may be misrecalling, Jeroslow also had the example 
of {S v (x)(y)(x = y) : S is an axiom or instance of an axiom schema of 
PA}.  If that is so, does anyone have a reference?   Did Jeroslow have 
any more natural examples?

(From a cloudy Paris!)

On Jun 4, 2005, at 5:42 PM, mdetlef1 at nd.edu wrote:

>
> ...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'.