Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the arithmetization of syntax

Stephen Boyce

TL;DR

By re-examining Gödel's arithmetization within $PA$ and a converse of the Hilbert-Bernays Derivability Condition, the paper shows that the standard incompleteness argument can imply that the class of theorems in $PA$ is not well defined. The analysis relies on Mendelson's framing and introduces a novel demonstration that theoremhood can be inferred from proving that there exists a Gödel-numbered proof. It discusses the tension between metamathematics and Principia-type type theory, arguing that arithmetization depends on a metatheoretical framework that can be blocked, challenging the coherence of classical arithmetic foundations. Overall, the work invites a reconsideration of formal foundations and the reliability of metamathematical accounts of arithmetic.

Abstract

It is generally accepted that Godel's proof implies the incompleteness of first-order number theory. This paper shows that the standard demonstration of this result implies that the class of theorems of such systems is not well defined. Proof of the converse of one of the Hilbert-Bernays Derivability Conditions for Godel's second incompleteness theorem essentially yields this result: the theoremhood of a formula is implied if it may be proven in the system that there exists a Godel number of a proof of the formula.

On the arithmetization of syntax

TL;DR

By re-examining Gödel's arithmetization within and a converse of the Hilbert-Bernays Derivability Condition, the paper shows that the standard incompleteness argument can imply that the class of theorems in is not well defined. The analysis relies on Mendelson's framing and introduces a novel demonstration that theoremhood can be inferred from proving that there exists a Gödel-numbered proof. It discusses the tension between metamathematics and Principia-type type theory, arguing that arithmetization depends on a metatheoretical framework that can be blocked, challenging the coherence of classical arithmetic foundations. Overall, the work invites a reconsideration of formal foundations and the reliability of metamathematical accounts of arithmetic.

Abstract

It is generally accepted that Godel's proof implies the incompleteness of first-order number theory. This paper shows that the standard demonstration of this result implies that the class of theorems of such systems is not well defined. Proof of the converse of one of the Hilbert-Bernays Derivability Conditions for Godel's second incompleteness theorem essentially yields this result: the theoremhood of a formula is implied if it may be proven in the system that there exists a Godel number of a proof of the formula.

Paper Structure

This paper contains 8 sections, 10 theorems, 4 equations.

Table of Contents

  1. Introduction
  2. An informal sketch
  3. The failure of the metamathematical notion of proof
  4. Notation and symbolism
  5. Results taken from the existing literature
  6. A novel demonstration
  7. Discussion
  8. Conclusion

Key Result

Proposition 3.1

Every $PA$ formula that is an instance of a tautology is a $PA$ theorem which may be proven on the basis of logical axioms and inference rules alone. (cf. mendelson2015 Proposition 2.1 paraphrase).

Theorems & Definitions (13)

  • Proposition 3.1
  • Proposition 3.2
  • Definition 3.3
  • Proposition 3.4
  • Proposition 3.5
  • Corollary 3.6
  • Proposition 3.7
  • Proposition 3.8
  • Proposition 3.9
  • Proposition 3.10
  • ...and 3 more