Normal derivability in classical natural deduction
The paper provides a normalization procedure for natural deduction systems for first-order intuitionistic, classical and some modal logics. The results are partly based on earlier works of von Plato and Negri. In contrast to other known methods, this procedure is based only on local permutation steps and does not require restrictions neither on the language of the system nor on the application of indirect proof or elimination rules. The system uses general elimination rules (with introduction of assumptions to be discharged instead of direct deduction from major premise) for all constants (not only for \(\vee \) and \(\exists \)) but it is shown that the procedure applies also to systems with standard elimination rules. Normal derivation is defined as the one where all major premises of elimination rules are assumptions. It is shown that all derivations in the considered systems convert into normal derivations, and that the latter satisfy the subformula property.NEWLINENEWLINEThe paper contains an interesting contribution to investigations on natural deduction but there is one drawback which needs to be noted. In the last section this result is extended to some system for modal logic which is called in the paper `classical modal logic'. This is misleading for two reasons. First, the name `classical' is sometimes applied to the weakest family of modal logics (instead of the name `congruent'); but the system presented in the paper certainly provides a formalization of some normal (hence much stronger) modal logic. Second, which logic is formalized by the rules depends on what we mean by `modal formulas' in the \(\square I\) rule. Following specific definitions of Prawitz we can obtain (due to \(\square E\)) either the system for S4 or for S5, but this is not stated in the text.
- A sequent calculus isomorphic to Gentzen's natural deduction
- Gentzen's proof systems: byproducts in a work of genius
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- Natural deduction with general elimination rules
- Normal derivability in modal logic
- Normalization theorems for full first order classical natural deduction
- Proof Analysis
- Normal natural deduction proofs (in classical logic)
- Peirce's rule in natural deduction.
- Natural deduction in normal modal logic
- A normalization-procedure for the first order classical natural deduction with full logical symbols
- Normality, non-contamination and logical depth in classical natural deduction
- An alternative normalization of the implicative fragment of classical logic
- Full classical S5 in natural deduction with weak normalization
- Postponement of $\mathsf {raa}$ and Glivenko's theorem, revisited
- Classical natural deduction
- Some formal considerations on Gabbay's restart rule in natural deduction and goal-directed reasoning
- Proof-graphs: a thorough cycle treatment, normalization and subformula property
- scientific article; zbMATH DE number 3853043 (Why is no real title available?)
- A new S4 classical modal logic in natural deduction
- Subformula and separation properties in natural deduction via small Kripke models
- Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization
- scientific article; zbMATH DE number 4068861 (Why is no real title available?)
- Propositions in Prepositional Logic Provable Only by Indirect Proofs
- scientific article; zbMATH DE number 1406467 (Why is no real title available?)
- Normal Gentzen deductions in the classical case
- Peirce's rule in a full natural deduction system
- Prawitz, Proofs, and Meaning
- Cut for classical core logic
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- Normal derivability in modal logic
- Two normalizations for naturald deductions in sequent style
- 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
- Gödel's modal interpretation of intuitionistic logic and its proof theory
- Unified natural deduction for logics of strong negation
- A new normalization strategy for the implicational fragment of classical propositional logic
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)
