A natural extension of natural deduction
From MaRDI portal
Publication:3691668
DOI10.2307/2274279zbMath0574.03045OpenAlexW2047063760MaRDI QIDQ3691668
Publication date: 1984
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.361.5791
Related Items (82)
Inductive families ⋮ Stabilizing quantum disjunction ⋮ The naturality of natural deduction ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ Calculi of epistemic grounding based on Prawitz's theory of grounds ⋮ THE RELEVANCE OF PREMISES TO CONCLUSIONS OF CORE PROOFS ⋮ Gentzen's Proof Systems: Byproducts in a Work of Genius ⋮ Logical connectives for constructive modal logic ⋮ HARMONISING HARMONY ⋮ European Summer Meeting of the Association for Symbolic Logic, (Logic Colloquium '87), Granada, Spain, 1987 ⋮ General-elimination harmony and the meaning of the logical constants ⋮ AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ ON FLATTENING ELIMINATION RULES ⋮ BILATERAL RELEVANT LOGIC ⋮ The categorical and the hypothetical: a critique of some fundamental assumptions of standard semantics ⋮ The placeholder view of assumptions and the Curry-Howard correspondence ⋮ Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach ⋮ Implications-as-rules vs. implications-as-links: an alternative implication-left schema for the sequent calculus ⋮ A SIMPLE SEQUENT SYSTEM FOR MINIMALLY INCONSISTENT LP ⋮ Sequent calculus in natural deduction style ⋮ WHAT IS A RULE OF INFERENCE? ⋮ On Inversion Principles ⋮ Proof-theoretic harmony: towards an intensional account ⋮ The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract) ⋮ Do-it-yourself type theory ⋮ Unnamed Item ⋮ A note on harmony ⋮ Focusing in Linear Meta-logic ⋮ Partial inductive definitions ⋮ Bilateralism in proof-theoretic semantics ⋮ Verificationism and Classical Realizability ⋮ Natural deduction bottom up ⋮ Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization ⋮ Proof-theoretic semantics and inquisitive logic ⋮ Proof Terms for Generalized Natural Deduction ⋮ On harmony and permuting conversions ⋮ General-elimination stability ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ WEAK DISHARMONY: SOME LESSONS FOR PROOF-THEORETIC SEMANTICS ⋮ Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different ⋮ The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony ⋮ HARMONIC INFERENTIALISM AND THE LOGIC OF IDENTITY ⋮ A framework for proof systems ⋮ Semantic values for natural deduction derivations ⋮ Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Proof, meaning and paradox: some remarks ⋮ Failure of completeness in proof-theoretic semantics ⋮ On reduction rules, meaning-as-use, and proof-theoretic semantics ⋮ PURE LOGIC OF ITERATED FULL GROUND ⋮ Functional completeness for subsystems of intuitionistic propositional logic ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Prawitz, Proofs, and Meaning ⋮ Inversion Principles and Introduction Rules ⋮ Meaning in Use ⋮ General-Elimination Harmony and Higher-Level Rules ⋮ Hypothesis-Discharging Rules in Atomic Bases ⋮ Harmony in Proof-Theoretic Semantics: A Reductive Analysis ⋮ Paradox and Inconsistency: Revising Tennant’s Distinction Through Schroeder-Heister’s Assumption Rules ⋮ A new connective in natural deduction, and its application to quantum computing ⋮ Unnamed Item ⋮ Classical harmony and separability ⋮ Deriving Natural Deduction Rules from Truth Tables ⋮ On the strength of dependent products in the type theory of Martin-Löf ⋮ INVERSION BY DEFINITIONAL REFLECTION AND THE ADMISSIBILITY OF LOGICAL RULES ⋮ The foundation of a generic theorem prover ⋮ The normalization theorem for extended natural deduction ⋮ Full Lambek Calculus in natural deduction ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic ⋮ Non-reflexivity and revenge ⋮ Does the Implication Elimination Rule Need a Minor Premise? ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ A Poly-Connexive Logic ⋮ \(\pi\)-calculus in (Co)inductive-type theory ⋮ Definite Descriptions in Intuitionist Positive Free Logic ⋮ ON THE NOTION OF CANONICAL DERIVATIONS FROM OPEN ASSUMPTIONS AND ITS ROLE IN PROOF-THEORETIC SEMANTICS ⋮ Simple consequence relations ⋮ CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI ⋮ Varieties of linear calculi ⋮ Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
Cites Work
This page was built for publication: A natural extension of natural deduction
