Short proofs for slow consistency

DOI10.1215/00294527-2019-0031zbMATH Open1455.03078arXiv1712.03251OpenAlexW3104797474WikidataQ113751503 ScholiaQ113751503MaRDI QIDQ2176406FDOQ2176406

Fedor N. Pakhomov, Anton Freund

Publication date: 4 May 2020

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Abstract: Let

o p e r a t o r n a m e C o n (m a t h b f T)! e s t r i c t i o n! x

denote the finite consistency statement "there are no proofs of contradiction in

m a t h b f T

with

l e q x

symbols". For a large class of natural theories

m a t h b f T

, Pudl'ak has shown that the lengths of the shortest proofs of

o p e r a t o r n a m e C o n (m a t h b f T)! e s t r i c t i o n! n

in the theory

m a t h b f T

itself are bounded by a polynomial in

n

. At the same time he conjectures that

m a t h b f T

does not have polynomial proofs of the finite consistency statements

o p e r a t o r n a m e C o n (m a t h b f T + o p e r a t o r n a m e C o n (m a t h b f T))! e s t r i c t i o n! n

. In contrast we show that Peano arithmetic (

m a t h b f P A

) has polynomial proofs of

o p e r a t o r n a m e C o n (m a t h b f P A + o p e r a t o r n a m e {C o n}^{*} (m a t h b f P A))! e s t r i c t i o n! n

, where

o p e r a t o r n a m e {C o n}^{*} (m a t h b f P A)

is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen and Weiermann. We also obtain a new proof of the result that the usual consistency statement

o p e r a t o r n a m e C o n (m a t h b f P A)

is equivalent to

v a r e p s i l o n_{0}

iterations of slow consistency. Our argument is proof-theoretic, while previous investigations of slow consistency relied on non-standard models of arithmetic.

Full work available at URL: https://arxiv.org/abs/1712.03251

Recommendations

zbMATH Keywords

Peano arithmetic slow consistency consistency statements proof size fast-growing functions

Mathematics Subject Classification ID

Complexity of proofs (03F20) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40) Recursive functions and relations, subrecursive hierarchies (03D20) Recursive ordinals and ordinal notations (03F15)

Cites Work

Cited In (5)

This page was built for publication: Short proofs for slow consistency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2176406)