Intuitionistic Existential Instantiation and Epsilon Symbol
Grigori Mints

TL;DR
This paper introduces a natural deduction system for intuitionistic predicate logic incorporating Hilbert's epsilon symbol, extending existing systems, and provides completeness and normalization insights.
Contribution
It presents a conservative natural deduction system with epsilon, extending prior intuitionistic logic frameworks, and offers a completeness proof and discussion on normalization.
Findings
The system is conservative over standard intuitionistic predicate logic.
A completeness proof for Kripke semantics is provided.
An approach to normalization is sketched.
Abstract
A natural deduction system for intuitionistic predicate logic with existential \ instantiation rule presented here uses Hilbert's -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 -symbol due to A. Dragalin and Sh. Maehara.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
