PaperlayerView exact revision on arXiv

Source-linked AI summary

Inductive Grounded Arithmetic: Goodstein, the Hydra, and $\Gamma_0$

Bryan Ford

arXiv:2610.34548v1math.LOcs.LOcs.PL

TL;DR

Grounded arithmetic needs a way to reason about recursive definitions when sentences may have no truth value. The paper adds ground induction for positive self-referential terms, then proves results about games, ordinal notations, and truth while characterizing the boundary around Γ0.

  • Problem

    RGA can express recursive definitions as self-referential terms but cannot use their least-fixed-point character to prove properties of all members.

    Source: §1 · p. 1

  • Method

    IGA adds ground induction for positive self-referential terms, applying a closure argument over one unfolding to establish a motive at a member.

    Source: §4.1 · p. 6

  • Results

    IGA proves Goodstein’s theorem and the Kirby–Paris hydra game for primitive recursive strategies, and proves the Veblen notation well-founded exactly when it admits bivalence of accessibility for that order.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The rule supports grounded proofs of game results and ordinal claims, including well-foundedness of ε0 Cantor-normal-form codes and certification of Veblen notations below each φ(n, 0).

    Source: §1 · p. 2

    The hydra result covers primitive recursive strategies, not all computable strategies; extending it would require a universal over partial computations with a totality guard.

    Source: §6.2 · p. 11

Abstract

from arXiv · show

What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard $\varepsilon_0$ notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every $\varphi(n,0)$. It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so $\Gamma_0$ lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's $\mathcal O$ are interderivable over IGA.

1 Introduction

RGA can express recursive definitions as self-referential terms but cannot use their least-fixed-point character; IGA adds ground induction for positive definitions. The paper tests what this rule proves and where its limits lie.

1 Introduction

  • The motivating gap is that RGA can write winning positions as a self-referential term but cannot infer properties of all winning positions from it.IGA adds the elimination rule for positive self-referential terms, called ground induction, and machine-checked results establish its omega-model soundness and consistency.Source: §1 · pp. 1–2
  • IGA proves well-foundedness of Cantor-normal-form codes for ε0 and certifies the Veblen notations below each φ(n, 0).Soundness transfers the internal ε0 result to HOL’s standard ε0 notation system.Source: §1 · p. 2
  • IGA proves Goodstein’s theorem outright and the Kirby–Paris hydra game for every primitive recursive strategy, with each arithmetic step a grounded derivation.The hydra result concerns strategies given by primitive-recursive codes.Source: §1 · p. 2
  • Kripke truth for RGA’s own language is defined as one positive fixed point that agrees exactly with the omega model.The truth term has an induction principle, clause laws and their inversions, and an internal refutation of truth at 0 = 1.Source: §1 · p. 2
  • IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order; whether IGA proves it remains open.Bivalence of accessibility is sound exactly when the order is well-founded, and the corresponding rule, well-foundedness sentence, and a Kleene O membership claim are interderivable over IGA.Source: §1 · p. 2
  • The paper distinguishes grounded derivations in RGA or IGA from classical HOL claims about the systems or their omega model.Soundness connects the two kinds of claim in one direction only.Source: §1 · pp. 2–3

2 Background: Reflective Grounded Arithmetic

RGA treats terms as computations and logical statements as values reached by those computations. Its self-reference and omega-model semantics provide the background for IGA’s added induction principle.

2 Background: Reflective Grounded Arithmetic

  • A closed RGA term may reach a numeral or run forever; terms without values are neither true nor false.The logical values 0 and 1 govern equality, negation, disjunction, and universal statements.Source: §2 · p. 3
  • RGA’s judgments distinguish truth, reaching a numeral, and being decided, while universal introduction requires one schematic argument for every instance.Primitive-recursive functions are represented by index trees and compiled to terms that RGA proves total.Source: §2 · p. 3
  • RGA’s fixed-point former builds self-referential terms, including the Liar, which RGA proves neither true nor false.A well-formed sentence with no value is independent: neither provable nor refutable.Source: §2 · pp. 3–4
  • RGA’s omega model makes a universal true when every instance is true, while certificate-grounded truth also requires a schematic proof.RGA is sound and complete for the certificate-grounded semantics and sound for the omega model; the latter is infinitary and can make noncomputable sets true.Source: §2 · p. 4
  • RGA has no induction principle for self-referential terms and no deduction theorem at an undecided hypothesis.Its deduction theorem holds at a hypothesis only when that hypothesis is provably decided; supplying self-reference induction is IGA’s addition.Source: §2 · p. 4

