Source-linked AI summary

A Non-Formulable Theorem: A Fundamental Limit of Finite Syntactic Systems and Its Consequences for Security and AI

Fabio F. G. Buono

arXiv:2609.04086v1cs.CRcs.AIcs.LO

TL;DR

The paper asks whether finite syntactic systems can autonomously produce a theorem about their own structural limits. It combines syntactic invariants with Gödel numbering and self-reference to prove that every coherent, sufficiently expressive finite system has at least one theorem it cannot produce autonomously.

  • Problem

    The paper investigates whether a finite syntactic system can formulate and derive a proposition asserting the existence of its own syntactic limits.

  • Method

    The paper combines the Syntactic Invariance Principle, Gödel numbering, and self-referential diagonalization to construct and analyze a system-specific limit proposition.

  • Results

    Every coherent and sufficiently expressive finite syntactic system has at least one theorem it cannot autonomously produce, including the theorem asserting its own structural blind spots.

  • Takeaways & Limitations

    The result applies across finite syntactic systems, while overcoming the limit requires a change of observational level rather than more computation.

  • Takeaways & Limitations

    The unified FCP is a post-hoc conceptual reinterpretation; its ingredients remain independently established by their own technical proof methods.

Abstract

from arXiv · show

For every coherent and sufficiently expressive finite syntactic system S, we prove the existence of at least one theorem that S cannot produce autonomously. The result is a metatheorem: it proves the existence of a theorem, and applies to every finite syntactic system - security mechanisms, AI systems, formal verifiers, legal systems, economic models, and the formal system in which it is itself proved.

1 Introduction

The paper asks whether a finite syntactic system can formulate and derive a proposition about its own limits, concluding that structural blind spots prevent autonomous production of at least one such theorem.

  • Central question: The paper turns the invariance principle inward by asking whether a system can derive a proposition asserting its own syntactic limits.The target concerns a semantic property of the system itself, beyond the local level observed by its rewriting rules.
  • Main result: The result is existential: every coherent and sufficiently expressive finite system has at least one theorem it cannot autonomously produce.The theorem concerns the existence of the system’s own structural blind spots, not the inability to originate every theorem.
  • System definition: Finite syntactic systems are tuples S = (V, F, R, I) with finite variables, function symbols, rewriting rules, and initial clauses.Every component is finitely specifiable and computable.
  • Syntactic invariants: The Syntactic Invariance Principle freezes properties preserved by every rewriting rule throughout all derivations.Frozen terms remain unchanged with respect to the invariant, regardless of which rules are applied.
  • Syntactic blind spots: A syntactic blind spot is a derivable term whose invariant property the system cannot itself communicate.The system can contain or process the term while lacking a derivation that states the invariant property.

5 Gödel numbering for syntactic systems

Gödel numbering encodes a finite syntactic system and its derivability relation as computable data, enabling a self-referential limit proposition that is true but not autonomously derivable.

  • Encoding: Gödel numbering injectively and computably represents every structural element and formula of the finite system by a natural number.Compound terms are encoded structurally, and every element of the system is representable.
  • Derivability: The encoded derivability predicate is computable because the finite deterministic rule system permits enumeration of all possible derivations.It returns whether the proposition encoded by n is derivable from S.
  • Self-reference: The diagonal lemma converts a meta-level limit observation into a proposition within the system’s own language that refers to its derivability status.Self-reference is needed for the contradiction showing that both deriving and denying the proposition fail.
  • Limit proposition: The limit proposition ϕS asserts that a frozen term containing a Skolem constant exists, but S cannot derive it because those constants lie outside its vocabulary.The proposition concerns the rule set’s inability to unify with certain terms, a structural fact no rule inspects from within.

7 The self-referential proposition

