Related papers: Consistency formula is strictly stronger in PA tha…

We offer a mathematical proof of consistency for Peano Arithmetic PA formalizable in PA. This result is compatible with Goedel's Second Incompleteness Theorem since our consistency proof does not rely on the representation of consistency as…

We describe a "slow" version of the hierarchy of uniform reflection principles over Peano Arithmetic ($\mathbf{PA}$). These principles are unprovable in Peano Arithmetic (even when extended by usual reflection principles of lower…

In much discussed work Artemov has recently shown that, for $\mathrm{PA}$, the consistency schema admits a form of uniform verification via selector proofs, despite the unprovability of the corresponding uniform consistency sentence…

Let $\operatorname{Con}(\mathbf T)\!\restriction\!x$ denote the finite consistency statement "there are no proofs of contradiction in $\mathbf T$ with $\leq x$ symbols". For a large class of natural theories $\mathbf T$, Pudl\'ak has shown…

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…

Non-compact proofs are a class of reasoning that is used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on proofs of arithmetical statements (*) "for any natural number n, F(n)." A proof of (*) is…

We study reflection principles of Peano Arithmetic PA which are based on both proof and provability. Any such reflection principle in PA is equivalent to either $\Box P\!\rightarrow\! P$ ($\Box P$ stands for `$P$ is provable') or $\Box^k…

Classical theory proves that every primitive recursive function is strongly representable in PA; that formal Peano Arithmetic, PA, and formal primitive recursive arithmetic, PRA, can both be interpreted in Zermelo-Fraenkel Set Theory, ZF;…

We show that it is provable in PA that there is an arithmetically definable sequence $\{\phi_{n}:n \in \omega\}$ of $\Pi^{0}_{2}$-sentences, such that - PRA+$\{\phi_{n}:n \in \omega\}$ is $\Pi^{0}_{2}$-sound and $\Pi^{0}_{1}$-complete - the…

In 2010, Vladimir Voevodsky gave a lecture on "What If Current Foundations of Mathematics Are Inconsistent?" Among other things he said that he was seriously suspicious that an inconsistency in PA (first-order Peano arithmetic) might…

The notion of slow provability for Peano Arithmetic ($\mathsf{PA}$) was introduced by S.D. Friedman, M. Rathjen, and A. Weiermann. They studied the slow consistency statement $\mathrm{Con}_{\mathsf{s}}$ that asserts that a contradiction is…

Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software where numbers are important. However, properties of the…

G\"odel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in…

It is generally accepted that the incompleteness of first-order number theory (PA) is established by an application of Godel's proof. This paper shows that the arithmetization of the syntax of PA implies that the hypothesised class of PA…

Based on the MRDP theorem concerning the Hilbert tenth problem, there is a corresponding Diophantine equation called proof equation for every formula of the First-order Peano Arithmetic (PA). A formula is provable in PA, if and only if the…

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…

We study when a sound arithmetic theory $\mathcal S{\supseteq}S^1_2$ with polynomial-time decidable axioms efficiently proves the bounded consistency statements $Con_{\mathcal S{+}\phi}(n)$ for a true sentence $\phi$. Equivalently, we ask…

We indicate that an argument of da Costa and Doria in fact proves P=NP. This observation makes their argument appear dubious. We isolate a weak version of one of their lemmas which would already prove P=NP. We point out that even this weak…

We present two new constructions of satisfaction/truth classes over models of PA (Peano Arithmetic) that provide a foil to the fact that the existence of a disjunctively correct full truth class over a model M of PA implies that Con(PA)…

Based on the MRDP theorem, we introduce the ideas of the proof equation of a formula and universal proof equation of Peano Arithmetic (PA); and then, combining universal proof equation and G\"odel's Second Incompleteness Theorem, it is…