Cinematic Strawberry

 Logo

LITE: Dynamic Self-Reference in Peano Arithmetic

Abstract

Gödel's construction produces one sentence that talks about itself. The Look In The Eye (LITE) construction produces a whole family of them, indexed by the natural numbers, and hangs the value of a single arithmetical function on what those sentences can prove about it. The function is fixed by Kleene's recursion theorem, which supplies a code β such that the function defined using β is the function β codes. At each input n the rule searches all proof codes up to a bound g(n) for a proof of a sentence ϕβ(n) about its own code, then for a proof of the negation, and returns one of three values according to what it finds.

The function is total and computable, and it never changes. What varies from input to input is which branch fires, and that is decided inside Peano Arithmetic by finite searches. The interesting content lies in the choice of the sentence family, and three results fix it. Choosing a sentence that asserts which branch fires makes every successful search self-fulfilling. Choosing one that denies its own branch makes the search empty at every input, if arithmetic is sound, which is Gödel's argument appearing inside the construction. Choosing a sentence that arithmetic neither proves nor refutes collapses the function to n + 1. The construction adds no axioms, and it defines a function whose values are determined in advance and are not surveyable in advance, because deciding a single value means searching a proof space of size g(n).

LITE in Plain Terms

Suppose a clerk follows one standing rule, written once and never revised. For each number in turn, the clerk opens a filing cabinet and looks for a certificate about what the rule itself will do at that number. If a certificate is found, the clerk writes down one figure. If a certificate for the opposite is found, another figure. If neither, a default. The rule is fixed. The output changes because what is in the cabinet changes from number to number, and the cabinet gets bigger as the numbers grow.

Two things make the arrangement work. The cabinet is finite at each step, so the clerk always finishes looking. And the rule is allowed to mention itself, because there is a theorem guaranteeing that a rule can be written which refers to its own written form without circularity, in the way a program can print its own source code.

What goes into the certificate decides everything, and there are three cases worth separating. Write a sentence that says "the rule pays the bonus here." If a proof of that turns up, the rule pays the bonus, and the sentence was right. The certificate makes itself true. Now write a sentence that says "the rule does not pay the bonus here." If a proof of that turned up, the rule would pay the bonus, and the sentence would be wrong. Arithmetic does not prove false things, so that proof never turns up at any number. The clerk searches forever and never finds it. Third, write a sentence arithmetic simply cannot settle, and both searches fail every time, so the rule always returns the default.

The last thing to notice is about knowing. The whole sequence is fixed in advance by the rule. Working out even one entry means checking every certificate shorter than a bound that grows very fast, so the sequence is decided and unreadable at the same time. That combination is what makes it a model of a system watching itself: everything about it is determined, and nothing about it is available cheaply from inside.

1. Self-Reference, Fixed Once

Formal arithmetic does not change its mind. A definition given in Peano Arithmetic fixes a function, and the function's values follow from the axioms whether or not anyone has worked them out. Discovery belongs to mathematicians; the values were there already.

Self-reference has been available inside arithmetic since Gödel (1931) showed how to encode syntax as numbers and build a sentence asserting its own unprovability. What that construction produces is one sentence, examined once. Rosser (1936) refined it to weaken the hypothesis needed, and Löb (1955) settled the companion question of what happens when a sentence asserts its own provability. In each case the object of study is a single fixed point.

LITE keeps the fixed definition and replaces the single sentence with a family indexed by the natural numbers. A function is defined so that its value at n depends on what can be proved, within a bound depending on n, about a sentence concerning the function's own code at that input. The rule never changes and the branch it takes does, so the output sequence records which bounded searches succeeded and where.

Within the wider Predictive Universe framework, this construction serves one purpose: it shows that the machinery the framework calls computational richness, a system that represents its own description, reasons about it, and evaluates predicates on the result, is available inside ordinary arithmetic with no additional axioms. LITE is a mathematical demonstration and not a physical model. It is not an account of consciousness and not a minimal predictive unit.

Beyond a Single Fixed Point

The classical construction produces one sentence, such as "I am not provable," and studies it. LITE produces a sentence for every natural number, all referring to one code, and routes a function's output through what can be proved about them under a growing bound.

Mathematical Foundation

Universe 00110000

2. The Ingredients

2.1 Coding and the Proof Predicate

The setting is Peano Arithmetic, with symbols for zero, successor, addition, multiplication, and order. Gödel numbering assigns a distinct natural number to every formula and every proof, so that syntactic facts become arithmetical ones. Within that coding the relation

Prf(p, ⌈ψ⌉)

holds when p codes a proof of the formula coded by ⌈ψ⌉. This relation is primitive recursive and is representable in Peano Arithmetic, a fact established by the arithmetization of syntax and set out with its standard conditions by Hilbert and Bernays (1939) and by Feferman (1960).

2.2 Bounded Search

Unbounded provability is not decidable, so the construction never asks whether a proof exists. It asks whether one exists below a bound. Fix a total computable, increasing function g and write

