{"path":"research/derivation-sciencepedia-and-the-logic-core.md","content":"# Derivation, SciencePedia and the logic core: three ways of recovering the reasoning a leap hides\n\n**Date:** 2026-10-23. **Standing:** a reading of the Derivation project's deck and of a bachelor\nthesis by one of its members against the corpus, and proposals entered as ledger rows AX5 to AX7; nothing ruled, nothing\nbuilt. Companion to [folded-routes-and-shared-premises.md](folded-routes-and-shared-premises.md),\nwritten the same evening.\n\n## 0. In short\n\n1. **Three projects share one diagnosis.** Written knowledge keeps conclusions and drops the\n   reasoning between them. SciencePedia calls what is dropped *the dark matter of knowledge*;\n   Derivation calls the whole *nets of knowledge* joined by long chains of conclusions; Deliberus\n   calls each link *a chain folded up*. His sentence joins them: *the inferences in the leap, in the\n   dark*. § 2.\n2. **They differ in what checks a recovered chain**, and that decides where each can work.\n   SciencePedia checks the end of a chain against an answer a machine can verify. Derivation means to\n   check the steps by formal logic and formulas, *\"like with a calculator\"*. Deliberus checks the\n   middle between two given ends, with small tasks and people, where no answer can be verified. § 2.\n3. **So logic in Deliberus has three layers, and only one is built.** A *deductive* layer, where a\n   step applies a rule that admits no exception and a prover can check it; a *computational* layer,\n   where a step computes a quantity from sourced inputs by a formula; and the *gradual* layer, where\n   steps are defeasible and strength is computed from relevance and independence. The gradual layer\n   is built; the other two are not, and they are what Derivation's deck describes. § 4.\n4. **The floor's two tests are already validity and irredundancy** (AG14: no ordinary situation where\n   the step's sentences hold and its end fails; no sentence that could be taken away). For a strict\n   step, once its sentences are formalised, a prover decides both exactly. What it cannot decide is\n   whether the formalisation is faithful: on record, a model filling a formal proof put the\n   conclusion in as an axiom in 59 of 105 fabricated-axiom cases. § 4a.\n5. **A member's thesis is the other half of what Derivation needs.** Knowledge lives in *epistemological\n   frameworks*; what one framework counts as knowledge is *presumed knowledge* to another; frameworks\n   coexist through their *intersections*, and the only meta-framework is the intersection they all\n   share. Deliberus has most of the parts to compute this (holders, stances, lenses) and none of the\n   surface. § 3.\n6. **What is possible today, what is not, and what each would need** is the table in § 6.\n\n---\n\n## 1. His words, 2026-10-23\n\n*\"Logic is obviously core to Deliberus. I feel like throwing this on the wall and seeing what sticks:\n[the deck] … You could also read up\non SciencePedia in the docs. The dark matter of science, as the inferences in the leap, in the dark,\nyou know.\"*\n\n*\"Reflect deeply about all this and what's already possible through Deliberus and what's not yet and\nwhat would be required. Make sure to not miss anything relevant in the corpus, use the corpus graph.\"*\n\n## 2. One diagnosis, three checkers\n\n**What is already on record.** Derivation was read in full on 1 April, the day a mutual friend\nintroduced one of its members to the founder (the private notes hold that reading, the overlap table and his\nvoice note from that day). SciencePedia (Li et al., *Inverse Knowledge Search over Verifiable\nReasoning*, arXiv:2510.26854) was read in May and again on 7 October\n([writing-out-the-unwritten.md](writing-out-the-unwritten.md) § 4; its helper's report\n[writing-out-the-unwritten/outside-reading-explication-with-checks.md](writing-out-the-unwritten/outside-reading-explication-with-checks.md) § 1).\nSince April that member has shared a bachelor thesis in theoretical philosophy (Stockholm University,\nspring 2026), read here in § 3; it is not published, so it is described and not quoted, and the\nmember is not named on this page.\n\n**The deck** (*Derivation Presentation*, the project's, made April 2023 and last edited October 2025; twelve\npages). What it holds that bears here: observations become data, data statistics, statistics knowledge\n(the hermeneutic circle); deduction with propositional and predicate logic; knowledge systematised\nacross fields because *\"there is no limitation between the fields in reality\"*; openness to *\"all\nconsistent methods of knowledge - those that do not contradict themselves\"*; nets in which *\"to make an\nadvanced conclusion in genetics … you need to connect a long and complex chain of conclusions from\nvarious fields\"*, updated by formulas that *\"generate the validity of arguments automatically, like\nwith a calculator\"*; the Moon's recession of 3.8 cm a year as a conclusion reached by formulas over\ncombined observations; a model of a building from formulas, like the finite element method; arguments\nshown *\"both formally and in plain language\"*; and discussion that refers to arguments instead of\nrepeating refuted ones.\n\n**What each project checks.**\n\n| | What is recovered | What checks it | Where it can work |\n|---|---|---|---|\n| SciencePedia | long chains from first principles to an answer, about 3–4 million questions in ~200 courses | the end only: two solver models from different makers must reach the same verifiable answer (a number, a formula, code, a choice); the steps are not checked | where an answer can be verified by machine; *\"largely omits human-centric information\"* in its own words |\n| Derivation (as designed) | premises and conclusions joined by logic and formulas | deduction and computation, automatically | where steps are strict or mathematical |\n| Deliberus | the step under a link, between two claims each in a text | the middle between two given ends: is what is written enough to get from one to the other, nothing missing, nothing idle; small tasks with measured agreement, and people | where neither end can be verified, which is most of what people disagree about |\n\nThe three are not rivals. Each checker covers a slice the others cannot reach, and a long chain\nacross fields (Derivation's genetics example) passes through all three kinds of step.\n\n## 3. A member's thesis, read against the corpus\n\n**What it argues.** Against both *forced monism* (one true way to know) and *radical pluralism*\n(anything goes, no coordination), knowledge lives in **epistemological frameworks**: sets of axioms,\nassumptions, methods or values that structure how claims to knowledge are justified and judged,\nexplicit or tacit, individual or shared. **Natural frameworks** are tacit (Polanyi and Kuhn's tacit\nknowledge) and can be analysed only from inside; **constructed frameworks** are explicit rule systems,\nlike Newton's mechanics or Carnap's linguistic frameworks. What framework X counts as knowledge is,\nto an adherent of Y, **presumed knowledge** (*förmodad kunskap*), unless X's axioms are strictly\ncompatible with Y's. Coexistence is when adherents tolerate each other's frameworks as presumed\nknowledge without sharing them. Frameworks meet in **intersections** (shared axioms, data, methods or\nconclusions), identified only by the agreement of those who hold them. A framework must be internally\nconsistent; a *meta-framework* that tolerates contradictions among its members is not one, and the\nonly meta-framework is **the intersection all its members share**. Communication across frameworks is\npossible, and *\"vi kan koordinera mellan dem utan att de behöver konvergeras\"*.\n\n**What maps onto Deliberus, and how far each is built.**\n\n| His term | In Deliberus | State |\n|---|---|---|\n| epistemological framework | a worldview lens; a holder's set of stances (ledger AU3: a lens is computed from its holder's own agree and disagree) | lenses open (Arc AU) |\n| presumed knowledge | a claim shown with who holds it (AO4, holder's stance shown wherever a claim is attributed) | open |\n| intersection | the claims several holders all accept; the shared rules among lenses (AT7) | computable once stances exist; no surface |\n| the meta-framework as the shared intersection | the common ground the bridging signal looks for; the 2012 group's *context spheres, each with its own axioms* ([what-the-group-held-2011-2017.md](what-the-group-held-2011-2017.md) § 1.3) | designed, unbuilt |\n| a framework must be consistent | Deliberus keeps opposite assertions of different holders side by side by design ([store-the-uses-read-the-meaning.md](store-the-uses-read-the-meaning.md) § 4c); inconsistency inside one holder's stances is not computed | not built |\n| coordinate without converging | the transformed convergence wager in [../vision.md](../vision.md): most disagreement dissolves, a small set of typed residues remains | a wager, his |\n| temporary axioms (Kronvall 2012) and Carnap's choice of framework | the hinge score clamps a claim granted or denied and re-propagates (`deliberus/hinge.py`); the what-if view (AU1) | computed inside, no surface |\n\n**A tension worth naming.** The canon line *what is invisible from inside a position is visible from\noutside it* says frames are best audited from outside. The thesis says, of cognitive dissonance,\nthat from outside we cannot know every premise a person holds, so only the person can find a\ncontradiction in their own natural framework. Both hold, for different objects: the outside sees the\nframe's shape, the inside holds the full set of premises. Writing premises out (AG14, AX3 in the\ncompanion note) is what lets the two meet: a contradiction among written premises can be shown to\nthe person, by code where the premises are formal and by a reader where they are not. Claude's\nreading.\n\n**What the thesis adds that the corpus lacks.** The corpus treats a holder's stance as one claim at a\ntime. Its frameworks are *sets* that must cohere, which makes a lens's own consistency a property\nworth showing to its holder, and makes the shared intersection, not an average, the honest form of\ncommon ground.\n\n## 4. Logic in Deliberus: three layers\n\nThe floor names four ways a step goes: a rule applied to a case, a sign to what it indicates, one\ncase to a like case, and cases to a general rule\n([the-chain-inside-a-link.md](the-chain-inside-a-link.md) § 11). Only the first can be strict, and\nonly when its rule admits no exception.\n\n### 4a. The deductive layer (not built)\n\n**What it would do.** For a step whose rule is strict (*all men are mortal*, a definition, a\nmathematical identity), translate its sentences into first-order logic and ask a prover two questions:\nis the end entailed by the sentences (AG14's first test, *no ordinary situation where the sentences\nhold and the end fails*, which for a strict step is validity), and is each sentence needed (the second\ntest, irredundancy; a SAT solver can prune unneeded premises, as GAAR does). Both answers are exact.\n\n**What it cannot do, measured in the corpus**\n([writing-out-the-unwritten/outside-reading-explication-with-checks.md](writing-out-the-unwritten/outside-reading-explication-with-checks.md) § 2–3):\nvalidity is easy to satisfy once the right bridging sentence is added, so a prover separates nothing\nright from wrong in what was added; translation errors are invisible to the solver (LINC: syntax\nerrors in 13 to 38 % of translations, 2023 models; implicit facts such as *Harry is a person* lost);\nand in a two-stage Lean pipeline GPT-5 fabricated axioms in 107 runs, 59 of the 105 classified being\nthe conclusion itself put in as an axiom. A human expert judged 207 of 209 translations correct in\nGAAR's narrower setting. So the prover is a second reader of form, never of content, and its input\nneeds its own check.\n\n**Where it pays.** Strict steps are few in debate and common in law, mathematics, definitions and\nclassification. The 2012 group's Socrates syllogism (*if all men are mortal, then if this is a man,\nthis is mortal*) is the case it decides completely.\n\n### 4b. The computational layer (not built)\n\n**What is missing.** A claim today is text. No field holds a value, a unit, or how a value was\ncomputed (searched in the code 2026-10-23: no field for a quantity, a unit or a formula; content\ndates are the one structured value, `deliberus/temporal_extraction.py`). Derivation's Moon example is\na claim of this kind: *the mean Earth–Moon distance grows about 3.8 cm a year*, computed from\nobservations by formulas.\n\n**The template is already ruled in part.** AL5 (open) gives a clock fact an instrument: inputs\nrecorded, result, time, instrument, an explicit unknown when it fails, one check reused by every claim\nthat depends on it. A computed quantity is the same contract with a formula as the instrument: its\ninputs are claims with values, units and their own sources; its result is a claim; when an input\nchanges, the result is recomputed and the change shows (Derivation's calculator, and the Lake-style\nre-validation in [lean-deliberus-analogies.md](lean-deliberus-analogies.md) § 7). Uncertainty travels\nwith it: an input's range gives the result's range. A what-if over quantities (*if the Moon were more\nmassive*) is then the what-if of Arc AU applied to numbers, under AT6's rule that every relationship it\nassumes still holds is a claim to argue.\n\n**The object-level graph** designed in the mail of April\n([store-the-uses-read-the-meaning.md](store-the-uses-read-the-meaning.md) § 4b: what each claim is\nabout, one proposition with subject, relation, object or value, qualifiers and time) is where a value\nwould first be read from a claim's words. Unbuilt.\n\n### 4c. The gradual layer (built)\n\nDefeasible steps, sign steps, analogies and generalisations: relevance as two factors (Q33), the\nweakest premise within an argument and independent arguments adding in log-odds (Q38, Q46, built\n2026-10-23), the independence reading (Q40, built), schemes with critical questions, the keeper's\nsameness check. This is where Deliberus is ahead of everything it has been compared with, and where\nneither a prover nor a calculator reaches.\n\n### 4d. How the three meet in one chain\n\nA long chain across fields mixes all three: a definition (deductive), a measurement turned into a\nrate (computational), and *so the mechanism likely applies here too* (gradual). Each step is checked\nby its own layer, and the chain's standing comes from the gradual layer, since one defeasible step\nmakes the whole defeasible. Shown folded, it is the route of the companion note (AX4): its weakest\nstep is where to look, whichever layer that step belongs to.\n\n## 5. The dark matter in the leap\n\nSciencePedia recovers chains backwards from concepts to the questions that reach them, and keeps only\nthose whose end two models verify alike. The corpus's May reading stands: the method is *\"parasitic on\nthe checkable endpoint\"*, and agreement between models is weaker evidence than it looks, since models\nerr together more often as they grow more accurate (Correlated Errors, ICML 2025). Its corpus is\npublic (the GitHub README: 4 million question and answer pairs, *\"AI-generated + expert-verified\"*,\nthough the paper mentions no expert check).\n\n**What it could still give Deliberus.** For an empirical claim in its domain, a chain from SciencePedia\nis a candidate evidence subgraph under that claim (the evidence-as-subgraph design): machine-written,\nmarked as such, carrying *endpoint agreed by two models* as its only check, and weighing nothing until\na text or a person takes it up (AG12, ruled). That fills the dark matter where a checker exists,\nwithout importing a guarantee the steps never had. Derivation could make the same move from its side.\n\n## 6. What is possible, what is not yet, what it would take\n\n| Derivation's or the thesis's aim | In Deliberus today | What it would take |\n|---|---|---|\n| premises and conclusions as addressable units | built: claims, links, schemes, critical questions | — |\n| conclusions update when observations change | built for strength (the badge recomputes); the hinge score clamps a claim and re-propagates | a surface for granting and denying (AU1) |\n| deduction shown and checked | the step's sentences can be written (trial only; AG14 ruled, no pass built) | a pass that writes steps; a step-kind mark; formalisation plus a prover for strict steps, with its own fidelity check (AX5) |\n| formulas and quantities | none: claims are text | value, unit and computation on a claim; the instrument contract (AL5) with a formula as instrument (AX6) |\n| long chains across fields, viewable | 2,003 claim pairs six or more support links apart; the map shows two links out | folded routes (AX4) |\n| shown formally and in plain language | plain language only | the formal rendering of strict and computed steps, beside the sentence |\n| many epistemologies, consistent | lenses designed (Arc AU), not built; contradictions kept across holders | lenses; a holder's own inconsistencies shown to them; the intersection of lenses (AX7) |\n| referring to arguments instead of repeating them | built in principle: one claim, one home (AL1), sameness detection | — |\n| a field classification (Dewey) | concepts by use, not a fixed classification (AM7, ruled) | deliberately not taken |\n| premises from peer-reviewed databases | sources extracted; evidence as subgraph designed | SciencePedia-style chains as marked evidence subgraphs (§ 5) |\n\n## 7. Proposals (Claude's, unruled; ledger AX5 to AX7)\n\n1. **AX5 · a strict step gets a formal check.** When a written step applies a rule that admits no\n   exception, its sentences are formalised and a prover answers AG14's two tests; the prover is a\n   second reader of form beside the reader the floor already uses, and its formalisation is checked\n   for faithfulness before its answer counts (§ 4a).\n2. **AX6 · a quantity is a claim with an instrument.** A claim that states a value carries the value,\n   its unit and how it was obtained; a computed value names its formula and its input claims, is\n   recomputed when an input changes, carries its inputs' uncertainty, and returns an explicit unknown\n   when an input is missing (§ 4b).\n3. **AX7 · a lens shows its holder its own contradictions, and lenses show their intersection.** Once\n   lenses exist, a holder sees where their own stances conflict (by code where the claims are formal,\n   by a reader where not, never as a verdict on the person), and several lenses show the claims they\n   all accept as their common ground, the thesis's meta-framework (§ 3).\n\n**Only he decides:** whether Deliberus takes on the deductive and computational layers at all, or\nleaves them to projects like Derivation and SciencePedia and links to them; and whether to pick up the\nApril proposal to Derivation (a shared trial on outside texts), for which the deductive layer is that member's field.\n\n## Sources\n\nThe deck: *Derivation Presentation*, the Derivation project, Google Slides, read 2026-10-23 as exported text.\nThe thesis: a bachelor thesis in theoretical philosophy, Stockholm University VT 2026, shared privately and\nread in full 2026-10-23; author, title and the messages around it in the private notes.\nCorpus notes named in each section;\nthe corpus graph's searches on deduction, derivability, interdisciplinary nets and quantitative\nclaims returned the notes cited here.\n"}