Intuitionistic existential instantiation and epsilon symbol

DOI10.1007/978-3-319-11041-7_9zbMATH Open1429.03057arXiv1208.0861OpenAlexW2963892445MaRDI QIDQ5213612FDOQ5213612

Authors: G. E. Mints 

Publication date: 4 February 2020

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

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.

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A short introduction to intuitionistic logic
• The Skolem method in intuitionistic calculi
• The Skolemization of existential quantifiers in intuitionistic logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Intuitionistic Predicate Calculus with ^|^epsilon;-Symbol
• A General Theory of Completeness Proofs
• Linear lambda-terms and natural deduction
• On axiomatizing fragments
• Title not available (Why is that?)

Cited In (3)

• Herbrand complexity and the epsilon calculus with equality
• Title not available (Why is that?)
• 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)