3 Positive Self-Reference

IGA’s ground-induction rule applies to self-referential terms whose recursive variable occurs positively. The grammar also restricts how that variable may be applied, preserving the soundness argument.

3 Positive Self-Reference

  • Positivity is required because only positive bodies make the oracle reading describe the term’s truth, not because their induced operators are monotone.The operator is monotone even for the Liar body, whose least fixed point is empty.Source: §3 · pp. 4–5
  • The grammar tracks positive and negative occurrences through negation, disjunction, and universal quantification; an atom under an even number of negations is positive.It admits the accessibility and winning-position bodies but excludes the Liar body.Source: §3 · p. 5
  • The recursive atom’s argument must be a numeral expression in bound variables, not an arbitrary computed term or parameter.A divergent argument could make the fixed point true while the rule’s closure premise ranges only over numerals; a separate evaluation in the soundness proof also creates an unresolved obstacle.Source: §3 · p. 5
  • Computed arguments are routed through a quantifier with a decided equality guard, allowing the recursive atom to apply to a bound variable.The truth predicate uses the existential form, and this routing costs additional binders.Source: §3 · p. 5
  • Positivity lets the oracle reading of a body agree with the term reading at the fixed point because truth does not depend on recursive atoms’ falsity or lack of value.This is the point where positivity enters the semantics.Source: §3 · pp. 4–5
  • Substitution preserves positivity for numeral expressions and lifting, but not for arbitrary terms substituted for other indices.The parameterized grammar does remain stable under substituting terms for parameters.Source: §3 · p. 6

4 Ground Induction

Ground induction lets IGA reason from membership in a positive fixed point to properties closed under one unfolding. The section illustrates the rule, establishes soundness and consistency, and identifies positive fixed points with least fixed points.

4 Ground Induction

  • Ground induction is the elimination rule for a positive self-referential term, and its intended meaning is induction over that term’s least fixed point.The rule and its soundness and consistency are established in the section.Source: §4 · p. 6

4.1 The rule

  • From membership at a number and a closure derivation at a fresh point, the rule concludes that the motive holds at that number.The rule requires the point to be a number; without that premise it would be unsound for the omega model.Source: §4.1 · p. 6

4.2 A worked example: the subtraction game

  • In the subtraction game, ground induction proves that every provably winning position is nonzero; soundness separately yields that IGA proves a position winning exactly when it is odd.The odd-position result itself follows by number induction and unfolding, without ground induction.Source: §4.2 · p. 7

4.3 Soundness and consistency

  • IGA is sound for the omega model and therefore does not prove 0 = 1.The omega model is used because its soundness proof does not depend on certificates for the extended system’s proofs.Source: §4.3 · p. 7

4.4 A positive fixed point is an inductive definition

  • For every positive body, the numbers where its fixed-point term is omega-true are exactly the least fixed point of its operator.Thus ground induction is the induction principle for the positive fixed point; accessibility and winning positions are examples of these denotations.Source: §4.4 · p. 8
  • Positive fixed points add an induction principle, not a larger class of definable truth sets than arbitrary closed terms.The paper states that these truth sets form exactly the Π1 1 sets by a classical argument using cited theorems, not a formalized argument in this development.Source: §4.4 · p. 8

5 Well-Foundedness as a Sentence

The paper represents well-foundedness as a sentence about accessibility, a positive recursive definition. Ground induction lets IGA prove well-foundedness for orders beyond RGA’s reach, including Cantor-normal-form codes and Veblen segments below each φ(n, 0).

