Paper Info
Title
Intuitionistic Existential Instantiation and Epsilon Symbol
Abstract
A natural deduction system for intuitionistic predicate logic with existential instantiation rule presented here uses Hilbert's epsilon-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 epsilon-symbol due to Dragalin and Maehara.
Year
DOI
Venue
2012
10.1007/978-3-319-11041-7_9
Outstanding Contributions to Logic
Keywords
Field
DocType
Hilbert's epsilon-symbol,Intuitionistic predicate logic,Existential instantiation,Natural deduction,Sequent calculus
Existential instantiation,Discrete mathematics,Normalization (statistics),Kripke semantics,Symbol,Natural deduction,Predicate logic,Completeness (statistics),Mathematics,Sketch
Journal
Volume
ISSN
Citations 
7
2211-2766
0
PageRank 
References 
Authors
0.34
2
1
Name
Order
Citations
PageRank
Grigori Mints123572.76