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

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

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