The paper constructs GS as a self-referential proposition asserting that the system’s own limit is not provable, then argues that coherence forces GS to remain undecidable.

  • Construction: GS states that its own content, describing a limit of S, is not provable by S.Its Gödel number is fixed by diagonalization so the proposition refers to itself.
  • Undecidability: The argument concludes that a coherent system derives neither GS nor ¬GS.The displayed conclusion is S ⊬ GS and S ⊬ ¬GS.
  • Structural obstruction: Deriving GS would require a local rewriting system to produce a global assertion about the structure of all its rules.The paper identifies this locality–globality gap as the structural source of the contradiction.
  • Contradiction: Deriving ¬GS contradicts the Syntactic Invariance Principle because frozen syntactic invariants are guaranteed to exist.Under coherence, the system cannot derive both the negation and the invariant-supported truth.
  • Interpretation: GS is a specific structurally unproducible proposition about intrinsic limits, rather than an arbitrary theorem the system has not yet found.Its undecidability reflects a limitation of the system’s syntactic resources.

9 Inextensibility and infinite regress

Extending a finite system to derive its limit proposition produces a new finite system with new frozen terms and a new undecidable proposition, so the incompleteness chain never closes.

  • 9 Inextensibility and infinite regress: A coherent finite extension S′ that attempts to derive GS remains a finite syntactic system with its own syntactic invariants.New rules create new frozen terms through fresh symbols and new pattern clashes.
  • 9 Inextensibility and infinite regress: The sequence S0 := S, Sn+1 := coherent extension of Sn that attempts to derive GSn generates a new undecidable proposition at every stage.Each extension inherits the same structural problem it was intended to resolve.
  • Universality: The universality theorem applies to every finite syntactic system regardless of its vocabulary, rules, domain, or expressive power.Each such system cannot autonomously generate at least one proposition about its own intrinsic limits.
  • AI implication: The AI corollary models weights, transformations, learning rules, and prompts as the components of a finite syntactic system.Under this modeling, an AI cannot autonomously generate understanding of its own fundamental limits.
  • AI implication: The paper distinguishes processing information about oneself from generating awareness of one’s structural limits.It conditionally links the latter capacity to consciousness and claims finite systems lack it under that definition.
  • Assumptions: The argument requires sufficient expressiveness for internal Gödel representation and self-reference, while coherence prevents contradictory derivations.Below the expressiveness threshold, the self-limitation question is not formulable; incoherent systems have no reliable output.

12 The main metatheorem

Theorem 12.1 establishes that every coherent, sufficiently expressive finite syntactic system has true limit propositions and self-referential propositions that it cannot derive or refute. Extending the system produces a new undecidable proposition rather than eliminating the limitation.

  • Every coherent, sufficiently expressive finite syntactic system has a true proposition ϕS asserting the existence of a syntactic invariant and its associated limit.
  • S cannot derive either ϕS or its negation: S̸ ⊢ϕS and S̸ ⊢¬ϕS.
  • A self-referential Gödel proposition GS exists, asserting that its own content is not derivable from S.
  • GS is likewise undecidable within S: S̸ ⊢GS and S̸ ⊢¬GS.
  • Every coherent extension S′ remains finite and has a new proposition GS′ with the same undecidability properties.

13 Irrefutability

The paper claims that its metatheorem cannot be refuted by any finite syntactic system because every such system has the intrinsic limits described by the theorem. The result is existential and structural: systems may generate other theorems, but not the theorem identifying their own blindness.

  • A finite syntactic system cannot coherently derive a proposition denying Theorem 12.1, because doing so would contradict the theorem’s guaranteed conclusion.
  • Coherence is presented as a best-case assumption because an incoherent system can derive any proposition and therefore provides no reliable security guarantee.
  • The theorem’s mechanism combines syntactic invariants, which supply frozen terms, with the Kleene fixed point, which supplies self-reference.
  • The result applies to finite syntactic systems beyond classical first-order theories, including rewriting systems, type checkers, neural networks, and automated provers.
  • The theorem is existential rather than total: a system cannot autonomously generate at least one theorem about its own intrinsic limits, but may generate many other theorems.
  • A system can understand, verify, or apply the theorem when it is communicated externally, although it cannot originate that theorem autonomously.

