| # | Description | Status | Sources |
|---|---|---|---|
| A. Inputs | |||
| A1p25001 | The classical theorems, used as proved: Gödel’s first and second incompleteness theorems with Rosser’s strengthening, Tarski’s undefinability of truth, the essential undecidability of $\mathsf{Q}$ and of $\mathrm{R}$, Gödel’s speed-up. No classical derivation is disputed. | I | |
| A2p25002 | Model theory, classical results used as proved. Trakhtenbrot: validity over the class of all finite structures is not recursively enumerable. Presburger arithmetic is complete and decidable. Second-order Peano arithmetic is categorical under full semantics (Dedekind). Second-order arithmetic truth is not arithmetical. | I | |
| A3p25003 | Proof complexity and bounded arithmetic, used as proved. Polynomially bounded proof systems are tied to the hard-tautologies problem, and superpolynomial lower bounds hold for specific weak systems. Pudlák bounds finite consistency statements and frames the finite-domain programme. The row also imports feasibility, bounded arithmetic, Chaitin’s information bound and partial truth definitions. | I | |
| A4p25004 | The corpus: effective determinacy characterises the finite structures, proved also as 5:D8. No bounded agent certifies that its universe is infinite: every bounded record consistent with an infinite domain is realised in all sufficiently large finite structures. The master rows naming this paper as a source are 00:A3, 00:A4, 00:A4, 00:Z1–00:Z3 and 00:Z9. | I | master: 00:A2 |
| B. Structures, agents and grades of decision | |||
| B1p25005 | The setting: a structure $\M$ in a finite signature $\sigma$ with $\lvert\M\rvert=m\ge2$ finite. $L$ is its first-order language, and $\varphi\in\Th(\M)$ abbreviates $\M\models\varphi$, likewise $\ThSO(\M)$ for second-order sentences under full semantics. The running example is $\M_p=(\{0,\dots,p-1\};0,1,+,\times)$, arithmetic modulo a prime. Rows E1, F7, F8, G5 and G8 are stated over $\M_p$. | D | Section 2 |
| B2p25006 | Iteration and induction: iteration names the successor act, total on a finite cycle, where it wraps. “Unbounded iteration” abbreviates the freshness claim, a successor injective and never returning to zero. Induction names the proof principle. The two are independent. A finite ontology keeps induction and the act, and declines the freshness claim. | D | Section 2 |
| B3p25007 | The agent: capacity $(K,H)$ over an alphabet of $a\ge2$ letters, at most $K$ symbols of storage and $H$ elementary steps. A derivation system $\D$ is sound, its steps locally checkable with checking polynomial $p_{\D}$. A certificate is a retained, step-checked record of a $\D$-derivation with one designated end sentence, of length at most $B=\min(K,H)$. | D | Def. 2.1 |
| B4p25008 | Local soundness: a rule is locally sound if it preserves truth in every structure that agrees with $\M$ on the table entries its check consults. An axiom rule is locally sound when its sentence is true in every such structure. An axiom asserted on syntactic recognition consults nothing. | D | Def. 2.1 |
| B5p25009 | Grades of decision. (i) A truth value and nothing more. (ii) A decision specified as a finite evaluation object over the tables, of computed size on the order of $m^{q}$ at quantifier depth $q$. (iii) Certification by an agent within its budget. A sentence is in the reach gap when decided at grade (ii) and not at grade (iii). | D | Def. 2.2 |
| C. Gödel’s hypotheses over a finite structure | |||
| C1p25010 | No finite structure interprets $\mathsf{Q}$: a model of $\mathsf{Q}$ has an injective successor with $0$ outside its range, and on a finite set an injective map is onto. | T |    Prop. 3.1 master: 00:Z1 |
| C2p25011 | Completeness and decidability: for finite $\M$ the theory $\Th(\M)$ is complete, consistent and decidable by exhaustive evaluation. A sentence of quantifier depth $q$ takes at most $c\,m^{q}$ atomic evaluations, $c$ depending on its length. One first-order sentence $\sigma_{\M}$ characterises $\M$ up to isomorphism. | T | Prop. 3.2 master: 00:Z1 |
| C3p25012 | Vacuity: over a fixed finite $\M$ neither incompleteness theorem has an instance. $\Th(\M)$ is consistent, effectively axiomatisable and complete. The hypothesis that fails is the interpretation of $\mathsf{Q}$ (C1). No sentence true in $\M$ is undecided by $\Th(\M)$. | T | master: 00:Z1 |
| C4p25013 | Trakhtenbrot’s theorem concerns validity over the class of all finite structures. The finite ontology examined here commits to one structure, not to the class. For a fixed $\M$ row C2 applies and no undecidability enters. | D | Rem. 3.3; C2 master: 00:Z1 |
| C5p25014 | Tarski scoped: the $m+1$ sentences $\varphi,\neg\varphi,\dots,\neg^{m}\varphi$ outnumber the $m$ elements of $\M$, so every numbering of the sentences by elements of $\M$ gives two of them the same number. Truth in $\M$ is defined externally by a finite table with the evaluation procedure of C2. What fails is the internalisation of truth. | T | Rem. 3.5; C2 |
| D. The part cannot hold the whole | |||
| D1p25015 | Relational diagonal: an agent of storage capacity $K$ with $a^{K}<m$ has no injective encoding of the elements of $\M$ into its storage states. Every internal representation identifies distinct elements. A fortiori the agent holds no faithful model of $\M$ that also represents the model’s own encoding map. | T | Thm. 4.1 master: 00:A4 |
| D2p25016 | The limitation relocated: the diagonal’s limitative role passes from the provability of truths to the representability of the totality by a part. Tarski undefinability relocates the same way in its representational face: truth of $\M$ is externally a table, internally unrepresentable by a smaller part. | D | Rem. 4.2 master: 00:A4 |
| D3p25017 | Wrap, aliasing: every total assignment of storage readings to the elements of $\M$ identifies distinct elements when $a^{K}<m$. Some reading stands for at least $\lceil m/a^{K}\rceil\ge2$ elements. Every element outside a maximal faithfully represented range is read as an alias of one inside it. | T | Lem. 4.3(1) master: 00:A4 |
| D4p25018 | Wrap, no internal trace: the steps that verify a certificate succeed in a finite $\M'$ built on its cited table entries, $\lvert \M'\rvert\le(r+1)\,p_{\D}(B)$, $r$ the largest arity. Under locally sound rules its end sentence is true there. An axiom asserted on syntactic recognition transports as a record, not as a truth. If $(r+1)\,p_{\D}(B)\le a^{K}$, no certificate marks a reading exact. | T | Lem. 4.3(2) |
| E. The reach bound | |||
| E1p25019 | Abundance: the closed terms over $\{1,+\}$ with $\ell$ leaves are the full binary trees, $C_{\ell-1}\ge2^{\ell-2}$ in number. In $\M_p$ all have the value $\ell\bmod p$, so any two give a true equation of length $O(\ell)$, at least $2^{\ell}$ of them for $\ell\ge6$. The true sentences of length at most $L$ number at least $2^{\alpha L}$ for large $L$, $\alpha>0$ constant. | T | Lem. 5.1 |
| E2p25020 | Vanishing reach: an agent of capacity $(K,H)$ certifies at most $a^{B+1}$ sentences over all its runs, the records being strings of length at most $B$. The certified fraction of the truths of length at most $L$ (E1) is at most $a^{B+1}/2^{\alpha L}$, below $1/N$ as soon as $\alpha L>(B+1)\log_2a+\log_2N$. | T | Prop. 5.2; E1 |
| E3p25021 | Possession: certification is possession under the retention clause. Holding a schema and a derivation procedure is holding two records, not the instances. An instance is possessed exactly when its own certificate is retained. | D | Rem. 5.3 |
| E4p25022 | A single hard sentence, system-relatively: the bare evaluation calculus infers $\forall x\,\varphi(x)$ from the $m$ premises $\varphi(c)$. Every derivation of a global clause there has length at least $m$ and defeats every budget $H<m$. A richer $\D$ may derive some global clauses briefly. | T | Rem. 5.4 |
| F. The diagonal under finitude | |||
| F1p25023 | Mention cost: if the truth of a formula in $\M$ depends on coordinate $i$ of a tuple of variables, then $v_{i}$ occurs in it. A formula whose truth depends on all $N$ coordinates has length at least $N$. A quantifier block binding an $N$-tuple contributes at least $N$ symbols. | T | Lem. 5.5 |
| F2p25024 | No compression: code strings of length at most $N$ as tuples in $\M^{N}$, one coordinate per symbol, signature and alphabet fixed independently of $N$, $\theta$ non-degenerate. The Gödel template has no instance at any scale. The diagonal formula needs $\lvert \delta\rvert\ge3N+\lvert \theta\rvert>N$ symbols, so its code is not in $\M^{N}$. Splitting the scales fails: $\delta$ outgrows the scale $\theta$ reads. | T | Thm. 5.6; F1 master: 00:Z9 |
| F3p25025 | Quotation exceeds mention: a formula’s arity is below its length. No sentence $\lambda$ contains a subformula whose truth depends on all coordinates of a tuple of arity at least $\lvert \lambda\rvert$. Under any coding that spends at least $\lvert \lambda\rvert$ coordinates on $\lambda$, per-symbol coding included, no sentence’s truth is sensitive to every coordinate of its own code. | T | Cor. 5.7; F1 master: 00:Z9 |
| F4p25048 | Density: $m$ has $d$ base-$a$ digits. An injective coding of length-$n$ strings by $k$-tuples, $k\ge1$, needs $m^{k}\ge a^{n}$, so $n<dk$. In F2’s $\delta(u)=\exists v\,(\mathrm{Diag}(u,v)\wedge\theta(v))$ let $v$ have $k$ coordinates and $u$ have $k_{1}$. Each coordinate of $v$ is named three times, each of $u$ once. So $\lvert\delta\rvert\ge2c(k)+c(k+k_{1})$, and $\lambda=\delta(\ulcorner\delta\urcorner)$ has $\lvert\lambda\rvert\ge3c(k)+k_{1}$, $c(j)$ the total length of the $j$ shortest names. | T | Lem. 5.8; F2 |
| F5p25027 | What the construction consumes: classically, one variable over an unbounded arithmetic carries a code of any size at constant syntactic cost. Over a fixed finite structure it carries one element’s digits. Gödel’s proof uses infinity as a syntactic resource, the exponential compression of quotation. Row F2 concerns the construction, not material biconditionals, and does not diminish the classical result. | D | Rem. 5.13 |
| F6p25047 | The threshold lies inside the count: the code of $\delta$ fills $u$, that of $\lambda$ fills $v$. By F4 the template needs $2c(k)+c(k+k_{1})<dk_{1}$ and $3c(k)+k_{1}<dk$. Let $k^{*}(\M)$ be the largest such $k$, or $0$ if none, and $t(\M)=d\,k^{*}(\M)$. No instance codes $\lambda$ at length $n\ge t(\M)$, and $t(\M)<m$ in every structure. $k^{*}(\M)<6a^{\lfloor d/3\rfloor+1}$, and $k<6a^{\lfloor d/4\rfloor+1}$ at one scale, $k_{1}=k$. | T | Lem. 5.8; F4 |
| F7p25049 | Decoders: over $\M_p$ with $+$, $\times$, $0$ and $1$, a formula $\mathrm{Int}_{J}(x)$ of $50J+29$ symbols in the syntax of F8 defines $\{0,\dots,2^{J}-1\}$ when $2^{J}\le p$. It writes the binary expansion with six bound variables, four of them reused. A formula $\mathrm{Dig}(y,r,s)$ defines digit $r$ of $y<\beta^{n}$ in base $\beta=2^{b}$ when $2^{bn+1}<p$, at a length linear in $bn$. | T | Lem. 5.9 |
| F8p25050 | A dense-coded instance: alphabet of $32$ symbols, constants $0,\dots,16$, $D=1024$ symbols per element, $k_{1}=4096$, $k=45044$, $p$ of at least $D+2$ digits in base $32$. For every $\theta(v)$ of at most $704\,170$ symbols without variables of $u$, a formula $\mathrm{Diag}$ defines diagonal substitution on strings with the layout of $\delta$, and $\lvert\delta\rvert\le Dk_{1}$, $\lvert\lambda\rvert\le Dk$, $\M_p\models\lambda\leftrightarrow\theta(\ulcorner\lambda\urcorner)$. | T | master: 00:Z9 |
| G. What stands in the diagonal’s place | |||
| G1p25028 | Length horizon: a certificate contains its designated end sentence, so no sentence longer than $B=\min(K,H)$ is certifiable. None longer than $H$ has a derivation of length at most $H$ in any system. Beyond every budget there are truths, by counting alone (E1, E2). | T | |
| G2p25029 | The evaluation ceiling: without the local-checkability clause the one-rule system $\D_{\mathrm{tt}}$ asserts $\varphi$ outright on exhaustive evaluation. It is sound, and every true $\varphi$ has a derivation of length $\lvert \varphi\rvert$. So a truth lacks a derivation of length at most $H$ exactly when it is longer than $H$. The step-check of $\D_{\mathrm{tt}}$ costs on the order of $m^{q}$ evaluations. | T | Prop. 5.15 |
| G3p25030 | The complexity remainder: whether every sound, locally checkable $\D$ leaves short truths underivable at every budget is the hard-tautologies problem, open in general and proved for specific weak systems. For bounded consistency, certificates below $H^{\varepsilon}$ are excluded where Pudlák’s bounds hold, and the budget-$H$ analogue is open. The status is the same on both ontologies. | I | Rem. 5.16; A3 master: 00:Z1 |
| G4p25031 | Prefix simulation: $Q_{1}z_{1}\cdots Q_{d}z_{d}\,\psi(\bar z)$ holds in $\M$ exactly when $\forall y_{1}\exists x_{1}\cdots\forall y_{d}\exists x_{d}\,[\bigwedge_{i:Q_{i}=\forall}x_{i}=y_{i}\wedge\psi(\bar x)]$ does: one uniform prefix simulates every coded quantifier pattern. | T | Lem. 5.17 |
| G5p25032 | Fragment truth is definable over $\M_p$ with $p\ge a+1$, in the expansion $L_{A}$ of $L$ by alphabet-code constants. For each $n$ of $s$ digits a formula $\mathrm{Truth}_{n}(v)$ of length $O(n^{2}s)$ defines truth for the coded prenex sentences of length at most $n$. It rejects every other code. It guesses parse and evaluation labels, checked by local clauses under G4’s prefix. | T | Thm. 5.18; G4 master: 00:Z9 |
| G6p25033 | What remains undefinable: no single formula defines truth across all lengths, since a formula has fixed arity. Under per-symbol coding none defines truth for sentences longer than itself, by F1. Between the two, truth is definable fragment by fragment, from just above and never from within. | T | master: 00:Z9 |
| G7p25034 | Decomposition: each classical limitation (Gödel I and II, Tarski, speed-up) splits into a counting and a complexity face. The counting face is a theorem (E2, G1, D1, G6), and $\Con{H}(\D)$ is true at grade (ii). The complexity face is imported (G3), with one reversal (G5). The diagonal is unavailable: per-symbol at every scale (F2), any coding beyond $t(\M)$ (F6). | T | |
| G8p25051 | Truth in the window: at the scale of F8 no formula $T(v)$ of at most $704\,169$ symbols without variables of $u$ defines truth for the densely coded sentences of length at most $Dk$. Take $\theta=\neg T$ in F8. The names of all $k$ variables take $225\,220$ symbols, so the bound is not one of arity. | T | Cor. 5.11; F8 master: 00:Z9 |
| H. Co-extensiveness | |||
| H1p25035 | The effectivity clause: among consistent, effectively axiomatised theories, interpreting $\mathsf{Q}$ forces incompleteness. $\Th(\N)$ is complete at grade (i) only, presentable by nothing. Presburger arithmetic separates unbounded iteration from coding power: it is complete and decidable. Incompleteness tracks an effective description confronting a domain that codes its own syntax. | D | |
| H2p25036 | Finiteness, the finite direction: for finite $\M$ the full second-order theory $\ThSO(\M)$ is decidable. A second-order quantifier over $k$-ary relations ranges over the $2^{m^{k}}$ subsets of $\M^{k}$, and exhaustive evaluation decides every second-order sentence. | T | Thm. 6.1 |
| H3p25037 | Finiteness, the classical direction: if $\M$ contains a countably infinite subset, $\ThSO(\M)$ under full semantics is undecidable. A decision procedure would decide second-order arithmetic truth through a copy of $\N$ (A2). The passage evaluates the infinite ontology by that ontology’s own semantics. | T | Thm. 6.1; A2 |
| H4p25038 | Determinacy meets effectivity only on the finite. The structures whose entire theory, second-order included under full semantics, is decidable are exactly the finite ones, in H3’s sense of infinite (H2, H3). Infinite structures offer determinacy at grade (i) or effectivity over a fragment. Finitude delivers both, at grade (ii). | T | |
| H5p25039 | Trichotomy: consistent, effectively axiomatised theories fall into three disjoint, exhaustive cells. (i) Essentially undecidable theories, whose incompleteness is irreparable. (ii) Theories outside (i) with no finite model, whose incompleteness an effective extension removes. “At least $n$ elements, for every $n$” with a free predicate is one. (iii) Theories with a finite model. Irreparable incompleteness tracks effective self-representation, not cardinality. | T | |
| J. Neutrality | |||
| J1p25040 | Evidential force: a certificate’s categorical and conditional content. The categorical content is its end sentence as warranted by the checked steps alone, present exactly when every rule used is locally sound. The conditional content is the end sentence under the undischarged hypothesis that the rules are sound in the inhabited structure. Counterparts agree in both, up to the hypothesis named. | D | Def. 7.1 |
| J2p25041 | Neutrality, certificate level: place a bounded agent in an infinite world under a consistent, effective $\mathsf{Q}$-interpreting description, or in a sufficiently large finite structure. Categorical contents are realised certificate for certificate (D4), and conditional contents transfer verbatim. No certificate available to a bounded agent discriminates the two situations. | T | |
| J3p25042 | The diagnosis: the effectivity hypothesis is the agent, abstracted. The excess of truth over certificates is information about the certifier’s finitude, not about the cardinality of the world. Consequences are drawn for Hilbert’s programme, for the anti-mechanist argument and for the platonist moral. The row is a reading argued from J2. | D | Section 7; J2 |
| J4p25043 | The residue for the finitist: agents get no completeness (E2). No certificate of a part has the totality’s cardinality as its categorical content (D4). Universal arithmetic claims are read schematically, instance by instance below the bound. In exchange, determinacy is effectively realised in full on this ontology alone (H4). | D | |
| J5p25044 | Objections O1–O8 are answered. Grade (ii) asserts a specification and a computed size, not the realisation of the evaluation object (O8). The agent bounds are parameters, not psychology (O4). No feasibility predicate is used, and no number is called too large to exist (O5). | D | Section 8 |
Nothing matches that filter.
Status
- I
- Import. A standard result, or a corpus result, used without reproof.
- D
- Definition. A naming, a declared convention or a reading, carrying no claim of its own.
- T
- Theorem. Derived in the paper, and machine-verified in exact arithmetic where the source column names a witness.
Sources
- Gold: the python check that decides the predicate, at its line in the script (the source, rendered on this site); on hover the deciding family and the families that corroborate it, and the verdict of the last run (red when it fails). The script page's bar runs the predicate's cell of the package's notebook on Google Colab (one cell per predicate; the whole notebook from the header badge).
- The predicate as one Lean declaration, named by its accession key (
p25010) — the conjunction of the theorems that prove it — at its line in the rendered module, one mark per library that proves it, the core's first. Green: the core (lean/FrcCore) — the statement on the shell ring, by computation and induction, no Mathlib, no axioms: the finitist witness. Violet: Mathlib (lean/FrcLedger) — the classical statement for every shell on Mathlib's hierarchy (its axioms,propext,Classical.choice,Quot.sound, on hover). Red: a proof the gate rejects (an unfinished proof,native_decide) — not a witness. A predicate proved in both libraries shows both marks; one mark, one proof. The module page's bar opens the module as one executable file in Lean Live (the core on plain Lean, no Mathlib; the file elaborates in the browser and prints every predicate's axioms at its end); the header's two Lean badges count the marks of each colour and open the two executables. - section
- The statement in the paper's body that carries the predicate: a proposition, a remark or a section.
- rests on
- The predicates it rests on, by label: realisations, definitions and imports of this ledger, predicates of other ledgers (
32:B3) and of the master (00:D15).