TY - JOUR

T1 - A new perspective on completeness and finitist consistency

AU - Santos, Paulo Guilherme

AU - Sieg, Wilfried

AU - Kahle, Reinhard

N1 - info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00297%2F2020/PT#
info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDP%2F00297%2F2020/PT#
info:eu-repo/grantAgreement/FCT/OE/SFRH%2FBD%2F143756%2F2019/PT#
The third author was supported by the Udo Keller Foundation.
© The Author(s) 2023. Published by Oxford University Press.

PY - 2023/7/8

Y1 - 2023/7/8

N2 - In this paper, we study the metamathematics of consistent arithmetical theories T (containing IΣ1 ); we investigate numerical properties based on proof predicates that depend on numerations of the axioms. NUMERAL COMPLETENESS. For every true (in N ) sentence Q⃗ x⃗ .φ(x⃗ ) , with φ(x⃗ ) a Σ1(IΣ1) -formula, there is a numeration τ of the axioms of T such that IΣ1⊢Q⃗ x⃗ .Prτ(┌φ(x⃗ .)┐) , where Prτ is the provability predicate for the numeration τ . NUMERAL CONSISTENCY. If T is consistent, there is a Σ1(IΣ1) -numeration τ of the axioms of IΣ1 such that IΣ1⊢∀x.Prτ(┌¬Prf(┌⊥┐,x.)┐) , where Prf(x,y) denotes a Δ1(IΣ1) -definition of ‘y is a T -proof of x ’. Finitist consistency is addressed by generalizing a result of Artemov: PARTIAL FINITISM. If T is consistent, there is a primitive recursive function f such that, for all n∈N , f(n) is the code of an IΣ1 -proof of ¬Prf(┌⊥┐,n¯¯¯) . These results are not in conflict with Gödel’s Incompleteness Theorems. Rather, they allow to extend their usual interpretation and show a deep connection to reflections in Hilbert’s last papers of 1931.

AB - In this paper, we study the metamathematics of consistent arithmetical theories T (containing IΣ1 ); we investigate numerical properties based on proof predicates that depend on numerations of the axioms. NUMERAL COMPLETENESS. For every true (in N ) sentence Q⃗ x⃗ .φ(x⃗ ) , with φ(x⃗ ) a Σ1(IΣ1) -formula, there is a numeration τ of the axioms of T such that IΣ1⊢Q⃗ x⃗ .Prτ(┌φ(x⃗ .)┐) , where Prτ is the provability predicate for the numeration τ . NUMERAL CONSISTENCY. If T is consistent, there is a Σ1(IΣ1) -numeration τ of the axioms of IΣ1 such that IΣ1⊢∀x.Prτ(┌¬Prf(┌⊥┐,x.)┐) , where Prf(x,y) denotes a Δ1(IΣ1) -definition of ‘y is a T -proof of x ’. Finitist consistency is addressed by generalizing a result of Artemov: PARTIAL FINITISM. If T is consistent, there is a primitive recursive function f such that, for all n∈N , f(n) is the code of an IΣ1 -proof of ¬Prf(┌⊥┐,n¯¯¯) . These results are not in conflict with Gödel’s Incompleteness Theorems. Rather, they allow to extend their usual interpretation and show a deep connection to reflections in Hilbert’s last papers of 1931.

KW - Hilbert'sprogramme

KW - Finitistconsistency

KW - Metamathematics

KW - Numeralcompleteness

UR - https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=nova_api&SrcAuth=WosAPI&KeyUT=WOS:000988827100001&DestLinkType=FullRecord&DestApp=WOS

U2 - 10.1093/logcom/exad021

DO - 10.1093/logcom/exad021

M3 - Article

SN - 0955-792X

JO - Journal Of Logic And Computation

JF - Journal Of Logic And Computation

M1 - exad021

ER -