15 Consequences for security

The paper applies the metatheorem to security mechanisms and formal verifiers, arguing that finite syntactic systems possess structural blind spots they cannot identify internally. It therefore frames external verification at a higher observational level as necessary within the paper’s scope.

  • Security mechanisms such as firewalls, intrusion detection systems, formal verifiers, type checkers, content filters, and antivirus engines are treated as finite syntactic systems.
  • A security system cannot autonomously formulate that inputs exist which its rules cannot inspect, although the proposition is semantically true under the Syntactic Invariance Principle.
  • Formal verifiers may miss semantic program properties above their syntactic rule level and certify a program as safe while it violates the intended specification.
  • Intrusion detection systems can miss semantically malicious inputs that remain syntactically indistinguishable from benign traffic at the pattern level.
  • The paper states that adding rules, patterns, parameters, or computation at the same observational level does not close the structural gap.
  • External verification at a higher observational level is presented as the practical response to limits that internal improvement cannot identify.
  • Which observer is sufficient, and whether such an observer can be physically implemented, remains an open question.

18 Alternative route: the result via the obstruction theorem

The alternative proof route uses a general local syntactic obstruction theorem to recover the paper’s qualitative self-limitation result. It additionally supplies quantitative lower bounds showing that local extensions become increasingly costly as instances grow.

  • The Local Syntactic Obstruction theorem generalizes the Syntactic Invariance Principle from the superposition calculus to arbitrary local syntactic systems.
  • Fresh Skolem constants create protected positions, and the invariant Inv is preserved because the system’s rules cannot rewrite those positions.
  • No derivation in S proves a+b = b+a, yielding syntactically separated but semantically equivalent terms that S cannot equate.
  • The subsequent Gödel numbering, fixed-point, undecidability, inextensibility, universality, and irrefutability arguments proceed from the existence and truth of ϕS.
  • Ω(n) derivation length is required for local extensions to prove a+b = b+a on n-gadget instances, rising to Ω(2n) under clause-per-configuration encoding.
  • The quantitative result strengthens inextensibility by showing that approaching the barrier costs at least linearly, and potentially exponentially, with instance complexity.
  • The obstruction theorem interprets self-limitation as an observational collapse that local computation cannot eliminate.

19 Minimal route: the result from finiteness alone

The minimal route derives self-limitation from finiteness alone: finite rule patterns leave an unrewritable term, induction preserves that obstruction, and the diagonal lemma supplies self-reference.

  • Existence: Finite left-hand-side heads leave a sufficiently expressive language with a symbol c that no rule can match at the root.Because c is outside the finite head set H, no substitution resolves the first-symbol clash.
  • Existence: If c is a constant, the resulting term has no internal positions, so no rule can rewrite it anywhere.This provides a concrete unrewritable witness without requiring a Skolem constant.
  • Permanence: Induction on derivation length shows that the unrewritable term remains unchanged whether rewriting occurs elsewhere or around it as a proper subterm.The term is never itself a redex, so it remains unrewritable at every subsequent step.
  • Truth and non-derivability: The proposition ϕS asserting that an everywhere-unrewritable term exists is true, because finiteness and expressiveness guarantee the witness.Its truth depends only on the finite rule set and the expressive language.
  • Truth and non-derivability: S cannot autonomously derive ϕS because its local rewrites do not enumerate, inspect, and reason about the global structure of its rule set.The required operations are meta-level operations on R, whereas derivations produce terms or clauses.
  • Self-reference and generality: The diagonal lemma creates the self-referential proposition GS, while coherence supplies the contradiction needed to exclude both GS and its negation.Adding finitely many rules merely creates a new uncovered term and a new GS, so the chain never terminates.

