[FOM] Proof Theory Query

[Thomas Forster]

I am told that they are both called the *strong existence property*
Your P1 is the version appropriate for constructive theories, and P2 the 
version for classical theories.  Typically a constructive theory 
satisfying P2 will satisfy P1 but this is not true for classical theories.


        tf




On Sat, 10 Oct 2009 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
> 

-- 
URL:  www.dpmms.cam.ac.uk/~tf; 
DPMMS ph: +44-1223-337981; 
UEA ph:  +44-1603-592719
Cant'y office fone: +64-3-3642987 x 8152
mobile in UK +44-7887-701-562; 
mobile in NZ +64-210580093.