On the unity of logic

DOI10.1016/0168-0072(93)90093-SMaRDI QIDQ685059zbMATH OpenOpenAlexFDO

Authors Jean-Yves Girard

Publication date 22 September 1993

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(93)90093-s

zbMATH Keywords

classical logiccut-free Gentzen-type systemintuitionistic logiclinear logicpolarity

Mathematics Subject Classification ID

Classical first-order logic (03B10) Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50)

Review text

This is a drastic extension of the author's previous work [Math. Struct. Comput. Sci. 1, No. 3, 255-296 (1991; Zbl 0752.03027)]. A single cut-free Gentzen-type system unifying classical, intuitionistic and linear logic is devised. The list of rules takes four pages, but the system is not a mechanical mixture of known systems for sublogics. The unifying element is the translation of stronger systems into linear logic, which underlines the notion of polarity, but is not explicitly present in the system.

Recommendations

• Cut elimination for the unified logic
• UNIFICATION IN INTERMEDIATE LOGICS
• On the unification of classical, intuitionistic and affine logics
• A focused approach to combining logics
• A new deconstructive logic: linear logic

Cites work

• A new constructive logic: classic logic
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• Linear logic
• Some Syntactical Observations on Linear Logic

Cited in

(58)

• On the algebraic structure of declarative programming languages
• Focusing and polarization in linear, intuitionistic, and classical logics
• Classical logic, storage operators and second-order lambda-calculus
• Semantics of weakening and contraction
• On the linear decoration of intuitionistic derivations
• A general adequacy result for a linear functional language
• A new framework for declarative programming
• A linear logical framework
• Multi-focused proofs with different polarity assignments
• On the logic of unification
• Structural cut elimination. I: Intuitionistic and classical logic
• A sequent calculus for subtyping polymorphic types
• Petri nets, Horn programs, linear logic and vector games
• Multimodal linguistic inference
• The multiplicative-additive Lambek calculus with subexponential and bracket modalities
• From the universality of mathematical truth to the interoperability of proof systems
• A pure view of ecumenical modalities
• Cut elimination for the unified logic
• On the unity of duality
• Rewritings for polarized multiplicative and exponential proof structures
• Structural focalization
• Kripke semantics for the logic of problems and propositions
• Static typing for a substructural lambda calculus
• Propositional mixed logic: its syntax and semantics
• scientific article; zbMATH DE number 3966049 (Why is no real title available?)
• Information completeness in Nelson algebras of rough sets induced by quasiorders
• The Logic of Bunched Implications
• A new deconstructive logic: linear logic
• A linear/producer/consumer model of classical linear logic
• scientific article; zbMATH DE number 7439427 (Why is no real title available?)
• Dual-context calculi for modal logic
• Multimodal dependent type theory
• A logical analysis of the Anselm's \textit{Unum argumentum} (from \textit{Proslogion})
• On the unification of classical, intuitionistic and affine logics
• Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory
• The practice of logical frameworks
• Linear Logic Properly Displayed
• On the semantics of classical disjunction
• Subtractive logic
• Proof theory in the abstract
• An ecumenical notion of entailment
• LNL polycategories and doctrines of linear logic
• Asynchronous functional sessions: cyclic and concurrent
• Hypersequent calculi for intuitionistic logic with classical atoms
• A focused approach to combining logics
• Comparing session type systems derived from linear logic
• Forum: A multiple-conclusion specification logic
• On the logic of UNITY
• Categories for computation in context and unified logic
• Data layout from a type-theoretic perspective
• Meaningfulness and genericity in a subsuming framework (invited talk)
• Gödel's absolute proofs and Girard's ludics: mutual insights
• On combining intuitionistic and S4 modal logic
• Separability and harmony in ecumenical systems
• The quantum monadology
• Lambek calculus with banged atoms for parasitic gaps
• A proof-theoretic approach to the semantics of classical linear logic
• The unity of a Tractarian fact

This page was built for publication: On the unity of logic

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