Normal derivability in classical natural deduction

DOI10.1017/S1755020311000311MaRDI QIDQ2890694zbMATH OpenFDO

Authors Jan von Plato, Annika Siders

Publication date 11 June 2012

Published in The Review of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S1755020311000311

zbMATH Keywords

proof theorynatural deductionnormalization

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

• Full classical S5 in natural deduction with weak normalization
• Normalization theorems for full first order classical natural deduction
• Normal derivability in modal logic
• A new S4 classical modal logic in natural deduction
• scientific article; zbMATH DE number 3275554

Cites work

• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A sequent calculus isomorphic to Gentzen's natural deduction
• Gentzen's proof systems: byproducts in a work of genius
• Natural deduction with general elimination rules
• Normal derivability in modal logic
• Normalization theorems for full first order classical natural deduction
• Proof Analysis

Cited in

(29)

• Subformula and separation properties in natural deduction via small Kripke models
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A normalization-procedure for the first order classical natural deduction with full logical symbols
• Normality, non-contamination and logical depth in classical natural deduction
• scientific article; zbMATH DE number 4068861 (Why is no real title available?)
• A new normalization strategy for the implicational fragment of classical propositional logic
• Proof-graphs: a thorough cycle treatment, normalization and subformula property
• Prawitz, Proofs, and Meaning
• scientific article; zbMATH DE number 3853043 (Why is no real title available?)
• An alternative normalization of the implicative fragment of classical logic
• Postponement of $\mathsf {raa}$ and Glivenko's theorem, revisited
• Normal natural deduction proofs (in classical logic)
• Peirce's rule in a full natural deduction system
• Peirce's rule in natural deduction.
• Cut for classical core logic
• Propositions in Prepositional Logic Provable Only by Indirect Proofs
• Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules
• A classical first-order normalization procedure with and based on the Milne-Kürbis approach
• Some formal considerations on Gabbay's restart rule in natural deduction and goal-directed reasoning
• Normal derivability in modal logic
• Natural deduction in normal modal logic
• Classical natural deduction
• scientific article; zbMATH DE number 1406467 (Why is no real title available?)
• Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization
• Gödel's modal interpretation of intuitionistic logic and its proof theory
• A new S4 classical modal logic in natural deduction
• Full classical S5 in natural deduction with weak normalization
• Unified natural deduction for logics of strong negation
• Two normalizations for naturald deductions in sequent style

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Normal derivability in classical natural deduction

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