TY - JOUR

T1 - VARIANTS of KREISEL'S CONJECTURE on A NEW NOTION of PROVABILITY

AU - Santos, Paulo Guilherme

AU - Kahle, Reinhard

PY - 2021/12/2

Y1 - 2021/12/2

N2 - Kreisel's conjecture is the statement: if, for all n ∈ ℕ, PA ⊢ksteps φ(n), then PA ⊢ ∀x.φ(x). For a theory of arithmetic T, given a recursive function h, T ⊢≤h φ holds if there is a proof of φ in T whose code is at most h(#φ). This notion depends on the underlying coding. PhT(x) is a provability predicate for ⊢≤h in T. It is shown that there exists a sentence φ and a total recursive function h such that T ⊢≤h PrT(⌈PrT (⌈φ⌉) → φ⌉), but T ⊢/≤h φ, where PrTstands for the standard provability predicate in T. This statement is related to a conjecture by Montagna. Also variants and weakenings of Kreisel's conjecture are studied. By use of reexion principles, one can obtain a theory ThΓ that extends T such that a version of Kreisel's conjecture holds: given a recursive function h and φ(x) a Γ- formula (where Γ is an arbitrarily fixed class of formulas) such that, for all n ∈ N, T ⊢≤h φ(n), then ThΓ⊢ ∀x.φ(x). Derivability conditions are studied for a theory to statisfy the following implication: if T ⊢ ∀x.PhT(pφ(x)q), then T ⊢ ∀x.φ(x). This corresponds to an arithmetization of Kreisel's conjecture. It is shown that, for certain theories, there exists a function h such that ⊢k steps ⊆ ⊢≤h.

AB - Kreisel's conjecture is the statement: if, for all n ∈ ℕ, PA ⊢ksteps φ(n), then PA ⊢ ∀x.φ(x). For a theory of arithmetic T, given a recursive function h, T ⊢≤h φ holds if there is a proof of φ in T whose code is at most h(#φ). This notion depends on the underlying coding. PhT(x) is a provability predicate for ⊢≤h in T. It is shown that there exists a sentence φ and a total recursive function h such that T ⊢≤h PrT(⌈PrT (⌈φ⌉) → φ⌉), but T ⊢/≤h φ, where PrTstands for the standard provability predicate in T. This statement is related to a conjecture by Montagna. Also variants and weakenings of Kreisel's conjecture are studied. By use of reexion principles, one can obtain a theory ThΓ that extends T such that a version of Kreisel's conjecture holds: given a recursive function h and φ(x) a Γ- formula (where Γ is an arbitrarily fixed class of formulas) such that, for all n ∈ N, T ⊢≤h φ(n), then ThΓ⊢ ∀x.φ(x). Derivability conditions are studied for a theory to statisfy the following implication: if T ⊢ ∀x.PhT(pφ(x)q), then T ⊢ ∀x.φ(x). This corresponds to an arithmetization of Kreisel's conjecture. It is shown that, for certain theories, there exists a function h such that ⊢k steps ⊆ ⊢≤h.

UR - http://www.scopus.com/inward/record.url?scp=85120898148&partnerID=8YFLogxK

U2 - 10.1017/bsl.2021.68

DO - 10.1017/bsl.2021.68

M3 - Article

AN - SCOPUS:85120898148

JO - Bulletin of Symbolic Logic

JF - Bulletin of Symbolic Logic

SN - 1079-8986

ER -