相关论文: DRAFT: A Formally Verified Constructive Proof of t…

This article critically reappraises arguments in support of Cantor's theory of transfinite numbers. The following results are reported: i) Cantor's proofs of nondenumerability are refuted by analyzing the logical inconsistencies in…

The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs. Although the proof theory and metatheory of BI are…

The calculus of constructions (CC) is a core theory for dependently typed programming and higher-order constructive logic. Originally introduced in Coquand's 1985 thesis, CC has inspired 25 years of research in programming languages and…

In this Part I, we shall prove the consistency of arithmetic without complete induction from a point of view of strong negation, using its embedding to the tableau system $\bf SN$ of constructive arithmetic with strong negation without…

Cut-elimination is one of the most famous problems in proof theory, and it was defined and solved for first-order sequent calculus by Gentzen in his celebrated Hauptsatz. Ceres is a different cut-elimination algorithm for first- and…

The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the…

This is a companion to a paper by the authors entitled "G\"odel on deduction", which examined the links between some philosophical views ascribed to G\"odel and general proof theory. When writing that other paper, the authors were not…

Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each bound treated. The proof can be checked with a higher order…

For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of…

G\"odel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand…

We show that the classical interpretations of Tarski's inductive definitions actually allow us to define the satisfaction and truth of the quantified formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers…

Lorenzen's ``Algebraische und logistische Untersuchungen \"uber freie Verb\"ande'' appeared in 1951 in The Journal of Symbolic Logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof…

In "Cut Elimination for Gentzen's Sequent Calculus with Equality and Logic of Partial Terms" LNCS 7750,161-172(2013), we have shown that the cut rule is eliminable in two ground equational sequent calculi, to be denoted by EQ_M and EQ'. In…

In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic…

G{\"o}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of valid formula to the notion of provable formula.We survey a…

We present an extension to the $\mathtt{mathlib}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and…

The Collatz conjecture, which posits that any positive integer will eventually reach 1 through a specific iterative process, is a classic unsolved problem in mathematics. This research focuses on designing an efficient algorithm to compute…

In 1994 Jech gave a model theoretic proof of G\"odel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano…

For each positive integer $n$, function $f$, and point $x$, the 1998 conjecture by Ghinchev, Guerragio, and Rocca states that the existence of the $n$-th Peano derivative $f_{(n)}(x)$ is equivalent to the existence of all $n(n+1)/2$…

We present an alternative cyclic proof system for Peano arithmetic that could be simpler than the existing ones and well-adapted both for proof analysis and for automatizing inductive proof search. In addition, we will show how various…