5 Well-Foundedness as a Sentence

  • Well-foundedness is one closed sentence asserting accessibility, making ordinal claims expressible in grounded arithmetic.The paper contrasts this with the classical Π1 1 formulation, which quantifies over all sets of numbers.Source: §5 · p. 8

5.1 Accessibility and the certificate

  • Accessibility is true in the omega model exactly on the HOL-accessible part of the not-refuted relation, and it is never false.Consequently, well-foundedness is never refutable; if IGA proves it, the not-refuted relation on the domain is well-founded in HOL.Source: §5.1 · p. 9

5.2 What RGA alone can prove

  • RGA proves well-foundedness of the naturals and every finite tower, but its induction schema stops at ωω.At a limit, the required induction hypothesis concerns an open tower height, while RGA can only unfold accessibility one step.Source: §5.2 · p. 9

5.3 What IGA proves

  • Ground induction lets IGA prove well-foundedness for the tower family and Cantor-normal-form codes, including a transfer from WF(R) to WF(ωR).The Cantor-normal-form proof uses nested rank and accessibility inductions; the transfer is a hypothetical derivation from the well-foundedness premise.Source: §5.3 · pp. 9–10

5.4 The notation certified, and HOL’s ε0 as a corollary

  • On canonical codes, IGA proves Veblen segments below every φ(n, 0) well-founded, and the ε0 notation’s HOL well-foundedness follows through soundness.The certification reaches at least φ(ω, 0); arbitrary codes need not be trichotomous, and no upper bound on IGA’s strength is claimed.Source: §5.4 · p. 10

6 Goodstein’s Theorem and the Hydra Game

Goodstein’s theorem and the Kirby–Paris hydra game are proved outright in IGA, using grounded derivations rather than an added transfinite-induction schema. The hydra result covers primitive recursive strategies, while the classical all-strategies statement is separately given in HOL.

6 Goodstein’s Theorem and the Hydra Game

  • IGA proves Goodstein’s theorem outright, with every arithmetic step a grounded derivation despite lacking implication at undecided hypotheses.The classical motivation is that Goodstein’s theorem and the hydra game are true but unprovable in Peano Arithmetic.Source: §6 · pp. 10–11

6.1 Goodstein’s theorem

  • Every Goodstein sequence reaches zero: IGA derives the ordinal-decrease lemma and then proves the closed theorem without hypotheses.The proof uses ground induction along ε0; its decrease lemma is derived through an internal theory of hereditary base representations.Source: §6.1 · p. 11

6.2 The hydra game

  • For every primitive recursive strategy, IGA proves outright that the hydra battle terminates, using a strategy-specific ordinal-decrease lemma.The grounded theorem quantifies over coded primitive recursive strategies, not all functions; the latter classical form is stated in HOL.Source: §6.2 · pp. 11–12

7 Truth as a Fixed Point

The paper defines truth for RGA’s own language as one positive fixed point, with ground induction supplying its minimality principle. The fixed point matches the omega model exactly, and the system proves that 0 = 1 is not true.

7 Truth as a Fixed Point

  • Truth for RGA’s language is one positive fixed point, and ground induction serves as its minimality principle.This brings the Kripke fixed-point construction into IGA without separate truth axioms.Source: §7 · p. 12

7.1 The omega model internalized

  • The truth term internalizes the omega model’s evaluation rules and agrees with it exactly for value and head-form points.Its points encode a tag, a term code, and a result; the term applies to codes of arbitrary terms, including its own applications.Source: §7.1 · p. 12

7.2 Clause laws, inversions, and the refutation

  • RGA proves the truth term refuted at 0 = 1, using negative unfolding rather than ground induction.Ground induction is the truth term’s induction principle, but the clause laws, inversions, and this refutation are RGA theorems.Source: §7.2 · p. 13

