Intuitionistic existential instantiation and epsilon symbol

DOI10.1007/978-3-319-11041-7_9MaRDI QIDQ5213612zbMATH OpenOpenAlexFDO

Authors G. E. Mints

Publication date 4 February 2020

Published in Dag Prawitz on Proofs and Meaning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1208.0861

zbMATH Keywords

natural deductionsequent calculusintuitionistic predicate logicexistential instantiationHilbert's \(\epsilon\)-symbol

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20) Structure of proofs (03F07)

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.

Recommendations

• Hilbert's ϵ‐operator in intuitionistic type theories
• scientific article; zbMATH DE number 3557745
• Existential instantiation and normalization in sequent natural deduction
• On the proof theory of the existence predicate
• Intuitionistic ϵ‐ and τ‐calculi

Cites work

• scientific article; zbMATH DE number 48365 (Why is no real title available?)
• scientific article; zbMATH DE number 3508471 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3296224 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• scientific article; zbMATH DE number 3411008 (Why is no real title available?)
• A General Theory of Completeness Proofs
• A short introduction to intuitionistic logic
• Intuitionistic Predicate Calculus with ^|^epsilon;-Symbol
• Linear lambda-terms and natural deduction
• On axiomatizing fragments
• The Skolem method in intuitionistic calculi
• The Skolemization of existential quantifiers in intuitionistic logic

Cited in

(3)

• Herbrand complexity and the epsilon calculus with equality
• scientific article; zbMATH DE number 3557745 (Why is no real title available?)
• On the proof theory of the existence predicate

This page was built for publication: Intuitionistic existential instantiation and epsilon symbol

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5213612)