Existential instantiation and normalization in sequent natural deduction

DOI10.1016/0168-0072(92)90002-HzbMath0766.03032MaRDI QIDQ1198828

Carlo Cellucci

Publication date: 16 January 1993

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

sequent calculusnormalizationsubformula property\(\exists\)-elimination\(\lor\)-elimination\(\varepsilon\)-termsHerbrand theoremsmid-sequent theoremnegation rulevariants of natural deduction

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Natural deduction for intuitionistic linear logic, Harmony in multiple-conclusion natural-deduction, Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization, CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI, An alternative normalization of the implicative fragment of classical logic

Cites Work

• On sequence-conclusion natural deduction systems
• Heyting predicate calculus with epsilon symbol
• Remarks on descriptions and natural deduction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item