Re: Answer to a question, and further speculation on a QED foundation

• Mail folder: QED
• Next message: David McAllester: "Verification systems "
• Previous message: Robert S. Boyer: "Feferman FSO reference"
• In-reply-to: Robert S. Boyer: "Answer to a question, and further speculation on a QED foundation"

To: QED <qed@mcs.anl.gov>
Subject: Re: Answer to a question, and further speculation on a QED foundation
In-reply-to: Your message of Sun, 18 Apr 93 12:36:45 -0500. <9304181736.AA13372@axiom.CLI.COM>
Date: Sun, 18 Apr 93 21:28:49 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-id: <"swan.cl.ca.904:18.04.93.20.28.57"@cl.cam.ac.uk>
Sender: qed-owner
Precedence: bulk

Bob Boyer writes:

> I feel a little bit queasy talking about `intension' in view of the
> fact that all the consistent, recursively axiomatizable theories I
> know about that include the primitive recursive functions admit
> multiple models.

Indeed, if you are talking about first-order theories, then since any
arithmetic worth the name has an infinite model, it must, by the upward
Lowenheim-Skolem theorem, have models of arbitrarily large cardinality,
which obviously can't all be isomorphic.

In fact I believe not all models can even be elementarily equivalent for the
following reason: any model assigns a definite true/false value to any
closed term. But if all models are elementarily equivalent, then a sentence
must either be true in all models or false in all models. This would mean
the theory is deductively complete (because FOL is semantically complete).
If the theory includes much arithmetic, Godel's theorem rules this out,
given consistency and recursive axiomatizability.

Perhaps PRA or FSO are so weak that this does not apply? Apparently they 
lack the usual quantifier rules. Maybe someone could post a brief 
explanation of what PRA is like, for those of us who don't know.

John Harrison (jrh@cl.cam.ac.uk)