Prf≤g(n)(⌈ψ⌉) ≡ ∃p ≤ g(n) Prf(p, ⌈ψ⌉)

This is a bounded quantifier over a decidable relation, so it is decidable for each n, and it is a Δ0 formula in the language of arithmetic. The search always terminates: it examines finitely many candidates and reports. Parikh (1971) studied exactly this move, showing that bounding proof length changes what is effectively available even where it does not change what is true, and the bound is what keeps the construction inside arithmetic.

2.3 The Recursion Theorem

The last ingredient allows the rule to mention its own code. Kleene's (1938) recursion theorem states that for every total computable operator Ψ(α, n) there is a code β with

φβ(n) = Ψ(β, n) for all n

The operator is written as though the code of the function it defines were already available, and the theorem supplies a code for which that assumption is correct. This is the same fact that lets a program print its own source, and it is what makes self-reference a construction rather than a circularity.

3. The Construction

Definition 3.1 (LITE function). Let g, H1, and H2 be total computable functions, and let n ↦ ϕα(n) be a computable assignment of sentences with the code α occurring in them. Define the operator Ψ by

Ψ(α, n) =  n + H₁(n)   if Prf≤g(n)( ⌈ϕ_α(n)⌉ )
           n + H₂(n)   if not, and Prf≤g(n)( ⌈¬ϕ_α(n)⌉ )
           n + 1       otherwise

and let β be a code with φβ(n) = Ψ(β, n), supplied by the recursion theorem. The LITE function is f = φβ, so that

f(n) =  n + H₁(n)   if Prf≤g(n)( ⌈ϕ_β(n)⌉ )
        n + H₂(n)   if not, and Prf≤g(n)( ⌈¬ϕ_β(n)⌉ )
        n + 1       otherwise

The branches are ordered, so the second is tested only after the first fails, and exactly one applies at each input. The sentences ϕβ(n) refer to the code of the very function being defined, which the recursion theorem licenses.

Theorem 3.2 (Totality). f is a total computable function. If g, H1, and H2 are provably total in Peano Arithmetic, then Peano Arithmetic proves that f is total.

Proof. For each n the two conditions are bounded searches over p ≤ g(n) of the decidable relation Prf, so each terminates and returns a verdict. The ordering of the branches makes the verdicts jointly exhaustive and mutually exclusive, so exactly one value is assigned, and each value is a natural number since H1 and H2 are total. Hence Ψ is total computable, the recursion theorem applies, and f = φβ is total computable. For the second claim, the searches are Δ0 formulas with a provably total bound, so Peano Arithmetic proves that each search terminates and that the case analysis is exhaustive. ∎

No paradox arises, and the reason is worth stating precisely. The rule never asserts that ϕβ(n) is provable or unprovable. It asks a decidable question about proof codes below a bound and acts on the answer. A sentence that asserted its own value would be a different construction with different risks, and Section 4 shows what happens when the sentence family is chosen to create one.

4. Three Choices of Sentence

Definition 3.1 leaves the sentence family open, and the choice decides what the function does. Three choices cover the interesting ground, and each is a small theorem.

4.1 The Self-Fulfilling Choice

Let ϕβ(n) be the sentence asserting that the first branch fires at n:

ϕβ(n) ≡ "f(n) = n + H1(n)"

Proposition 4.1. With this choice, a successful bounded search makes its own sentence true. If Prf≤g(n)(⌈ϕβ(n)⌉) holds then ϕβ(n) is true. If instead the second branch fires and H2(n) ≠ H1(n), then ¬ϕβ(n) is true.

Proof. If the first search succeeds, Definition 3.1 gives f(n) = n + H1(n), which is what ϕβ(n) asserts. If the first search fails and the second succeeds, then f(n) = n + H2(n), which differs from n + H1(n) under the stated inequality, so ϕβ(n) is false and its negation is true. ∎

Both branches vindicate whichever proof was found, so nothing forces a contradiction and Peano Arithmetic can consistently prove either. This is the pattern Löb (1955) identified: a sentence asserting its own provability is provable, and the reason is that acting on the proof makes the sentence come true. The self-fulfilling choice is the one that keeps the construction interesting, because both jump branches remain live.

4.2 The Self-Defeating Choice Is Empty

Reverse the assertion. Let the family be

ψβ(n) ≡ "f(n) ≠ n + H1(n)"

and use ψ in place of ϕ in Definition 3.1.

Proposition 4.2. If Peano Arithmetic is sound for these sentences, then for every n there is no proof code p ≤ g(n) proving ψβ(n). The first branch never fires, at any input, for any choice of g.

Proof. Suppose some p ≤ g(n) proves ψβ(n). The first condition of Definition 3.1 then holds, so f(n) = n + H1(n), which makes ψβ(n) false. Peano Arithmetic would have proved a false sentence, contradicting soundness. Since n and g were arbitrary, no such proof code exists at any input. ∎

This is Gödel's argument turning up inside the construction, and the mechanism is worth naming. Proving the sentence would cause the rule to act in a way that falsifies it, so the proof cannot exist. What makes the first branch unreachable is the same feature that makes the liar sentence troublesome: the content of the sentence is the negation of what asserting it brings about. Enlarging the bound does not help, because the argument never mentioned the bound.