7.3 What the truth term does and does not give

  • The truth term supports uniform reasoning about the base language’s semantics, but does not give IGA a proof of RGA’s consistency by the obvious route.The paper also notes that determinacy of the truth term’s values inside IGA depends on an undischarged closure obligation.Source: §7.3 · p. 13

8 The Price of the Classical World

Section 8 identifies the gap between IGA’s finite Veblen results and the whole Veblen notation with bivalence at an undecided accessibility hypothesis. It also delineates limits on conditional proof and internal soundness arguments.

8.1 Well-foundedness of the Veblen notation, exactly

  • IGA proves the Veblen notation well-founded exactly when it admits bivalence of accessibility for that order; whether it proves either remains open.By the deduction theorem, this is equivalent to proving excluded middle for the accessibility predicate.Source: §8.1 · p. 14

8.2 What bivalence costs

  • Bivalence of accessibility for a closed order is sound for the omega model exactly when the order is well-founded in HOL.At an inaccessible point, applying the rule to accessibility itself would derive excluded middle for a claim that is neither true nor false.Source: §8.2 · p. 14

8.3 One rule, or one claim

  • The Veblen well-foundedness commitment is interderivable as a rule, a sentence, or the claim that a specific code is a notation in Kleene’s O.Adding the rule yields a sound and consistent extension; the claim-form derivation uses induction along O and ground induction, not Veblen-order induction.Source: §8.3 · p. 15

8.4 Where the lower bound sits

  • The proved route reaches φ(n, 0) for every finite n, while its lower bound is likely sharp and IGA’s upper bound is unknown.The text places this lower bound below the cited Kripke–Feferman and PKF strength calibrations.Source: §8.4 · p. 15

8.5 Conditional proof is inconsistent

  • Any term former over RGA’s terms that supports modus ponens and conditional proof at arbitrary hypotheses derives 0 = 1.The Curry fixed point supplies the contradiction; separately, admitting the bivalence rule with the Liar in place of accessibility also yields 0 = 1.Source: §8.5 · p. 16

8.6 No internal soundness proof of RGA

  • The internal-soundness argument for RGA’s consistency is unavailable in the analyzed form: its motive and weaker variants are underivable in IGA at a specified hypothesis node.The result covers that argument and its weakenings, not every conceivable internal argument.Source: §8.6 · p. 16

9 Related Work

The related work situates IGA among theories of truth, inductive definitions, ordinal analysis, and grounded arithmetic. It distinguishes the paper’s grounded proofs from prior mechanizations in assistants’ classical or constructive logics.

Theories of truth

  • Kripke’s fixed-point construction supplies the semantics, while Cantini’s minimality principle is the truth-predicate induction schema generalized by ground induction.The discussion also compares IGA’s truth term with paracomplete axiomatizations and the cost analyses of Halbach and Horsten.Source: §9 · p. 17

Inductive definitions and fixed-point induction

  • Park’s fixed-point induction, the µ-calculus, and proof assistants’ positivity-based inductive definitions are identified as close forms of the paper’s central idea.Earlier hydra and ordinal mechanizations establish results in the assistant’s own logic; here the assistant checks proofs in a weaker object system.Source: §9 · p. 17

Ordinals and predicativity

  • Feferman–Schütte progressions and Kreisel’s analyses place Γ0 at the limit of predicativity, while reverse-mathematical equivalences offer measures for well-foundedness transfers.Gentzen’s consistency proof is presented as the route left open by the no-go result.Source: §9 · p. 17

The grounded family

  • RGA [19] is the base system, OGA [20] adds decidedness for arithmetic sentences, and whether either extension contains the other remains open.The Gödel companion paper [21] supplies deduction and internal-soundness results reused here.Source: §9 · p. 17

10 Conclusion and Open Questions

The conclusion recaps IGA’s inductive-definition results and locates its current boundaries. It lists open questions about strength, generality, and consistency, and reports the mechanized artifact.

Conclusion

  • IGA’s limits include an open Γ0 well-foundedness commitment, inconsistency of conditional proof at arbitrary hypotheses, and an unavailable analyzed internal-soundness route to RGA consistency.The paper also states that bivalence is sound exactly when the order is well-founded and that the Γ0 commitment has rule, sentence, and Kleene O claim forms.Source: §10 · p. 18

