GEOMETRISATION OF FIRST-ORDER LOGIC

DOI10.1017/bsl.2015.7zbMath1368.03013OpenAlexW2216255786MaRDI QIDQ2795295

Roy Dyckhoff, Sara Negri

Publication date: 18 March 2016

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

Full work available at URL: http://hdl.handle.net/10023/6818

zbMATH Keywords

conservative extensiongeometric logiccoherent logiccoherent implicationweakly positive formula

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Classical first-order logic (03B10) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Basic properties of first-order languages and structures (03C07)

Related Items

From axioms to synthetic inference rules via focusing ⋮ Invited Talk: Coherentisation of First-Order Logic ⋮ A theory of duality in Euclidean geometry ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Formalizing Kant's rules. A logic of conditional imperatives and permissives ⋮ Automated generation of illustrated proofs in geometry and beyond ⋮ The intensional side of algebraic-topological representation theorems ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ On Relating Theories: Proof-Theoretical Reduction ⋮ From mathematical axioms to mathematical rules of proof: recent developments in proof analysis ⋮ Multicomponent proof-theoretic method for proving interpolation properties ⋮ PROOF ANALYSIS FOR LEWIS COUNTERFACTUALS ⋮ Proof-theoretic analysis of the logics of agency: the deliberative STIT ⋮ Inducing Syntactic Cut-Elimination for Indexed Nested Sequents ⋮ Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi ⋮ Theorem proving as constraint solving with coherent logic ⋮ Geometric Rules in Infinitary Logic

Uses Software

• ArgoCLP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof analysis in intermediate logics
• Proof analysis in modal logic
• Toposes without points
• Gentzen-type systems, resolution and tableaux
• Contraction-free sequent calculi for geometric theories with an application to Barr's theorem
• Proofs and countermodels in non-classical logics
• The Church-Fitch knowability paradox in the light of structural proof theory
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• Contraction-free sequent calculi for intuitionistic logic
• An Intuitionistic Axiomatisation of Real Closed Fields
• A Systematic Presentation of Quantified Modal Logics
• Aspects of topoi
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS

This page was built for publication: GEOMETRISATION OF FIRST-ORDER LOGIC