4.3 The Undecided Choice Collapses

Proposition 4.3. If ϕβ(n) is chosen so that Peano Arithmetic neither proves nor refutes it, for every n, then f(n) = n + 1 for every n.

Proof. A bounded proof is a proof, so if no proof of the sentence or of its negation exists then neither bounded search can succeed, and the default branch applies at every input. ∎

The three propositions bracket the construction. Sentences that defeat themselves make the jump branches unreachable, sentences arithmetic cannot settle make them unreachable for a different reason, and sentences that fulfil themselves keep them live. The interest is in the choice of family, and not in the schema alone.

Mathematical Analysis

Universe 00110000

5. What the Function Is Like

5.1 Determined and Not Surveyable

Theorem 3.2 makes f total and computable, so every value exists and an algorithm returns it. The algorithm is not usable. Deciding a single value at n means examining every proof code up to g(n), and g is chosen to grow quickly; with g(n) = 2n+1 the search at n = 100 already exceeds any physical resource. The sequence is fixed in advance and unavailable in advance.

That combination is the point of the construction as a model. A system whose behaviour is entirely determined by a fixed rule about itself, and whose next value cannot be obtained cheaply from inside, is precisely the situation the wider framework describes for finite predictors. Nothing here is uncomputable. Everything here is out of reach.

5.2 The Shape of the Output

Under the self-fulfilling choice, the sequence spends long stretches on the default branch and jumps where a bounded proof appears. Whether the jumps thin out or accumulate depends on how quickly g grows against how the proof lengths of the sentence family grow. That relation is a question about proof complexity in the sense Parikh (1971) opened, and the construction converts it into a question about a sequence of integers.

5.3 A Worked Instance

Take g(n) = 2n+1, H1(n) = 10, and H2(n) = 20, with the self-fulfilling family of Section 4.1. Then

  • n = 0: the search runs over p ≤ 2. No proof of anything interesting has a code that small, so both searches fail and f(0) = 1.
  • n = 1: the search runs over p ≤ 4, fails again, and f(1) = 2.
  • n = k: if the bound first reaches the length of a proof of ϕβ(k) at this input, the first branch fires and f(k) = k + 10. By Proposition 4.1 the sentence proved is then true.
  • If instead the bound first reaches a proof of the negation, the second branch fires and f(k) = k + 20, and by the same proposition that negation is true.

Every entry follows from the single rule of Definition 3.1. What differs across inputs is only which of the three conditions the bounded search reports.

6. Where This Sits

Three features distinguish the construction from the classical results it uses.

Construction What refers to what What is fixed Result
Gödel (1931) One sentence asserts its own unprovability The sentence, examined once Incompleteness of any consistent, sufficiently strong theory
Rosser (1936) One sentence compares proof and refutation lengths The sentence, examined once Incompleteness from consistency alone
Löb (1955) One sentence asserts its own provability The sentence, examined once Such a sentence is provable
Reflection principles A schema asserts that what is provable is true Added to the theory as new axioms A strictly stronger theory
LITE A family of sentences, one per input, referring to one code One rule, with branch selection by bounded search A total function whose values record which bounded searches succeed

The technical ingredients are all standard, and the arrangement is what is new: coding and the proof predicate from the arithmetization of syntax, bounded search from Parikh's (1971) treatment of proof length, and the fixed point from Kleene (1938). No axiom is added, and the function stays inside the theory. The modal analysis of provability that Boolos (1993) and Smoryński (1985) present is the standard setting for the sentences of Section 4, and the propositions there are the LITE instances of its two basic patterns.

What the construction demonstrates for the wider framework is a specific claim, and only that claim. The pattern of a system that encodes a description of itself, runs decidable checks on statements about that description, and routes its behaviour through the outcome, is realizable in Peano Arithmetic without new axioms. Section 4 adds the part that matters for the framework's account of self-reference: the self-defeating family is empty, so a system of this kind can consistently act on what it proves about itself only when what it proves is of the self-fulfilling kind.

BROADER PERSPECTIVE

Universe 00110000

7. Conclusion

The LITE construction defines one total computable function whose value at each input is selected by a bounded search for proofs about the function's own code. The recursion theorem supplies the code, the proof predicate makes the search arithmetical, and the bound makes it terminate. Nothing is added to Peano Arithmetic and nothing about the function changes after it is defined.

The three propositions of Section 4 say what such a construction can do. A sentence family that vindicates the branch it triggers keeps both jumps available. A family that contradicts the branch it triggers is never proved, at any input and under any bound, so long as arithmetic is sound. A family arithmetic cannot settle leaves the function equal to n + 1. Self-reference inside a fixed rule is therefore possible, restricted, and restricted in a way that can be stated exactly.

The function is determined by its definition and expensive to read. That is the property worth carrying away: a system can be entirely fixed by a rule that mentions itself, and still have no cheap route from inside to its own next value.

References

❮
❯