SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS

DOI10.1017/S175502030999030XzbMath1204.03054MaRDI QIDQ3577741

Peter Milne

Publication date: 23 July 2010

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

zbMATH Keywords

natural deductionKripke modelsconservative extensionseparation propertysubformula propertyLindenbaum-Henkin constructionseparation of fragments

Mathematics Subject Classification ID

Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Classical propositional logic (03B05) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55)

Related Items

Normalisation and subformula property for a system of intuitionistic logic with general introduction and elimination rules, THE SUBFORMULA PROPERTY IN CLASSICAL NATURAL DEDUCTION ESTABLISHED CONSTRUCTIVELY, Inversion Principles and Introduction Rules, Constructive Modalities with Provability Smack, Normalisation and subformula property for a system of classical logic with Tarski's rule

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantical investigations in Heyting's intuitionistic logic
• Peirce's rule in natural deduction.
• Trees and finite satisfiability: proof of a conjecture of Burgess
• Independence of Tarski's law in Henkin's propositional fragments
• A propositional calculus intermediate between the minimal calculus and the classical
• A note on partial postulate sets for propositional logic
• On the proof theory of the intermediate logic MH
• Normalization theorems for full first order classical natural deduction
• A logic stronger than intuitionism
• The Demarcation Line Between Intuitionist Logic and Classical Logic
• On the strong semantical completeness of the intuitionistic predicate calculus
• The separation theorem of intuitionist propositional calculus