Strength

  • Whether φ(ω, 0) is sharp, IGA’s proof-theoretic ordinal, and whether PKF interprets into IGA remain open questions.The section also asks how the grounded reflection rule relates to induction on an ordinal measure.Source: §10 · p. 18

Generality

  • Ground induction is currently restricted to unary bodies with numeral-expression atoms; mutual recursion and broader argument forms are identified as extensions or open questions.Determinacy of the truth term’s values in IGA is also open.Source: §10 · p. 18

Consistency

  • The paper conjectures that no consistent grounded extension proves RGA consistency by internal soundness, while Gentzen’s alternative requires finding an ordinal assignment to RGA proofs.Theorem 8.5 settles the conditional-proof-with-contraction case, but the remaining conditional possibilities are not settled.Source: §10 · p. 18

Artifact

  • Every theorem is checked in Isabelle/HOL, and the IGA, Combined, and IGA_NoGo sessions are released at project tag iga-2026-10-25.The appendices list theorem statements, definitions, proof steps, and lemmas for readers seeking to re-mechanize the proofs.Source: §10 · pp. 18–19

Appendices: the headline proofs in detail

The appendices provide mechanization-oriented accounts of the headline proofs and a shared vocabulary for reading their Isabelle sources.

Appendices: the headline proofs in detail

  • The seven appendices give theorem statements with hypotheses, supporting definitions, numbered proof steps, induction motives, and lemmas useful for re-mechanization.They target competent Masters or early PhD readers without logic expertise and use Isabelle names that can be located in the sources.Source: Appendices: the headline proofs in… · p. 22
  • The common vocabulary explains source terms, substitutions, omega-truth, value congruence, head reduction, and the omega model’s mutually inductive head-form and value relations.It also clarifies that soundness ranges over substitutions because derivations may contain open hypotheses and conclusions.Source: Appendices: the headline proofs in… · p. 22

A The soundness case of ground induction

Ground induction is sound for the omega model: its new proof case transports the fixed-point premise and closure premise to the motive, and the system is consistent. The transport argument also yields set and term induction forms, including a parametric form without a closedness requirement.

A The soundness case of ground induction

  • The transport lemma proves that a positive fixed-point term’s omega-value judgments preserve a five-part motive, using shape analysis across applications, connectives, quantifiers, and beta reduction.Its application case uses the closure condition to transfer truth of the unfolded body to membership in the set.Source: A The soundness case of ground induction · pp. 22–23
  • The set form says omega-truth of the fixed-point term implies membership in any set closed under its positive body; the term form follows by taking the truth set of the target term.For the term form, oracle reading is converted to term truth, then the stated hypothesis discharges the closure obligation.Source: A The soundness case of ground induction · pp. 23–24
  • The parametric transport, set, and term forms require no closedness hypothesis because the parametric grammar constrains atom arguments to bound variables.The ordinary proof uses closedness only in the application case; the parametric version replaces that condition with bound-variable admissibility.Source: A The soundness case of ground induction · pp. 23–24
  • The soundness theorem implies consistency because 0 = 1 is not true in the omega model.The result is stated as non-derivability of 0 = 1 from the empty context.Source: A The soundness case of ground induction · pp. 23, 25
  • Omega soundness handles ground induction by instantiating its premises at a numeral and using the induction hypothesis on the closure premise to establish the motive.The proof proceeds by induction on derivations; the forty-two RGA cases replay, while ground induction is the new case.Source: A The soundness case of ground induction · pp. 24–25

B The characterization theorem

The truth set of a positive fixed-point term is characterized as the least fixed point of its associated operator, and the same characterization connects accessibility and winning positions to their inductive definitions. The paper also proves the Cantor-normal-form code order well-founded in IGA, yielding HOL’s well-foundedness result for the standard ε0 notation system.

