Sep 2026· The Review of Symbolic Logic· pp. 1-27· 0 citations· 11 references
Abstract
This paper investigates the question: what is a formal logical proof (in general—as opposed to: what is a formal proof in this or that specific proof system)? I begin by setting out a core conception of formal proof and substantiating its designation as ‘core’. The heart of this conception is that there must be an effective or mechanical procedure for checking the correctness of a purported proof. I then consider a proposed strengthening of this conception—one that has become standard in the literature on propositional proof complexity—according to which the proof-checking procedure must be able to be carried out in polynomial time. I discuss a variety of arguments in favour of the strengthened conception—and reject them all. My conclusion is that, when it comes to analysing the very idea of formal logical proof, we have no good reason to move to the strengthened conception and should stick with the core conception.
Pistis is introduced, an agentic, oracle-guided proof search that produces formal Lean proofs that satisfy faithfulness conditions and can accept or refute natural language proofs written by humans or AI, demonstrating that faithful formalization is useful as a proof-checking tool.
Tadd Mao, Tianjun Zhong, Dhruva Arekar et al.· 1 citation
We present new proofs of weak normalization for intuitionistic and classical propositional logics (with the full set of operators -- falsum, implication, conjunction and disjunction). These proofs work with cuts rather than cut segments, and they provide explicit ``local''rules for determining whether to contract a who...
We introduce Type-6 logic, a variant of dynamic epistemic logic augmented with two operators (uncertainty and recurrence), designed to model the inferential dynamics of contemporary large language model (LLM) chain-of-thought (CoT) reasoning. Type-6 accounts for common LLM reasoning pathologies such as unlicensed revis...
An automated fact-checking system returns a label: the claim is true, or it is false. In many such systems the verdict remains the primary output. What is generally missing is a record of which document settled the question, of what would have had to be different for the verdict to change, or of whether the same claim,...
Nikolaos Kekatos, Theodoros Nestoridis, Charalampos Bratsas et al.· 0 citations
The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzm\"uller and Scott's Notes on G\"odel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nomin...
It is shown that the epsilon calculus provides a natural framework for analyzing tolerance of falsity in proofs and for identifying conditions under which an incorrect proof can be semantically repaired.
Matthias Baaz, Mariami Gamsakhurdia· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