20 The unifying principle: finite coverage

The finite coverage principle abstracts the paper’s mechanism: a finite set of inspection patterns leaves uncovered elements in a richer domain, preserves their inaccessibility, and cannot autonomously formulate that blind spot.

  • Finite coverage principle: A finite inspection mechanism matches domain elements against a finite pattern set, classifying each element as covered or uncovered.The mechanism acts only when an element matches at least one pattern.
  • Finite coverage principle: If an uncovered element exists, the mechanism cannot act on it, and finite iteration cannot bring it into coverage.Uncoverage persists when the element appears as a sub-element of generated outputs.
  • Finite coverage principle: Under coherence and sufficient expressiveness, the true proposition that an uncovered element exists is not autonomously derivable by the mechanism.This is the principle’s blindness consequence: the claim concerns the pattern set itself.
  • Applications: The finite-coverage principle subsumes the paper’s syntactic example because any symbol outside the finite head set produces the same uncovered term; Skolem constants are unnecessary.The SIP is presented as one instantiation of this broader principle.
  • Applications: In the obstruction theorem, locally indistinguishable configurations remain outside finite coverage, while covering all 2^n configurations requires Ω(n) steps.The lower bound quantifies the cost of overcoming the local inspection limit.
  • Classical connections: The same structural pattern is used to interpret observer collapse, classical impossibility results, and the paper’s self-limitation theorem, but the finite-coverage principle is explicitly explanatory rather than derivational.The paper states that each classical result remains logically independent and retains its own proof method.

21 Conclusions

The paper concludes that every coherent, sufficiently expressive finite syntactic system has at least one theorem about its own structural blind spots that it cannot originate. The result extends across formal disciplines, while its proposed escape is a change of observational level.

  • Core conclusion: At least one theorem asserting a finite system’s own structural blind spots cannot be autonomously produced by that system.The claim is existential, not a statement that the system cannot originate any theorem.
  • Core conclusion: Three routes converge on the same conclusion: the SIP supplies mechanism, the obstruction theorem quantifies cost, and the minimal route identifies finiteness as the cause.The paper presents all three because each contributes something the others do not.
  • Scope and applications: The metatheorem is presented as applicable to disciplines using finite formal systems, including formalized mathematics, legal systems, formal epistemology, and computational biology.Each application is framed as a system-level structural limit rather than a claim that the domain is generally incapable of reasoning.
  • Scope and applications: The metatheorem applies to its host formal system rather than to the theorem itself, so self-application does not place the theorem outside its stated scope.The host system retains its own theorem that it cannot originate.
  • Open direction: Overcoming the established limit requires changing the observational level rather than merely adding computation, and the sufficient observer remains an open question.The paper identifies implementation within physical-system constraints as unresolved.
  • Open direction: Different observers can cover different uncovered elements, but no finite union of finite pattern sets exhausts a sufficiently rich domain.Divergent thinking widens coverage without making any culture or observer complete.

A Application to Large Language Models

The appendix models a fixed-weight, greedily decoded LLM as a finite syntactic system whose rules encode next-token behavior. It then shows that applying the main theorem is conditional on expressiveness, with a composed verifier or parser preserving an undecidable structure when the LLM alone falls short.

  • Structure: A fixed-weight LLM with vocabulary Vtok and context window L is represented as a finite syntactic system SM=(V,F,Rθ,IM).Tokens become function symbols, token sequences become terms, and prompts provide initial clauses.
  • Structure: Greedy decoding rewrites each context c to itself concatenated with the highest-probability next token under fθ.The rewriting rules Rθ encode the model’s learned behavior.
  • Structure: The context bound makes Rθ finite, and the resulting tuple satisfies the paper’s finite-system definition even though its rules are ground rather than variable-based.Ground rules are a special case of the required rewriting-rule format.
  • Conditions: The main theorem applies to SM only if the model satisfies coherence and sufficient expressiveness.The appendix explicitly treats the application as conditional rather than automatic.
  • Conditions: Practical LLMs may generate encodings of formulas without possessing an explicit internal symbolic representation of their own axioms, rules, or derivations.Their formal meaning must be interpreted through inference from implicit real-valued parameters.
  • Composed systems: If the LLM falls below the expressiveness threshold, the main theorem does not apply directly, but an LLM combined with an external verifier or parser still exhibits the undecidable structure.The appendix presents this composed-system result as the more robust conclusion.

