LITE: Dynamic Self-Reference in Peano Arithmetic

Abstract

The Look In The Eye (LITE) framework demonstrates how a fixed arithmetical construction within Peano Arithmetic (PA) can encode bounded self-reference. By combining the Recursion Theorem with bounded proof-code searches formalized in PA, LITE defines a function whose output is selected by local checks for proofs or refutations concerning propositions about its own Gödel code. The function is not redefined as proofs are discovered by an external mathematician. Its rule is fixed; for each input n, the bounded search determines which branch applies. LITE broadens our perspective on definability and self-reference by showing how arithmetic can represent a structured feedback pattern through ordinary function definitions and proof predicates.

1. Introduction: Understanding LITE

1.1. The Traditional View: Formal Arithmetic as Static

Historically, many areas of mathematics, such as dynamical systems, ergodic theory, and chaos theory, have dealt extensively with evolving or changing phenomena. Within formal arithmetic, however, definitions do not change after they are given. Their values are determined by fixed rules, axioms, and proof predicates, not by later human discovery.

By focusing on dynamic self-reference specifically in Peano Arithmetic, the LITE framework shows how a fixed arithmetical rule can include a bounded feedback pattern. The function does not acquire a new definition when proofs are found. Instead, its definition already contains finite proof-code searches that select different branches at different inputs.

• Fixed Definitions in PA: Formal arithmetic keeps definitions fixed once given. LITE preserves this while encoding bounded checks inside the definition itself.
• Contrast with Other Fields: In dynamical systems, geometry, or parts of proof theory, “change” and iteration are commonplace. LITE shows a parallel pattern inside Peano Arithmetic without adding new axioms.
• The LITE Perspective: By constructing a function that checks for bounded proof codes of statements referencing its own code, LITE bridges static arithmetical foundations and branch-selected self-reference.

1.2. A Fresh Angle on Self-Reference

Classical Gödelian self-reference focuses on the existence of certain sentences (“I am not provable in PA”) whose truth and provability statuses intertwine in profound ways. LITE extends this tradition by using an infinite family of self-referential statements, one for each natural number input. The value of the fixed function at each input depends on whether bounded proof-code searches find support for the relevant statement or its negation:

• Iterative Aspect: At each input n, LITE checks a statement ϕ_β(n) that references the fixed point code β of the function itself.
• Branch Selection: If bounded support is found, the rule selects one of the jump branches. If no bounded support is found, the rule selects the default branch.
• Dynamic Self-Reference: The sequence can display adaptive-looking behavior because different inputs may satisfy different bounded checks, even though the defining rule remains fixed.

By combining the Recursion Theorem with bounded proof-code searches, LITE generates a family of statements whose bounded provability determines the branch chosen by f at each input.

1.3. What This Means for Arithmetic

LITE shows that arithmetic can encode a function whose output depends on bounded proof-code searches about formulas referring to its own code. The function does not update itself. Self-reference is built into one fixed rule, and each input activates one branch of that rule:

• From Static to Dynamic: The definition remains fixed, but the output sequence can vary according to which bounded proof-code checks succeed at each input.
• Embedding Feedback Loops: By referencing its own code and bounding proof-code searches, f models a formal self-monitoring pattern inside standard PA.
• Richer Self-Reference: Unlike single-shot sentences, LITE uses an input-indexed sequence of self-referential statements to determine branch behavior across the natural numbers.

Within the Predictive Universe framework, LITE is a mathematical model of bounded self-monitoring. It illustrates the logical pattern behind Dynamic Self-Reference Operator behavior and Property R: a system encodes a description of itself, runs bounded checks on propositions about that description, and routes outputs through the result. LITE is not a physical model of consciousness or an MPU. It is a clean arithmetical demonstration that the self-referential machinery used by the framework can be implemented inside ordinary arithmetic.

The sections below lay out how LITE is formally constructed, the mathematical details that ensure its consistency, and why it broadens the frontier of arithmetical definability and self-reference.

Universe 00110000

2. Mathematical Foundation

2.1. Peano Arithmetic and Gödel Encoding

LITE rests on classical Peano Arithmetic (PA). Its language comprises symbols for 0, successor (S(⋅)), addition, multiplication, and ordering, along with the usual logical machinery. Through Gödel numbering, every finite string (be it a formula or proof) is encoded as a natural number:

1. Gödel Coding: A bijection ⟨·⟩: Σ* → ℕ assigns unique codes to expressions, enabling arithmetic to speak about syntactic objects numerically.
2. Provability Predicate Prf(p, ⌈ψ⌉): Within PA, this relation asserts that p is the code of a valid proof of ψ. This is key for referencing “whether ψ can be proven in PA.”

With this apparatus, statements in arithmetic can self-reflect: they can contain references to codes of formulae and proofs, including statements about the function f we aim to define.

