arXiv · 1208.0861
Intuitionistic Existential Instantiation and Epsilon Symbol
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.
Explore related subjects
Keep this discovery
Grigori Mints. 2012-08-03. Intuitionistic Existential Instantiation and Epsilon Symbol. https://arxiv.org/abs/1208.0861
Cite the original work for its findings. Save a collection to share your selection of sources.