The existence property in the presence of function symbols

Abstract

We are going to reconsider the existence property in intuitionistic first order logic (IQC) with function symbols, as presented in Dag Prawitz': "Natural Deduction, A Proof Theoretical Study." That is, we will examine its formulation, and try to give a constructive proof of the theorem. I mention in particular the function symbols in IQC, because their presence give rise to a new view on this property. Especially a tool from resolution in automated theorem proving (Gallier [2]) will be necessary for the tightening up of the property.,