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 -