The existence property in the presence of function symbols

authors	Doorman, M.
source	Logic Group Preprint Series, Volume: 41 (2008)
full text	[Full text]
document type	Preprint
disciplines	Wijsbegeerte
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.,