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.
Abstract
We investigate the proof-theoretic structure of incorrect/incomplete proofs, that is, derivations containing syntactic errors or incomplete inferential steps that nonetheless preserve partial semantic validity. Building on Hilbert's epsilon calculus, we formalize how such derivations can be corrected through semantic projection and weakest preconditions, leading to valid Herbrand disjunctions. We show 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. This approach extends Hilbert's program beyond correctness, toward a logic of error and recovery. Moreover we show that the extended first epsilon theorem is false-tolerant.
The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse.
Melanie Taprogge, F. Blanqui, Alexander Steen· 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...
This paper provides an expository comparison of two foundational proof systems in classical propositional logic: Gentzen's sequent calculus and Beth's semantic tableaux. Gentzen's sequent calculus is presented as a rule-based system built upon the single axiom $\alpha \Rightarrow \alpha$, whose key feature — the subfor...
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
This paper bridges two distinct traditions – philosophy of mathematics and proof theory – to provide a formal framework for explanatory proofs in mathematics. We focus on explanatory proofs that uncover the grounds of mathematical theorems, and we formalize their structure using a new “axioms-as-rules” approach. Our...
Elaine Pimentel, F. Poggiolesi· Topoi· 0 citations
This work presents a proof extraction algorithm for versioned e-graphs, an extension of e-graphs that supports branching reasoning contexts and proof by cases and implements it in Vegie, a lightweight automated inductive theorem prover.
George Zakhour, J. Gabriele, Cesário et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
