Normalization theorems for full first order classical natural deduction

DOI10.2307/2274910zbMath0735.03028OpenAlexW2143121603MaRDI QIDQ3981450

Gunnar Stålmarck

Publication date: 26 June 1992

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2274910

zbMATH Keywords

validitystrong normalization theoremfull first order classical natural deduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (16)

NORMAL DERIVABILITY IN CLASSICAL NATURAL DEDUCTION ⋮ Postponement of $\mathsf {raa}$ and Glivenko's theorem, revisited ⋮ Gentzen's Proof Systems: Byproducts in a Work of Genius ⋮ HARMONISING HARMONY ⋮ Bilateralism does not provide a proof theoretic treatment of classical logic (for technical reasons) ⋮ Unnamed Item ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ Full classical S5 in natural deduction with weak normalization ⋮ SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ Normality, non-contamination and logical depth in classical natural deduction ⋮ Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization ⋮ Intrinsic reasoning about functional programs. II: Unipolar induction and primitive-recursion ⋮ A new S4 classical modal logic in natural deduction ⋮ CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI ⋮ Peirce's rule in natural deduction.

Cites Work

• Unnamed Item
• On the proof theory of the intermediate logic MH
• Assumption Classes in Natural Deduction

This page was built for publication: Normalization theorems for full first order classical natural deduction