Algebra of proofs

zbMath0532.03030MaRDI QIDQ788719

Manfred E. Szabo

Publication date: 1978

Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)

zbMATH Keywords

completenessproof theorycut-eliminationalgebraic modelfunctional description of quantifiersintuitionistic first-order logicLindenbaum-Tarski algebras

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Topoi (18B25) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Research exposition (monographs, survey articles) pertaining to category theory (18-02) Foundations, relations to logic and deductive systems (18A15)

Related Items

Proof of a S.Mac Lane conjecture (extended abstract) ⋮ A cut-free Gentzen-type system for the logic of the weak law of excluded middle ⋮ Coherence via focusing for symmetric skew monoidal categories ⋮ The linear abstract machine ⋮ Algebra of constructions. I. The word problem for partial algebras ⋮ A note on sequent calculi intermediate between LJ and LK ⋮ Proof of a conjecture of S. Mac Lane ⋮ Lambek vs. Lambek: functorial vector space semantics and string diagrams for Lambek calculus ⋮ On categorical equivalence of Gentzen-style derivations in IMLL ⋮ Kohaerenz in Kategorien mit Gruppenstruktur ⋮ Sequent calculus for classical logic probabilized ⋮ Reversible monadic computing ⋮ Monoidal logics: completeness and classical systems ⋮ Identity of Proofs Based on Normalization and Generality ⋮ Coherence in Cartesian closed categories and the generality of proofs ⋮ Multiplicative Linear Logics and Fibrations ⋮ Unnamed Item ⋮ A cut-elimination proof in intuitionistic predicate logic ⋮ Algebre categoriali ed equazioni flessibili (una generalizzazione dell’ algebra universale) ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction