A new perspective on completeness and finitist consistency

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Article numberexad021
Number of pages20
JournalJournal Of Logic And Computation
Early online date24 Apr 2023
DOIs
Publication statusPublished - 8 Jul 2023

Keywords

  • Hilbert'sprogramme
  • Finitistconsistency
  • Metamathematics
  • Numeralcompleteness

Fingerprint

Dive into the research topics of 'A new perspective on completeness and finitist consistency'. Together they form a unique fingerprint.

Cite this