B The characterization theorem

  • For a positive body with a closed abstraction, the omega-truth set of its fixed-point term equals the least fixed point of the associated operator.The proof establishes both inclusions: the truth set is a pre-fixed point, and ground induction gives the reverse inclusion using positivity and closedness.Source: B The characterization theorem · pp. 25–26
  • The same least-fixed-point characterization identifies the truth sets of accessibility and winning-position terms with the corresponding inductively defined sets.For accessibility, the least fixed point is HOL’s accessible part; for winning positions, it is HOL’s inductively defined winning set.Source: B The characterization theorem · p. 26

C Well-foundedness of the Cantor-normal-form order

  • The internal well-foundedness theorem for the Cantor-normal-form order yields HOL’s well-foundedness theorem for the standard ε0 notation system through soundness.The mechanized results are identified as gi_WF_cnf, gi_WF_epsilon0, and epsilon0_wf.Source: C Well-foundedness of the… · p. 26
  • IGA proves the Cantor-normal-form code order well-founded, using nested rank induction and ground induction along accessibility to establish accessibility of each code.The proof combines four inductions: rank, accessibility of the head, rank again, and accessibility of the tail.Source: C Well-foundedness of the… · pp. 26–27

D The Γ0 equivalence, the one-claim theorem, and the triangle

For the Veblen order, IGA proves well-foundedness exactly when it admits bivalence of accessibility; the paper also relates that well-foundedness to membership of γ0 in a primitive-recursive form of Kleene’s O. Its one-claim theorem derives both results from O-induction at γ0, while adding the accessibility-bivalence rule gives a sound and consistent extension that proves well-foundedness.

D The Γ0 equivalence, the one-claim theorem, and the triangle

  • IGA proves well-foundedness of the whole Veblen notation exactly when it admits bivalence of accessibility for that order.The bivalence rule is sound for the Veblen order exactly when that order is well-founded.Source: D The Γ0 equivalence, the one-claim… · p. 28
  • Over IGA, well-foundedness of the Veblen order is interderivable with the claim that γ0 belongs to Kleene’s O.The one-claim theorem derives γ0 ∈ O and well-foundedness from O-induction at γ0; the reverse direction uses well-foundedness in the proof of O-membership.Source: D The Γ0 equivalence, the one-claim… · pp. 28, 30
  • The one-claim theorem’s O-induction at γ0 uses rank and number inductions in its supporting lemmas, but no induction along the Veblen order.A build-time dependency check and proof reading provide evidence for this restriction; the check is not a proof-term search for such rule instances.Source: D The Γ0 equivalence, the one-claim… · p. 30
  • Adding bivalence of accessibility for the Veblen order as a rule gives a sound and consistent extension that proves its well-foundedness.The proof replays the right-to-left direction of the equivalence with the rule present.Source: D The Γ0 equivalence, the one-claim… · p. 30

E Goodstein’s theorem

IGA proves Goodstein’s theorem by combining the internally proved well-foundedness of the ε0 code order with a decrease lemma for Goodstein sequences. The resulting grounded derivation yields the usual HOL statement that every Goodstein sequence reaches zero.

E Goodstein’s theorem

  • IGA proves that every Goodstein sequence reaches zero, and omega soundness yields the corresponding HOL theorem.The result is stated as iga_goodstein; its HOL reading says every run from ⟨0, n⟩ has some step with value 0.Source: E Goodstein’s theorem · pp. 31, 33
  • The decrease argument represents each state by a canonical ordinal code, bumps the base, and shows the next code is smaller when the current value is nonzero.The compiled terms compute the ordinal, stepped state, and run; the internal order is the ε0 order at those projections.Source: E Goodstein’s theorem · pp. 31–33
  • The decrease lemma is proved in RGA and embedded into IGA as the premise for the Goodstein theorem.Its proof assembles arithmetic and course-of-values results, including the digit law, a bound, base change, and monotonicity of canonical codes.Source: E Goodstein’s theorem · pp. 31, 33
  • The IGA proof applies well-founded induction along the compiled ε0 order to a motive stating that any run reaching a given ordinal code terminates.The proof first invokes the internal well-foundedness theorem for ε0, then establishes the motive’s progressiveness using the decrease lemma.Source: E Goodstein’s theorem · p. 33