2.2. Bounded Proof Search via g(n)

Central to LITE is the notion of checking for a proof within a specific size bound, controlled by a fast-growing function g(n):

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

Although potentially huge, g(n) remains finite for each n, so there is no paradox in searching all proof codes p ≤ g(n). If none exist, the search terminates without success; if a bounded proof code exists, it is eventually identified. This bounding technique makes the entire process definable inside PA and ensures that checking these proofs does not require stepping outside the system.

By coupling g(n) with the function we define, LITE determines at each input whether certain statements can be proven or refuted under that proof-code bound. This local proof search is the engine of the branch-selection process.

2.3. The Recursion Theorem

An essential ingredient is the Recursion Theorem, which guarantees that a function can validly reference its own code without inconsistency. In simpler terms, it states that for any total computable operator Ψ(α,n), there is a code β such that the partial computable function ϕ_β satisfies:

ϕ_β(n) = Ψ(β, n).

By interpreting β as the code of f, we obtain a legitimate self-referential definition. In LITE, this theorem allows the formula ϕ_β(n) to include the code of the very function whose value is being computed. The resulting construction connects bounded proof-code checks with numeric outputs.

3. Dynamic Self-Reference in LITE

3.1. Main Construction

At the heart of LITE is a function f: ℕ → ℕ defined via:

f(n) =
  { n + H1(n), if Prf≤g(n)(⌈ϕβ(n)⌉);
    n + H2(n), if ¬Prf≤g(n)(⌈ϕβ(n)⌉) ∧ Prf≤g(n)(⌈¬ϕβ(n)⌉);
    n + 1, otherwise. }
    

Here, Prf_≤g(n)(⌈ψ⌉) abbreviates ∃p ≤ g(n) Prf(p, ⌈ψ⌉). The formula ϕ_β(n) is a statement about the fixed point with Gödel code β. The second branch is written with explicit priority: it applies only when the first bounded search fails and the bounded search for the negation succeeds. The functions H₁(n) and H₂(n) are chosen to produce noticeable jumps when a bounded proof-code search succeeds. If neither branch succeeds, f(n) = n + 1 by default.

Because of the Recursion Theorem, there is no contradiction in letting ϕ_β(n) refer to the fixed point code of the same function whose value is being computed. This yields a total computable function whose self-reference is handled by a fixed piecewise rule.

3.2. Shifting Values Based on Proof Discovery

The novelty lies in how f(n) is determined by a fixed self-referential branch rule rather than by a simple closed-form expression. For each input, the computation performs a finite proof-code search for ϕ_β(n) and then, if needed, for ¬ϕ_β(n). A successful bounded search selects the corresponding jump branch. If no bounded support is found, the default value n + 1 is returned.

Because n + H₁(n) or n + H₂(n) can be relatively large jumps, the resulting sequence can show long stable stretches followed by sharp changes. These changes are outputs of the original fixed rule, not later redefinitions of f.

3.3. Feedback Over the Natural Numbers

By design, each n activates a local bounded check: “Is ϕ_β(n) provable by some code p ≤ g(n)? If not, is ¬ϕ_β(n) provable by such a code?” This input-indexed sequence of checks creates an iterative feedback pattern throughout the natural numbers. The fixed definition stays the same, while different inputs can activate different branches.

4. Mathematical Properties

4.1. Well-Defined and Total

• Consistency: The Recursion Theorem supplies a fixed point code β, allowing ϕ_β(n) to reference the same function without an informal circular definition.
• Finite Search: Checking proof codes p ≤ g(n) is always finite. The priority order in the piecewise rule assigns exactly one output branch.
• Totality: Assuming g, H₁, and H₂ are total computable functions, every branch yields a natural number, so f(n) is total on ℕ.

4.2. Intrinsic Dynamism

Classic recursive functions remain fixed after definition, and f remains fixed in the same sense. Its distinctive feature is that the fixed definition contains bounded self-referential branch checks. The output sequence can display adaptive-looking behavior without changing the defining rule.

4.3. Rich Structure

Each point n belongs to an indexed family of self-referential checks. Depending on how the formulas are chosen, bounded proof results at some inputs can produce long stable intervals followed by large jumps in output values. The structure is generated by one fixed rule.

5. Theoretical Significance

5.1. Extending Gödel’s Legacy

Gödel’s incompleteness opened the door to self-reference in arithmetic. LITE pushes this further, showcasing how an entire collection of self-referential statements, one per input, can collectively govern the branch behavior of a fixed arithmetical function.

5.2. Bridging Proof Discovery and Function Values

• Local Proof Checks: Rather than positing broad reflection principles, LITE uses bounded statements “∃p ≤ g(n) Prf(p, ⌈ϕ(n)⌉)” to modulate f in a tightly controlled manner.
• Unified Formalism: The entire mechanism fits within standard PA with no extra axioms, relying on definable proof predicates and the Recursion Theorem.