A.1.3 Temporal Snapshot: The Role of Fixed Weights

The theorem applies to a finite syntactic system representing an LLM at a fixed time, while training changes create new systems with new blind spots. Composing the LLM with a finite parser or verifier preserves finiteness and can restore sufficient expressiveness for the theorem to apply.

  • Fixed-weight systems: At fixed weights, context, and input, an LLM is modeled as a finite syntactic system to which the theorem applies when coherence and sufficient expressiveness hold.The resulting system has an undecidable proposition that this instantiation cannot derive.
  • Temporal change: Each training or adaptation step creates a new finite system with different rewriting rules and a different undecidable proposition.The sequence of propositions is infinite and non-closing, so no finite number of updates eliminates them all.
  • Composition: An LLM-parser composition operates through token generation, token-to-symbol mapping, and symbolic parsing or verification.The combined rule set includes the component rules and interface rules, and remains finite.
  • Composition: The composed system is itself a finite syntactic system, so the theorem applies whenever the composition is coherent and sufficiently expressive.The parser or verifier may supply formal machinery that the LLM alone lacks, allowing the composed system to cross the expressiveness threshold.
  • Assumptions: The composition proof assumes that both components are coherent and that interface rules do not introduce inconsistencies.Under those assumptions, the union of the component systems remains coherent.

A.2.2 Blind Spots in the Composed System

A composed LLM-parser or verifier system can contain a representable proposition that neither component combination can derive or verify. Modifying the parser changes the blind spot but does not remove the structural incompleteness.

  • Composite blind spot: The composite blind spot is a proposition expressible in the composed formal language but not derivable by the composed system.No generated token sequence becomes a valid proof or derivation of that proposition after parsing and verification.
  • Parser independence: Any finite parser redesign preserves undecidability, although the specific blind-spot proposition may change.The persistence follows because each modified composed system has its own diagonal proposition.
  • Parser independence: The sequence of blind spots across parser modifications is infinite and non-closing, so no finite redesign resolves all of them simultaneously.The paper identifies this as an instance of the Finite Coverage Principle.
  • Discrete composition: Continuous LLM weights do not escape the result because deterministic decoding converts weight-dependent probabilities into discrete rewriting rules.The parser then operates symbolically, making the composed system finite and discrete.
  • Concrete example: In proof-generation systems, the blind-spot proposition can be expressible in the verifier’s type theory while remaining neither provable nor disprovable by the combined system.This concerns the specific fixed-weight LLM and fixed-rule verifier, not necessarily independence from stronger axioms.

A.3.3 Blind Spot as a Function of Architecture

