Short proofs for slow consistency

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)

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.

Recommendations

Cites work

Cited in

(7)

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)