[FOM] Existence property

[Studtmann, Paul]

Dear Professor Friedman,
 
I have a question that might be appropriate for FOM discussion, but it might
also be the case that you could answer the question for me.  I was recently
reading your paper The Disjunction Property Implies the Numerical Existence
Property Proc. Nat. Acad. Sci. USA, 1975.  Your proof holds for systems that
include the axioms of HA0.  I am wondering whether you can tell me anything
about the following sort of system in this regard.

Call Free Arithmetic (FA) the theory whose axioms are: (1) the non-logical
axioms of standard (Peano) arithmetic; (2) any sentence of the form:
(Ex)(x=Sn0); and (3) the axioms of free logic.  The change from classical
logic to free logic can be effected by replacing (x)(A(x)) -> A(t) with
(y)((x)A(x) -> A(y)).  This change has the result that one cannot prove
denotations for function symbols.  So, for instance, one cannot prove
(x)(Ey)(y = Sx) in free logic.  Moreover, in order to instantiate to a term,
one must already have the existence of the object in question.  This is the
rationale for the axioms of the form (Ex)(x = Sn0). Consider, then, then
system of arithmetic that results from replacing the classical axioms of the
propositional calculus in FA with intuitionistic axioms.  Call the resulting
system Intuitionistic Free Arithmetic (IFA).  IFA would thus stand to HA as
FA stands to Peano Arithmetic.  I have the following questions: (1) Is it
plausible (or perhaps known) that IFA has the existence property? (2) If it
has yet to be proven but is plausible to suppose that IFA has the existence
property, along which lines do you think a proof would proceed? (3) How
strong a system do you think would be needed in order to prove that IFA has
the existence property, if it does?  Of course, if IFA has the disjunction
property and your proof applies to IFA, then the answer to these question is
obvious.  So I suppose that one way of asking my question is: can your proof
be extended to IFA and can IFA be proven to have the disjunction property?
Thank you for your consideration of these questions.
 
 
Sincerely,  
 
Paul Studtmann