[FOM] Proof Theory Query

Monroe Eskew meskew at math.uci.edu
Sun Oct 11 14:04:15 EDT 2009

I've seen P1 called "T is fully witnessed" and also "T has Henkin
witnesses."  If T is both complete and fully witnessed, then it has P2
as well.  I don't know what the general relation between P1 and P2 is,
but here's one aspect:  If you look at Peano Arithmetic and restrict
Phi(x) to the Delta_0 formulas, then there is an example where you
have P1 but not P2.  Let Phi(x) be the formula saying x does not code
a proof of 0=1.  Let Psi be something equivalent to Con(PA).

On Sat, Oct 10, 2009 at 7:57 AM,  <joeshipman at aol.com> wrote:
> Let T be a recursively axiomatizable first-order theory in a language
> with countably infinitely many constant symbols c0, c1, ....
> Consider the following properties:
> P1: Whenever ExPhi(x) is in T, there exists i such that Phi(c_i) is in
> T.
> P2: Whenever AxPhi(x)-->Psi is in T, there exist finitely many
> constants c_i1, c_i2, ..., c_i_n such that
> ((Phi(c_i1)&Phi(c_i2)&...&Phi(c_i_n))-->Psi) is in T.
> What are these properties called, and can a theory have one but not the
> other?
> -- JS
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list