Proof-theoretic methods in quantifier-free definability

DOI10.1016/J.APAL.2025.103555MaRDI QIDQ7032975zbMATH OpenFDO

Authors Zoltan A. Kocsis

Publication date 4 February 2025

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

Full work available at URL https://doi.org/10.1016/J.APAL.2025.103555

zbMATH Keywords

connectivesintermediate logicsproof theorysecond-order propositional logictype theory

Mathematics Subject Classification ID

Higher-order logic (03B16) Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

Cites work

• A sheaf representation and duality for finitely presented Heyting algebras
• A small complete category
• A terminating sequent calculus for intuitionistic strong Löb logic with the subformula property
• Contraction-free sequent calculi for intuitionistic logic
• Convergence in formal topology: a unifying notion
• Dependently typed programming in Agda
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3726340 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512769 (Why is no real title available?)
• scientific article; zbMATH DE number 3349775 (Why is no real title available?)
• Interpolation properties of superintuitionistic logics
• Lectures on the Curry-Howard isomorphism
• Mechanised uniform interpolation for modal logics K, GL, and iSL
• On a second order propositional operator in intuitionistic logic
• On an interpretation of second order quantification in first order intuitionistic propositional logic
• On second order intuitionistic propositional logic without a universal quantifier
• On some new intuitionistic propositional connectives. I
• On the necessity of some topological spaces
• Pitts' quantifiers are not topological quantification
• Positive formulas in intuitionistic and minimal logic
• Propositional quantifiers
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• Strong completeness of S4 for any dense-in-itself metric space
• The existential fragment of second-order propositional intuitionistic logic is undecidable
• Undefinability of propositional quantifiers in the modal system S4
• Uniform interpolation and compact congruences
• Uniform interpolation and the existence of sequent calculi

This page was built for publication: Proof-theoretic methods in quantifier-free definability

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