Intuitionistic Existential Instantiation and Epsilon Symbol
classification
🧮 math.LO
cs.LO
keywords
intuitionisticsymbolexistentialinstantiationlogicpredicateproofsystem
read the original abstract
A natural deduction system for intuitionistic predicate logic with existential \ instantiation rule presented here uses Hilbert's $\e$-symbol. It is conservative over intuitionistic predicate logic. We provide a completeness proof for a suitable Kripke semantics, sketch an approach to a normalization proof, survey related work and state some open problems. Our system extends intuitionistic systems with $\e$-symbol due to A. Dragalin and Sh. Maehara.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.