F Truth exactness

The truth construction encodes RGA’s own evaluation rules in one positive fixed point and establishes exact agreement with the omega model. The section also shows that adding conditional proof for a self-referential conditional yields Curry explosion, while a related Liar argument needs additional classical rules.

F Truth exactness

  • The fixed point is omega-true exactly when a term has the stated value or reaches the stated head form.Soundness and completeness are established by induction over the omega relations, with clause-specific lemmas handling the rules.Source: F Truth exactness · pp. 33–35
  • Truth for RGA’s own language is represented by one positive, closed fixed-point body whose clauses mirror the omega model’s evaluation rules.The construction uses twenty-two clauses, including a split of the equality rule into equal- and distinct-value cases.Source: F Truth exactness · p. 34

G Curry’s paradox

  • Under assumptions for a conditional former, the Curry term converts to its own conditional and yields the derivation of 0 = 1.The proof uses conversion in both directions and applies the hypothesis twice; the resulting explosion contradicts RGA consistency.Source: G Curry’s paradox · pp. 35–36
  • A conditional-proof argument for the definable implication ¬a ∨ b also yields explosion, but uses disjunction elimination and double-negation elimination.The paper separately notes that the accessibility-bivalence shape fails when the Liar replaces accessibility.Source: G Curry’s paradox · p. 36

H The Theorems and Their Isabelle Names

The theorem register records IGA’s grounded and classical results, from fixed-point induction and well-foundedness to Goodstein, hydra, and truth theorems. It also locates the Γ0 boundary in accessibility bivalence and distinguishes proved results from classical metatheorems.

Ground induction and fixed points

  • Ground induction supports transport and induction for positive fixed points, and the omega model validates the rule, is consistent, and identifies their truth sets with least fixed points.The register also identifies accessibility with HOL’s accessibility predicate and the winning set with the game’s least fixed point.Source: H The Theorems and Their Isabelle Names · p. 37

Well-foundedness

  • IGA proves the Cantor-normal-form order well-founded at ε0 and proves accessibility for each φ(n, 0), while HOL derives standard ε0 well-foundedness through soundness.The register distinguishes these grounded claims from corresponding classical HOL results.Source: H The Theorems and Their Isabelle Names · p. 37

Goodstein and the hydra

  • IGA proves Goodstein’s theorem outright from its decrease lemma, with the corresponding HOL theorem obtained through soundness.The theorem register names the sequence coding, ordinal map, decrease lemma, and grounded termination result.Source: H The Theorems and Their Isabelle Names · p. 38
  • For every primitive-recursive hydra strategy, IGA derives termination from a decrease lemma, alongside a classical omega-model result and HOL readings.The register lists the internal hydra decrease and order-theory lemmas separately from the grounded termination theorem.Source: H The Theorems and Their Isabelle Names · p. 38

Truth

  • The truth results include classical exactness with the omega model, a least-fixed-point characterization, and grounded induction and refutation results.Determinacy of the truth term’s values is listed separately as depending on a closure obligation.Source: H The Theorems and Their Isabelle Names · p. 38

The price of the classical world

  • IGA proves well-foundedness of the Veblen notation exactly when it admits accessibility bivalence for that order, and bivalence is sound exactly for well-founded orders.The register also records a Γ0 adoption result that is sound and consistent and interderivable with the corresponding well-foundedness claim.Source: H The Theorems and Their Isabelle Names · p. 38

Other registered results

  • The register also records Curry explosion under conditional-proof assumptions, failure of the Liar-shaped accessibility-bivalence rule, a no-go result, and OGA’s containment of PA.It distinguishes these results by system and viewpoint, including classical results and grounded derivations.Source: H The Theorems and Their Isabelle Names · pp. 37–38
Loading 2610.34548v1…