The blind spot depends on the particular architecture and changes when weights or verifier rules change, but every qualifying finite configuration retains one. Consequently, training, composition, and engineering improvements relocate rather than eliminate incompleteness.

  • Architecture dependence: Changing LLM weights or verifier rules creates a new composed system with a new blind spot.The blind spot is therefore a function of the specific architecture rather than a universal mathematical proposition.
  • Security implications: The direct security implication is a coverage gap in which true formal statements may be neither generated nor certified by the LLM-verifier system.The paper connects these gaps to reliability, robustness, and potential adversarial exploitation in security-critical applications.
  • Adaptive systems: Training produces a sequence of new finite systems, each with its own undecidable proposition.The resulting sequence is infinite and non-closing, so adaptation does not eliminate all blind spots simultaneously.
  • Scope: The incompleteness limit applies universally across finite formal systems, including human reasoning when modeled as finite.The paper does not present the limit as unique to LLMs.
  • Composition: A weak LLM can still participate in a sufficiently expressive composite system whose blind spot is guaranteed at the composed level.Formal layers such as inference rules or decision procedures can supply expressiveness absent from the LLM alone.
  • Engineering implications: No parser-rule choice eliminates the blind spot, and the composed system remains subject to classical incompleteness once it is finite and discrete.The limitation is structural rather than a temporary consequence of insufficient training.
  • Scope: The theorem’s application to an individual LLM remains conditional on coherence and sufficient expressiveness, with whether current models cross that threshold left as an empirical question.The caveat concerns applicability to a given LLM, not the theorem’s conclusion once the threshold is met.

B Philosophical Implications: Scientific Progress as Observational Level Transitions

The paper interprets scientific progress as movement between finite observational levels rather than completion within one level. Each new level exposes earlier blind spots while generating new limits of its own.

  • Structural incompleteness: Every finite scientific theory contains at least one true proposition about its structural limits that it cannot derive internally.This is presented as a mathematical property of finite formal theories, not merely a gap in current knowledge.
  • Structural incompleteness: An external observer in a stronger system can formulate and derive a limit proposition that the original theory cannot formulate or derive.The distinction is between internal derivability and access from a larger formal framework.
  • Observational levels: Scientific progress is characterized as a change of observational level with new primitives, observables, and formal machinery.The paper contrasts this with merely accumulating facts, measurements, or data within an unchanged framework.
  • Historical transitions: The historical transitions from Kepler to Newton, Newton to Einstein, and classical to quantum mechanics are formalized as strict observational-level transitions.Each later system has a larger domain of derivable propositions than the earlier system.
  • Open-ended progress: Each new finite and coherent scientific system reveals prior blind spots but possesses an undecidable proposition of its own.Scientific progress therefore forms a sequence of level transitions rather than convergence to a complete final description.
  • Scientific method: Because the scientific method is codifiable as a finite system, it too has propositions about its limits that it cannot validate, prove, or refute internally.The paper presents this as an application of the theorem to the method itself.

B.5 The Hierarchy of Observational Levels

The paper presents scientific knowledge as ascent through an infinite hierarchy of observational levels, where each successor reveals predecessor blind spots and expands derivable knowledge. Complete understanding remains unreachable, but progress is objective, cumulative, and indefinitely possible.

  • Unreachable completeness: The ideal level O⊤ would completely describe reality, but no finite system can attain it.The paper therefore rejects a final Theory of Everything as mathematically impossible within finite formal systems.
  • Cumulative expansion: Each successor system can derive everything its predecessor could derive and additionally resolve propositions that were previously undecidable.The systems form a strictly increasing sequence of derivable domains, with each level complete relative to predecessors but incomplete relative to successors.
  • Cumulative expansion: Progress between levels is objective: richer systems express and formalize propositions that earlier systems could not even represent.The paper characterizes this expansion as genuine growth in the domain of derivable knowledge rather than merely a change of description.
  • Scientific consequence: Although complete understanding is never reached, finite minds can progress indefinitely toward truth through continuous expansion of knowledge.The paper describes this as asymptotic approach rather than final convergence, while maintaining that each advance is a lasting achievement.
  • Mechanisms of scientific change: Scientific revolutions introduce new primitives, pattern sets, and observational perspectives that expose the limits of established frameworks.External observers and intellectual outsiders can identify blind spots because they operate from systems with richer pattern sets.
  • Hierarchy of observational levels: Scientific progress follows an infinite hierarchy of observational levels, with each new level revealing blind spots of its predecessor.The hierarchy is represented as O⊥ ≺ O1 ≺ O2 ≺ · · · ≺ O⊤.
Loading 2609.04086v1…