5.3. Deeper View of Arithmetic’s Expressive Power

By embedding a bounded self-reference protocol into a single function, LITE shows that arithmetic can exhibit formal feedback patterns once we leverage self-reference carefully. This broadens conceptions of what “arithmetical definability” can achieve.

Universe 00110000

6. Mathematical Analysis

6.1. Iterative Construction

1. For each n: Check for proof codes of ϕ_β(n) or ¬ϕ_β(n) with p ≤ g(n).
2. Branching: If the first search succeeds, return n + H₁(n). If it fails and the second search succeeds, return n + H₂(n). Otherwise, return n + 1.
3. Sequence: Repeating this fixed rule across inputs yields a self-referential output sequence over ℕ.

6.2. Potentially Complex Behavior

Although f is total, its path can exhibit surprising turns when proofs (or disproofs) become accessible. Long periods of quiescence may give way to sudden large changes if certain short proofs about f appear.

6.3. Governed by Proof Bounds

All stages remain anchored in finite proof-code searches bounded by g(n). As n grows, g(n) grows, allowing the rule to test larger finite regions of the proof-code space. This interplay of a growing bounding function and input-indexed self-reference is the essence of LITE’s dynamic flavor.

6.4. Concrete Example

7. Formal Structure

7.1. Recursion Theorem Implementation

To ensure ϕ(n) truly references f, one typically constructs a computable operator Ψ(α, n) that uses α as the code of a function. The Recursion Theorem guarantees a fixed point β with ϕ_β(n) = Ψ(β, n). Interpreting β as the code of f completes the self-referential loop.

In essence, this means the definition of f can use its own Gödel code and incorporate references to its own values in the statement ϕ_β(n). This is performed within PA’s ordinary coding of syntax and proof predicates, yielding a self-consistent definition that does not overstep the theory’s expressive capabilities.

7.2. The Proof Predicate

The definability of Prf(p, ⌈ψ⌉) in PA makes it possible for f(n) to check whether ψ has a proof code p ≤ g(n). This tight coupling of code, proof, and bounding function ensures the construction is represented internally in arithmetic.

7.3. Harmony of Components

• Self-Reference: From the Recursion Theorem.
• Bounded Search: From ∃p ≤ g(n) criteria.
• Branch-Selected Function: From the piecewise rule that assigns f(n) based on bounded proof-code results.

Combined, these yield LITE’s characteristic feedback pattern: each numeric argument n triggers a bounded inspection of proof codes about ϕ_β(n), and the result determines the numeric output.

7.4. Core Theorem and Complete Proof

Universe 00110000

8. Broader Perspective

8.1. From Single Statement to Infinite Family

Traditional self-reference often hinges on a single statement (Gödel’s “I am not provable”). LITE extends this to a structured infinite family {ϕ_β(n) : n ∈ ℕ}, each referencing a different input n and the same fixed point code β.

8.2. Iterative Updates

• Ongoing Branch Selection: The function f can produce different output patterns when different bounded proof-code searches succeed or fail.
• Potential Complexity: Because g(n) grows, the output sequence may remain stable for many inputs, then jump significantly when a bounded proof-code search succeeds.

8.3. New Interpretations of Self-Reference

LITE demonstrates that self-reference need not be limited to self-negating or self-asserting statements. It can also be used to build fixed arithmetical structures whose output branches depend on the presence or absence of bounded proof codes about themselves.

8.4. Possible Generalizations

• Stronger Theories: While this construction is shown in PA, one can import the same ideas into larger axiomatic systems, preserving or amplifying the dynamic feedback loops.
• Variants of g(n): Different bounding functions might yield different patterns of when new proofs become accessible, further diversifying the possible behaviors of f.

8.5. Comparison with Classic Self-Reference Frameworks

9. Conclusion

The LITE framework underscores a novel view of self-reference in which an arithmetical function f(n) selects its values based on whether bounded proof-code searches concerning ϕ_β(n) or its negation succeed within a bound g(n). In contrast to single-shot Gödelian statements, LITE organizes a sequence of self-referential checks across the natural numbers. The function is fixed once defined; the output sequence records which bounded branches succeed at each input.

By relying solely on standard tools, including Gödel coding, the definable proof predicate Prf(p, ⌈ψ⌉), a fast-growing bound g(n), and the Recursion Theorem, this construction remains within classical PA. It shows that arithmetic can encode formal feedback patterns without adding new axioms or redefining the function after the fact.

LITE therefore gives a precise arithmetical model of bounded self-monitoring. With careful constraints and finite proof-code bounds, a function can reference its own code and route its output through local checks about itself while remaining a standard fixed construction.