proposit-core

Core engine for building, evaluating, and checking the logical validity of propositional-logic arguments. Manages typed trees of variables and expressions across one or more premises, with strict structural invariants, automatic operator collapse, a display renderer, and a truth-table validity checker.

Also ships a CLI (proposit-core) for managing arguments, premises, variables, expressions, and analyses stored on disk.

Full documentation is available at https://proposit-app.github.io/proposit-core/.

Visual Overview

flowchart TD
    AE["ArgumentEngine"]

    AE --> PM["PremiseEngine (0..N)"]
    AE --> VM["Variables (0..N, shared)"]
    AE --> Roles["Roles"]

    PM --> EM["ExpressionManager"]
    EM --> ET["Expression Tree"]

    VM --> CBV["Claim-Bound\n(claimId, claimVersion)"]
    VM --> PBV["Premise-Bound\n(boundPremiseId,\nboundArgumentId,\nboundArgumentVersion)"]

    CBV -.-> CL
    PBV -.->|"references specific premise\n(may be cross-argument)"| PM

    Roles -.->|"conclusionPremiseId\n(supporting & constraint\nroles are derived)"| PM

    subgraph Injected["Injected Libraries"]
        CL["ClaimLibrary\n(normal + citation claims)"]
        CCL["ClaimCitationLibrary"]
    end

    AE -.-> Injected

    style Injected fill:none,stroke:#888,stroke-dasharray: 5 5

Installation

pnpm add @proposit/proposit-core
# or
npm install @proposit/proposit-core

Concepts

Argument

An ArgumentEngine is scoped to a single argument — a record with an id, version, title, and description. Every variable and expression carries a matching argumentId and argumentVersion; the engine rejects entities that belong to a different argument. Expressions also carry a premiseId identifying which premise they belong to, and premises carry argumentId and argumentVersion for self-describing references.

Premises

An argument is composed of one or more premises, each managed by a PremiseEngine. Premises come in two types derived from their root expression:

• Inference premise ("inference") — root is implies or iff. Used as a supporting premise or the conclusion of the argument.
• Constraint premise ("constraint") — root is anything else. Restricts which variable assignments are considered admissible without contributing to the inference chain.

Variables

A propositional variable (e.g. P, Q, Rain) is a named atomic proposition. Variables are registered with the ArgumentEngine via addVariable() and are shared across all premises. Each variable must have a unique id and a unique symbol within the argument.

Expressions

An expression is a node in the rooted expression tree managed by a PremiseEngine. There are three kinds:

• Variable expression ("variable") — a leaf node that references a registered variable.
• Operator expression ("operator") — an interior node that applies a logical operator to its children.
• Formula expression ("formula") — a transparent unary wrapper, equivalent to parentheses around its single child.

The five supported operators and their arities are:

| Operator | Symbol | Arity | | --------- | ------ | -------------- | | not | ¬ | unary (= 1) | | and | ∧ | variadic (≥ 2) | | or | ∨ | variadic (≥ 2) | | implies | → | binary (= 2) | | iff | ↔ | binary (= 2) |

implies and iff are root-only: they must have parentId: null and cannot be nested inside another expression.

The following diagram shows how the expression ¬(P ∧ R) → (Q ∨ S) is represented as a tree. Note the formula node — a transparent wrapper equivalent to parentheses — and that implies must be the root:

flowchart TD
    IMP["→ implies\n(root-only, binary)"]

    IMP --> NOT["¬ not\n(unary)"]
    IMP --> OR["∨ or\n(variadic, ≥ 2)"]

    NOT --> FRM["( ) formula\n(transparent wrapper,\nexactly 1 child)"]

    FRM --> AND["∧ and\n(variadic, ≥ 2)"]

    AND --> P["P\n(variable)"]
    AND --> R["R\n(variable)"]

    OR --> Q["Q\n(variable)"]
    OR --> S["S\n(variable)"]

    style IMP fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style NOT fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style AND fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style OR fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style FRM fill:none,stroke:#888,stroke-dasharray: 5 5
    style P fill:#f5f5f5,stroke:#666,color:#1a1a1a
    style R fill:#f5f5f5,stroke:#666,color:#1a1a1a
    style Q fill:#f5f5f5,stroke:#666,color:#1a1a1a
    style S fill:#f5f5f5,stroke:#666,color:#1a1a1a

Argument roles

To evaluate or check an argument, premises must be assigned roles:

• Conclusion — the single premise whose truth is being argued for. Set with ArgumentEngine.setConclusionPremise(). The first premise added to an engine is automatically designated as the conclusion if none is set; explicit setConclusionPremise() overrides this.
• Supporting — any inference premise (root is implies or iff) that is not the conclusion is automatically considered supporting. There is no explicit method to add or remove supporting premises.

A premise that is neither supporting nor the conclusion and whose type is "constraint" is automatically used to filter admissible variable assignments during validity checking.

The following diagram shows how premises, roles, and shared variables compose an argument:

flowchart TD
    ARG["Argument"]

    ARG --> P1["Premise 1\n<b>Conclusion</b>\n(inference: root is →)"]
    ARG --> P2["Premise 2\n<b>Supporting</b>\n(inference: root is ↔)"]
    ARG --> P3["Premise 3\n<b>Constraint</b>\n(root is ∧)"]

    subgraph Shared["Shared Variables"]
        VP["P"]
        VQ["Q"]
        VR["R"]
    end

    P1 -.- VP
    P1 -.- VQ
    P2 -.- VQ
    P2 -.- VR
    P3 -.- VP
    P3 -.- VR

    note1["Conclusion: set via setConclusionPremise()\nFirst premise auto-designated if not set"]
    note2["Supporting: any inference premise\nthat is not the conclusion (derived)"]
    note3["Constraint: any non-inference premise (derived)"]

    P1 ~~~ note1
    P2 ~~~ note2
    P3 ~~~ note3

    style P1 fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style P2 fill:#e8f4fd,stroke:#2196f3,color:#1a1a1a
    style P3 fill:#fff3e0,stroke:#ff9800,color:#1a1a1a
    style Shared fill:none,stroke:#888,stroke-dasharray: 5 5
    style note1 fill:none,stroke:none
    style note2 fill:none,stroke:none
    style note3 fill:none,stroke:none

PropositCore

PropositCore is the recommended top-level entry point. It creates and wires together every library and provides unified cross-library operations:

import { PropositCore } from "@proposit/proposit-core"

const core = new PropositCore()

// Create a normal claim in the global claim library
const claim = core.claims.create({
    id: "claim-1",
    type: "normal",
    text: "All men are mortal",
})

// Create a citation claim (the v0.10.0 replacement for the former Source entity)
const citationClaim = core.claims.create({
    id: "citation-1",
    type: "citation",
    text: "Aristotle, Categories, ~350 BCE",
})

// Cite the citation claim as supporting the normal claim
core.citations.add({
    id: "edge-1",
    claimId: claim.id,
    claimVersion: claim.version,
    supportingClaimId: citationClaim.id,
    supportingClaimVersion: citationClaim.version,
})

// Create an argument engine — libraries are wired automatically
const engine = core.arguments.create({
    id: "arg-1",
    version: 0,
    title: "Socrates is mortal",
    description: "",
})

// Fork the argument — clones claims (including citation-typed ones) + citation edges, records provenance
const { engine: forked, remapTable } = core.forkArgument("arg-1", "arg-2")

// Diff with automatic fork-aware entity matching
const diff = core.diffArguments("arg-1", "arg-2")

// Snapshot the entire system state
const snapshot = core.snapshot()
const restored = PropositCore.fromSnapshot(snapshot)

PropositCore is designed for subclassing. All library fields (claims, citations, axioms, origins, forks, arguments) are public and readable. Pass pre-constructed library instances via TPropositCoreOptions to inject custom implementations.

A snapshot written before origin data existed carries no origins slot. PropositCore.fromSnapshot restores such a payload with an empty origin library rather than refusing it.

No application metadata

The core library does not deal in user IDs, timestamps, or display text. These are application-level concerns. The CLI adds some metadata (e.g., createdAt, publishedAt) for its own purposes, but the core schemas are intentionally minimal. Applications extend core entity types via generic parameters.

An origin document's text is the one string the core schemas carry that a reader might mistake for display text. It is not: core stores it, digests it, measures it, and slices it by index, and never parses, renders, formats, or interprets it. What core owns is the structure around it — entity identity, the anchor relation, checksum participation, and snapshot round-tripping — exactly as it owns a citation claim's identity while the IEEE extension owns its reference data. Who pasted the text, when, whether they may share it, how it renders, and how long it may be all remain application concerns.

Claims, citations, and axioms

Every claim in the unified ClaimLibrary carries an immutable type: 'normal' | 'citation' | 'axiomatic' discriminator set at creation:

• Normal claims (type: 'normal') are primary-reasoning propositions referenced by an argument's variables.
• Citation claims (type: 'citation') represent external/cited content — papers, articles, URLs. They are the v0.10.0 unified replacement for the former separate Source entity. Application schemas (e.g. the IEEE extension) extend citation claims with structured reference data.
• Axiomatic claims (type: 'axiomatic', added in v0.12.0) represent self-evident propositions invoked as the bottom-level "proof" of a derived claim's truth — propositions that hold by definition, by historical convention, or by logical necessity. Axiomatic claim-bound variables are forced to true during evaluation (see "Evaluation semantics by claim type" below). Application layers attach a reason discriminator via the open additionalProperties slot — for example, the CLI schema requires reasonCode: 'true-by-definition' | 'historically-established' | 'logically-required'.

Two parallel connection libraries track the support edges between claims:

• ClaimCitationLibrary<TCitation> — stores citation connections (claimId → supportingClaimId). The supporting-side endpoint must reference a claim with type: 'citation'. ClaimCitationLibrary validates both endpoints, the supporting-side type, and global-graph acyclicity on add().
• ClaimAxiomLibrary<TAxiom> (v0.12.0) — stores axiom-invocation connections (claimId → supportingClaimId). The supporting-side endpoint must reference a claim with type: 'axiomatic' and the dependent-side endpoint must reference a claim with type: 'normal'. ClaimAxiomLibrary skips cycle detection — cycles are structurally impossible because axiomatic claims cannot appear on the dependent side.

Both libraries implement a generic TClaimConnectionLibraryManagement interface (add, remove, get, getAll, getConnectionsForClaim, filter, snapshot, validate), so consumers can write code that works against either flavour.

Connections are immutable (create or delete, no update). Each connection pins both endpoints to specific claim versions. They live on PropositCore as core.citations and core.axioms.

The @proposit/proposit-core/extensions/citations/ieee subpath export provides IEEECitationClaimSchema — an extended citation-claim type with IEEE reference schemas covering 33 reference types. The @proposit/proposit-core/extensions/citations/unparsed subpath export provides UnparsedCitationSchema — an extracted-but-not-yet-structured citation (text + a guessed reference type + optional url).

Evaluation semantics by claim type

Claim-bound variables evaluate differently depending on the bound claim's type:

| Claim type | Evaluation behavior | Caller override | | ----------- | ----------------------------------- | -------------------------------------------- | | normal | Caller assigns; unassigned → null | Yes — standard | | citation | Caller assigns; unassigned → null | Yes — standard | | axiomatic | Forced to true | No — caller attempts are rejected pre-flight |

Citations and normal claims continue to require explicit assignment. Apps that want auto-true defaults for citations implement that policy at their own layer. Axiomatic claim-bound variables are forced to true by a pre-pass in ArgumentEngine.evaluate and ArgumentEngine.checkValidity; a caller assignment for an axiomatic-bound variable raises AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN before evaluation runs.

To express "this derivation should NOT be supported by this axiom," wrap the axiom's variable expression in the antecedent with not (toggleNegation). Because the axiom's value is fixed at true, the negated reference contributes false to its parent operator — the standard expression-tree negation, no new mechanism. The consequent variable expression is protected by assertNotConsequentExpression and cannot be negated.

Derivation Premises

Every premise carries an immutable type discriminator:

• Freeform (type: "freeform") — the classic premise with no shape constraints beyond Structural data integrity. Allows any well-formed expression tree.
• Derivation (type: "derivation") — a shape-constrained premise that commits to deriving a specific named claim. Requires a derivedClaimId at creation time.

A derivation premise's expression tree is constrained Structurally (S-14) to a root operator in { variable, implies, iff } and Derivable-ly (D-1) to one of two canonical shapes:

• Naked-Q — a single variable expression at the root, bound to derivedClaimId. This is the initial state created automatically on createPremise({ type: "derivation", derivedClaimId }) and represents "no support given yet." Naked-Q is a valid Derivable state — validate('derivable') does not flag it. (Whether a naked-Q premise should be populated is an application-layer UX concern in proposit-server.)
• Populated form — root IMPLIES with the consequent at position 1, and the antecedent being either a single claim variable (D-2) or OR of same-grounding-kind claim variables (D-3 — no mixing of citation and axiom claim variables in a single antecedent). At Presentable the OR is wrapped in a formula buffer (IMPLIES(formula(OR(c, c, ...)), Q)) per P-1.

IFF is structurally allowed at a derivation premise's root (S-14, preserving the existing two-way-propagation evaluation feature for programmatic / CLI consumers) but is flagged as a Derivable violation (D-1 restricts the populated form to IMPLIES).

import { PropositCore } from "@proposit/proposit-core"

const core = new PropositCore()

// Create the claim to be derived
const claim = core.claims.create({ type: "normal", text: "It rains" })

// Create a citation claim (external support)
const citeA = core.claims.create({
    type: "citation",
    text: "Weather report, 2024",
})

// Add a citation connection: claim is supported by citeA
core.citations.add({
    id: "edge-1",
    claimId: claim.id,
    claimVersion: claim.version,
    supportingClaimId: citeA.id,
    supportingClaimVersion: citeA.version,
})

const engine = core.arguments.create({
    id: "arg-1",
    version: 0,
    title: "Rain argument",
    description: "",
})

// Create a derivation premise — auto-initializes to naked-Q form
const { result: pm } = engine.createPremise({
    type: "derivation",
    derivedClaimId: claim.id,
})

// Populate from citations (factory; atomic replacement of the naked-Q tree)
const result = engine.populateFromCitations(pm.getId(), core.citations)
// result = { kind: 'populated' | 'no-op', state, resolved? }

populateFromCitations and populateFromAxioms are the recommended way to build a derivation premise's antecedent from the relevant connection library. Each method operates on one grounding kind (D-3 forbids mixing) and is a factory — it constructs the fully-populated tree (IMPLIES(c, Q) for n = 1; IMPLIES(OR(c1, …, cn), Q) for n ≥ 2) and atomically replaces the existing naked-Q tree. If the premise is already populated, the factory no-ops and returns the existing state — D-3 is non-Structural, so mutations never throw on it. The UI explicitly confirms with the user (and clears the antecedent via a repair primitive) before switching grounding kinds, satisfying the no-changes-without-consent principle.

For mid-edit cases where a single command should populate from whichever support kind exists, the CLI's premises populate-supports command runs populateFromCitations first, then populateFromAxioms on the result — citations take effect when present, otherwise axioms do, matching the D-3 "no mixing" rule.

Auto-variable creation

When a premise is created via createPremise() or createPremiseWithId(), the engine automatically creates a premise-bound variable for it. This variable allows other premises in the same argument to reference the premise's truth value in their expression trees without manual variable setup.

The auto-created variable gets a symbol from an optional symbol parameter, or an auto-generated one ("P0", "P1", ...) with collision avoidance. The variable is included in the returned changeset.

Argument forking

An argument can be forked via PropositCore.forkArgument() to create an independent copy — useful for responding to, critiquing, or expanding on another author's argument. Forking:

• Creates a new argument with a new ID (version 0)
• Assigns new UUIDs to all premises, expressions, and variables
• Walks the combined citation + axiom connection graph from the source argument's claim-bound variables (a single BFS that consults both core.citations and core.axioms at each frontier pop) and clones every reachable claim ('normal', 'citation', and 'axiomatic') plus both kinds of connections between them
• Creates fork records in all five ForkLibrary namespaces (arguments, premises, expressions, variables, claims)
• Remaps all internal references (expression parent chains, variable bindings, conclusion role, claim references)
• Registers the new engine in ArgumentLibrary
• Returns the new engine, a remap table, a claim remap map (covering normal, citation, and axiomatic claims), and the argument fork record

The forked argument is fully independent — mutations don't affect the source. Fork-aware diffing is automatic via PropositCore.diffArguments(), which uses ForkLibrary records as entity matchers rather than ID-based pairing.

Subclasses can override the public canFork() method to restrict which arguments may be forked (e.g., only published versions). For low-level forking without orchestration, use the standalone forkArgumentEngine() function.

Cross-argument variable binding

A variable can reference a premise in a different argument via bindVariableToExternalPremise(). This enables structured inter-argument reasoning — for example, Rich's response to John's argument can reference John's premises as variables.

External bindings are evaluator-assigned: during evaluation they behave like claim-bound variables (the evaluator provides truth values in the assignment). The binding is navigational — it tells readers where the proposition is defined, but the engine doesn't resolve across argument boundaries. External bindings are included as free variables in truth-table generation.

bindVariableToArgument() is a convenience for binding to another argument's conclusion premise — the caller provides the conclusion premise ID and the method delegates to bindVariableToExternalPremise().

Subclasses can override the protected canBind() method to restrict which external arguments may be referenced (e.g., only published versions).

Each expression carries:

| Field | Type | Description | | ----------------- | ---------------- | ---------------------------------------------------------- | | id | string | Unique identifier. | | argumentId | string | Must match the engine's argument. | | argumentVersion | number | Must match the engine's argument version. | | premiseId | string | ID of the premise this expression belongs to. | | parentId | string \| null | ID of the parent operator, or null for root nodes. | | position | number | Numeric position among siblings (midpoint-based ordering). |

Usage

Creating an engine and premises

import { ArgumentEngine, POSITION_INITIAL } from "@proposit/proposit-core"
import type { TPropositionalExpression } from "@proposit/proposit-core"

// The constructor accepts an argument without checksum — it is computed lazily.
const argument = {
    id: "arg-1",
    version: 1,
    title: "Modus Ponens",
    description: "",
}

const eng = new ArgumentEngine(argument)

const { result: premise1 } = eng.createPremise("P implies Q") // PremiseEngine
const { result: premise2 } = eng.createPremise("P")
const { result: conclusion } = eng.createPremise("Q")

Adding variables and expressions

// Variables are passed without checksum — checksums are computed lazily.
const varP = {
    id: "var-p",
    argumentId: "arg-1",
    argumentVersion: 1,
    symbol: "P",
}
const varQ = {
    id: "var-q",
    argumentId: "arg-1",
    argumentVersion: 1,
    symbol: "Q",
}

// Register variables once on the engine — they are shared across all premises
eng.addVariable(varP)
eng.addVariable(varQ)

// Premise 1: P → Q
premise1.addExpression({
    id: "op-implies",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "operator",
    operator: "implies",
    parentId: null,
    position: POSITION_INITIAL,
})
premise1.addExpression({
    id: "expr-p1",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-p",
    parentId: "op-implies",
    position: 0,
})
premise1.addExpression({
    id: "expr-q",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-q",
    parentId: "op-implies",
    position: 1,
})

console.log(premise1.toDisplayString()) // (P → Q)

// Premise 2: P
premise2.addExpression({
    id: "expr-p2",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-p",
    parentId: null,
    position: POSITION_INITIAL,
})

// Conclusion: Q
conclusion.addExpression({
    id: "expr-q2",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-q",
    parentId: null,
    position: POSITION_INITIAL,
})

Setting roles

// The first premise created is automatically designated as the conclusion.
// Supporting premises are derived automatically — any inference premise
// (root is implies/iff) that isn't the conclusion is automatically supporting.
// Use setConclusionPremise to override the auto-assigned conclusion:
eng.setConclusionPremise(conclusion.getId())

Mutation results

All mutating methods on PremiseEngine and ArgumentEngine return TCoreMutationResult<T>, which wraps the direct result with an entity-typed changeset:

const { result: pm, changes } = eng.createPremise("My premise")
// pm is a PremiseEngine
// changes.premises?.added contains the new premise data

const { result: expr, changes: exprChanges } = pm.addExpression({
    id: "expr-1",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-p",
    parentId: null,
    position: POSITION_INITIAL,
})
// exprChanges.expressions?.added contains the new expression

Evaluating an argument

The evaluation pipeline proceeds as follows:

flowchart LR
    IN["Input\n(variable ID → true/false/null\n+ operator decisions)"]

    IN --> VAL{"validateEvaluability()"}

    VAL -->|"fail"| FAIL["{ ok: false }\nvalidation errors"]
    VAL -->|"pass"| CON["Evaluate\nConstraint\nPremises"]

    CON --> ADM{"Admissible?\n(three-valued)"}

    ADM -->|"true"| SUP["Evaluate\nSupporting\nPremises"]
    ADM -->|"false/null"| INADM["Not admissible\n(skip)"]

    SUP --> SUPR{"All supporting\ntrue?\n(three-valued)"}

    SUPR -->|"true"| CONC["Evaluate\nConclusion"]
    SUPR -->|"false/null"| NONCE["Not a\ncounterexample"]

    CONC --> CONCR{"Conclusion\ntrue?\n(three-valued)"}

    CONCR -->|"false"| CE["Counterexample\n(admissible + all supporting\ntrue + conclusion false)"]
    CONCR -->|"true/null"| NONCE2["Not a\ncounterexample"]

    subgraph Validity["Validity Check (all 2ⁿ assignments)"]
        direction LR
        VALID["No counterexamples\namong admissible\nassignments → Valid"]
    end

    CE --> Validity
    NONCE --> Validity
    NONCE2 --> Validity
    INADM --> Validity

    style FAIL fill:#ffebee,stroke:#f44336,color:#1a1a1a
    style CE fill:#ffebee,stroke:#f44336,color:#1a1a1a
    style NONCE fill:#e8f5e9,stroke:#4caf50,color:#1a1a1a
    style NONCE2 fill:#e8f5e9,stroke:#4caf50,color:#1a1a1a
    style INADM fill:#f5f5f5,stroke:#888,color:#1a1a1a
    style VALID fill:#e8f5e9,stroke:#4caf50,color:#1a1a1a
    style Validity fill:none,stroke:#888,stroke-dasharray: 5 5

Assignments use TCoreExpressionAssignment, which carries both variable truth values (three-valued: true, false, or null for unknown) and the reader's operator decisions ("accepted", "rejected", or absent).

An operator decision is not a truth value. "accepted" grants the step, so propagation may derive values through it. "rejected" withholds the step and strikes the whole premise the operator lives in from the evaluated set — it asserts nothing, and never forces the expression or its children to false. The conclusion premise and derivation premises are never struck; a struck premise is still evaluated and still returned, so you can render it crossed out.

const result = eng.evaluate({
    variables: { "var-p": true, "var-q": true },
    operatorAssignments: {},
})
if (result.ok) {
    console.log(result.conclusionTrue) // true
    console.log(result.survivingSupportingPremisesTrue) // true
    console.log(result.premisesHoldConclusionFalse) // false
    console.log(result.struckPremiseIds) // []
    console.log(result.conclusionAttribution) // { assertedByReader: …, reachedWithoutAssertion: … }
}

Evaluation emits orthogonal facts, not a single named outcome, and the library ships no label strings — composing a reading is the consumer's job. Two facts are easy to conflate and must not be: survivingSupportingPremisesTrue is vacuously true when every supporting premise has been struck, so whether the argument reached its conclusion is conclusionAttribution.reachedWithoutAssertion — which withholds the reader's own assignments and recomputes the derivation from what is left. See docs/api-reference.md → Evaluation facts for the full set, including per-value provenance and premise-set satisfiability.

Checking validity

const validity = eng.checkValidity()
if (validity.ok) {
    console.log(validity.isValid) // true (Modus Ponens is valid)
    console.log(validity.counterexamples) // []
}

Using with React

ArgumentEngine implements the useSyncExternalStore contract, so it works as a React external store with no additional dependencies:

import { useSyncExternalStore } from "react"
import { ArgumentEngine } from "@proposit/proposit-core"

// Create the engine outside of React (or in a ref/context)
const engine = new ArgumentEngine({ id: "arg-1", version: 1 })

function ArgumentView() {
    // Subscribe to the full snapshot
    const snapshot = useSyncExternalStore(engine.subscribe, engine.getSnapshot)

    return (
        <div>
            <h2>Variables</h2>
            <ul>
                {Object.values(snapshot.variables).map((v) => (
                    <li key={v.id}>{v.symbol}</li>
                ))}
            </ul>
            <h2>Premises</h2>
            {Object.entries(snapshot.premises).map(([id, p]) => (
                <div key={id}>
                    Premise {id} — {Object.keys(p.expressions).length}{" "}
                    expressions
                </div>
            ))}
        </div>
    )
}

For fine-grained reactivity, select a specific slice — React skips re-rendering if the reference is unchanged thanks to structural sharing:

function ExpressionView({
    premiseId,
    expressionId,
}: {
    premiseId: string
    expressionId: string
}) {
    // Only re-renders when THIS expression changes
    const expression = useSyncExternalStore(
        engine.subscribe,
        () =>
            engine.getSnapshot().premises[premiseId]?.expressions[expressionId]
    )

    if (!expression) return null
    return (
        <span>
            {expression.type === "variable"
                ? expression.variableId
                : expression.operator}
        </span>
    )
}

Mutations go through the engine as usual — subscribers are notified automatically:

function AddVariableButton() {
    return (
        <button
            onClick={() => {
                engine.addVariable({
                    id: crypto.randomUUID(),
                    argumentId: "arg-1",
                    argumentVersion: 1,
                    symbol: "R",
                })
            }}
        >
            Add variable R
        </button>
    )
}

Inserting an expression into the tree

insertExpression splices a new node between existing nodes. The new expression inherits the anchor node's current slot in the tree (leftNodeId ?? rightNodeId).

// Extend  P → Q  into  (P ∧ R) → Q  by inserting an `and` above expr-p1.
const varR = {
    id: "var-r",
    argumentId: "arg-1",
    argumentVersion: 1,
    symbol: "R",
}
eng.addVariable(varR)
premise1.addExpression({
    id: "expr-r",
    argumentId: "arg-1",
    argumentVersion: 1,
    type: "variable",
    variableId: "var-r",
    parentId: null,
    position: POSITION_INITIAL,
})
premise1.insertExpression(
    {
        id: "op-and",
        argumentId: "arg-1",
        argumentVersion: 1,
        type: "operator",
        operator: "and",
        parentId: null, // overwritten by insertExpression
        position: POSITION_INITIAL,
    },
    "expr-p1", // becomes child at position 0
    "expr-r" // becomes child at position 1
)

console.log(premise1.toDisplayString()) // ((P ∧ R) → Q)

Removing expressions

Removing an expression also removes its entire descendant subtree. After the subtree is gone, ancestor operators left with fewer than two children are automatically collapsed:

• 0 children remaining — the operator is deleted; the check recurses upward.
• 1 child remaining — the operator is deleted and that child is promoted into the operator's former slot.

// Remove expr-r from the and-cluster.
// op-and now has only expr-p1 → op-and is deleted, expr-p1 is promoted back
// to position 0 under op-implies.
premise1.removeExpression("expr-r")

console.log(premise1.toDisplayString()) // (P → Q)

Forking an argument

// Fork John's argument to create Rich's response
import { PropositCore } from "@proposit/proposit-core"

const core = new PropositCore()

// Create John's argument (engine registered in core.arguments)
const johnEngine = core.arguments.create({
    id: "john-arg-id",
    version: 1,
    title: "John's argument",
    description: "",
})
// ... populate with premises, variables, expressions ...

// Fork — clones claims (and citation claims) + citation edges, creates fork records, registers new engine
const { engine: richArg, remapTable } = core.forkArgument(
    "john-arg-id",
    "rich-arg-id"
)

// Rich now has a mutable copy — modify, add, or remove premises
const forkedPremiseId = remapTable.premises.get(originalPremiseId)!
richArg.removePremise(forkedPremiseId) // reject a premise
richArg.createPremise(undefined, "RichNewPremise") // add a new one

// See what Rich changed relative to John's original (fork-aware matching is automatic)
const diff = core.diffArguments("john-arg-id", "rich-arg-id")
// diff.premises.removed — premises Rich rejected
// diff.premises.added — premises Rich introduced
// diff.premises.modified — premises Rich altered

Cross-argument variable binding

// Rich's argument references a premise from John's argument
richArg.bindVariableToExternalPremise({
    id: "v-john-p2",
    argumentId: "rich-arg-id",
    argumentVersion: 0,
    symbol: "JohnP2",
    boundPremiseId: "johns-premise-2-id",
    boundArgumentId: "johns-arg-id",
    boundArgumentVersion: 2, // must be a published version
})

// Or reference John's conclusion directly
richArg.bindVariableToArgument(
    {
        id: "v-john-conclusion",
        argumentId: "rich-arg-id",
        argumentVersion: 0,
        symbol: "JohnConclusion",
        boundArgumentId: "johns-arg-id",
        boundArgumentVersion: 2,
    },
    "johns-conclusion-premise-id" // caller resolves the conclusion
)

// External bindings are evaluator-assigned — provide truth values in the assignment
const result = richArg.evaluate({
    variables: { "v-john-p2": true, "v-john-conclusion": false },
    operatorAssignments: {},
})

Invalid Constructions and How They're Handled

The engine enforces invariants at two levels:

• Mutation-time throws for Structural-tier rules (S-1..S-14 — see docs/Proposit_Grammar.md §3.1). Mutations on ArgumentEngine / PremiseEngine reject Structural violations with a thrown error.
• Validation-time violations for everything else. engine.validate('evaluable' | 'derivable' | 'presentable') returns readonly TViolation[] covering tiers up to the requested level. Mutations never throw on Evaluable, Derivable, or Presentable issues — they surface through validate(tier) and can be addressed by the AN post-hook (assistive behavior) or by user-initiated repair primitives.

The tables below list invalid constructions and what happens.

Expression tree — Structural (thrown on mutation)

| Invalid construction | What happens / rule | | -------------------------------------------------------------------------------- | -------------------------------------------------------------- | | implies or iff with parentId !== null | Throws — S-5 (root-only IMPLIES/IFF) | | Expression with parentId === id (self-parentage) | Throws — S-4 (no cycles) | | Duplicate expression ID within a premise | Throws — S-10 (EXPR_DUPLICATE_ID) | | Expression references a non-existent parentId | Throws — S-1 (FK soundness) | | Expression's parent is a variable expression | Throws — only operators and formulas can have children | | formula node with zero or more than one child | Throws — S-13 (formula unary) | | not operator with anything other than one child | Throws — S-12 (not unary) | | implies or iff with anything other than two children | Throws — S-8 (binary arity) | | Two siblings share the same position under the same parent | Throws — S-9 (sibling position uniqueness) | | insertExpression with leftNodeId === rightNodeId | Throws | | insertExpression or wrapExpression targeting a root-only operator as a child | Throws — S-5 (root-only IMPLIES/IFF) | | wrapExpression with not as the wrapping operator | Throws — not is unary; wrapping always produces two children | | Expression's argumentId/argumentVersion doesn't match the premise | Throws — S-1 (FK soundness) | | Derivation premise root operator outside { variable, implies, iff } | Throws — S-14 (DERIVATION_ROOT_OPERATOR_INVALID) |

In v1.0 the engine no longer throws on non-not operators placed as direct children of operators (the pre-1.0 enforceFormulaBetweenOperators throw). That shape is now a Presentable issue (P-1); in assistive behavior the AN post-hook inserts a formula buffer (AN-1), and in permissive behavior it surfaces via validate('presentable'). Neither mode throws.

Expression tree — Evaluable / Presentable violations (returned by validate)

| Invalid construction | Rule code | Tier | | ---------------------------------------------------------------- | --------- | ----------- | | and or or operator with fewer than 2 children | E-1 | Evaluable | | Variable binding does not resolve | E-3 | Evaluable | | Axiomatic-bound variable assignment supplied to evaluate | E-4 | Evaluable | | Derivation premise expression tree lacks the consequent variable | E-5 | Evaluable | | Claim has more than one paired derivation premise | E-6 | Evaluable | | Argument has premises but no conclusion designated | E-7 | Evaluable | | Non-not operator placed directly under another operator | P-1 | Presentable | | not(not(x)) chain in the tree | P-2 | Presentable | | formula wrapping no operator (leaf or single not) | P-3 | Presentable | | Single-child and / or | P-4 | Presentable | | Same-operator parent/grandchild separated only by formula | P-5 | Presentable | | Premise-bound variable expression marked as an enthymeme | P-6 | Presentable | | Operator or formula expression marked as an enthymeme | P-6 | Presentable |

Variables — prevented at construction time

| Invalid construction | What happens | | --------------------------------------------------------------------------------------- | ----------------------------------------------------------------------- | | Duplicate variable id | Throws | | Duplicate variable symbol | Throws | | Variable argumentId/argumentVersion doesn't match the engine | Throws | | Claim-bound variable references a non-existent claim/version | Throws | | Premise-bound variable references a non-existent premise (internal) | Throws | | Adding a premise-bound variable via addVariable() | Throws — use bindVariableToPremise or bindVariableToExternalPremise | | Circular binding (variable → premise → expression → variable, transitively) | Throws | | bindVariableToPremise with boundArgumentId !== engine.argumentId | Throws — use bindVariableToExternalPremise for cross-argument | | bindVariableToExternalPremise with boundArgumentId === engine.argumentId | Throws — use bindVariableToPremise for internal | | External binding rejected by canBind() policy | Throws | | Renaming a variable to a symbol already in use | Throws | | Changing a variable's binding type (claim → premise or vice versa) via updateVariable | Throws — delete and re-create |

Variables — detected by validation

| Invalid construction | Error code | Severity | | -------------------------------------------------- | -------------------------- | -------- | | Premise-bound variable references an empty premise | EXPR_BOUND_PREMISE_EMPTY | Warning |

Premises — Structural (thrown on mutation)

| Invalid construction | What happens / error code | | --------------------------------------------------------------------------------- | ------------------------------------------------------ | | Duplicate premise ID | Throws — S-10 | | Adding a second root expression (parentId: null) to a premise | Throws | | createPremise({ type: "derivation" }) without derivedClaimId | Throws — CREATE_DERIVATION_REQUIRES_DERIVED_CLAIM_ID | | createPremise({ type: "derivation", derivedClaimId }) when claim not in library | Throws — CREATE_DERIVATION_CLAIM_NOT_FOUND | | Setting a derivation premise's root operator to and/or/not/formula | Throws — S-14 (DERIVATION_ROOT_OPERATOR_INVALID) | | ensureClaimBoundVariable(claimId) when the claim is not in the library | Throws — CLAIM_NOT_FOUND | | Restoring a pre-v0.11 snapshot whose premises lack the type field | Throws — LEGACY_PREMISE_MISSING_TYPE |

In v1.0 there is no ManagedDerivationPremiseEngine subclass — derivation-premise canonical shape is enforced via the Derivable-tier rules (D-1..D-6, surfaced through validate('derivable')) and the new Evaluable rule E-6 (claim-derivation pairing, cardinality ≤ 1). Mutations on derivation premises go through the regular PremiseEngine and never throw on Derivable issues — they surface via validate(tier) and can be cleaned up by AN (assistive mode) or repair primitives.

Premises — Evaluable / Derivable violations (returned by validate)

| Invalid construction | Rule code | Tier | | -------------------------------------------------------------------------------------- | --------- | --------- | | Derivation premise expression tree lacks the consequent variable | E-5 | Evaluable | | Normal claim has more than one paired derivation premise | E-6 | Evaluable | | Derivation premise's populated form is not IMPLIES(c, Q) or IMPLIES(OR, Q) | D-1 | Derivable | | Derivation premise antecedent has a single citation not wrapped as IMPLIES(c, Q) | D-2 | Derivable | | Derivation premise antecedent mixes axiom-bound and citation-bound variables | D-3 | Derivable | | Variable bound to an axiomatic claim appears outside a derivation premise's antecedent | D-4 | Derivable | | Variable bound to a citation claim appears outside a derivation premise's antecedent | D-5 | Derivable | | Derivation premise has role: "conclusion" | D-6 | Derivable |

Naked-Q (a derivation premise whose tree is a single variable bound to derivedClaimId) is a valid Derivable state in v1.0 — it represents "no support given yet" and is not flagged by validate('derivable'). evaluate() and checkValidity() skip naked-Q derivation premises (they neither assert their consequent nor support its derivation); this replaces the pre-1.0 DERIVATION_STRUCTURE_INVALID_AT_EVALUATION throw. Server-side publish-time pruning deletes naked-Q derivation premises before storage, so post-publish arguments never carry them.

Argument — Evaluable violations (returned by validate)

| Invalid construction | Rule code / engine code | Tier | | ----------------------------------------------------------- | ---------------------------------------------------------------- | ---------- | | Argument has premises but no conclusion designated | E-7 (ARGUMENT_NO_CONCLUSION) | Evaluable | | Conclusion premise ID points to a non-existent premise | E-7 (ARGUMENT_CONCLUSION_NOT_FOUND) | Evaluable | | Same variable ID used with multiple symbols across premises | ARGUMENT_VARIABLE_ID_SYMBOL_MISMATCH (engine error) | — | | Same variable symbol used with multiple IDs across premises | S-11 (ARGUMENT_VARIABLE_SYMBOL_AMBIGUOUS) — thrown on mutation | Structural |

Claims, citations, and axioms — prevented at construction time

| Invalid construction | What happens / error code | | -------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------- | | Updating a claim's type field after creation | Throws — CLAIM_TYPE_IMMUTABLE | | Restoring a pre-v0.10 snapshot whose claims lack the type field | Throws — LEGACY_CLAIM_MISSING_TYPE | | Adding a citation whose id already exists | Throws — CITATION_DUPLICATE_ID | | Adding a citation whose claimId@claimVersion is not in the lookup | Throws — CITATION_CLAIM_REF_NOT_FOUND | | Adding a citation whose supportingClaimId@supportingClaimVersion is not in the lookup | Throws — CITATION_SUPPORTING_REF_NOT_FOUND | | Supporting-side claim of a citation has type !== 'citation' | Throws — CITATION_SUPPORTING_NOT_CITATION_TYPE | | Citation that would create a cycle in the global claim-citation graph | Throws — CITATION_CYCLE_DETECTED (ID-only — versions don't disambiguate) | | Calling ClaimCitationLibrary.remove(id) with an unknown id | Throws — CITATION_NOT_FOUND | | Adding an axiom connection whose id already exists | Throws — AXIOM_DUPLICATE_ID | | Adding an axiom connection whose claimId@claimVersion is not in the lookup | Throws — AXIOM_CLAIM_REF_NOT_FOUND | | Adding an axiom connection whose supportingClaimId@supportingClaimVersion is not in lookup | Throws — AXIOM_SUPPORTING_REF_NOT_FOUND | | Supporting-side claim of an axiom connection has type !== 'axiomatic' | Throws — AXIOM_SUPPORTING_NOT_AXIOMATIC_TYPE | | Dependent-side claim of an axiom connection has type !== 'normal' | Throws — AXIOM_CLAIM_NOT_NORMAL_TYPE | | Caller passes an assignment for an axiomatic-bound variable to evaluate or checkValidity | Throws — AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN (use toggleNegation to reject the axiom in the antecedent instead) | | Calling ClaimAxiomLibrary.remove(id) with an unknown id | Throws — AXIOM_NOT_FOUND | | Restoring a pre-v0.12 snapshot whose citation-library wrapper or entities use legacy fields | Throws — LEGACY_CLAIM_CITATION_SHAPE (run the v0.12 CLI migration) | | Restoring a pre-v0.12 PropositCore snapshot that lacks an axioms slot | Throws — LEGACY_MISSING_AXIOM_SLOT (run the v0.12 CLI migration) |

Removal cascades

These are not errors — they're intentional structural maintenance:

| Trigger | Cascade behavior | | ---------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | removeVariable(id) | All expressions referencing the variable are deleted across all premises, triggering operator collapse | | removePremise(id) | All variables bound to the premise are removed (which cascades to their expressions). If the premise was the conclusion, the conclusion becomes unset. | | removeExpression(id) | The expression's subtree is deleted. Ancestor operators with 0 remaining children are deleted. Operators with 1 remaining child promote that child into their slot (operator collapse). Promotions are checked against nesting and root-only rules. |

Engine behavior (assistive vs permissive)

The pre-1.0 grammarConfig / autoNormalize / enforceFormulaBetweenOperators machinery is removed in v1.0. Expression-tree shape is now driven by the four-tier grammar (Structural ⊇ Evaluable ⊇ Derivable ⊇ Presentable; see docs/Proposit_Grammar.md) together with a single engine setting:

| Setting | Default | Effect | | ------------------------ | ---------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | | behavior: "assistive" | (default) | After every successful Structural mutation, the engine runs auto-normalization (AN-1..AN-4) as a post-hook. AN preserves Presentable: if the pre-mutation state was Presentable, the post-mutation state is Presentable. | | behavior: "permissive" | (advanced) | AN does not run. Mutations execute exactly as described; the engine guarantees Structural integrity only. Evaluable / Derivable / Presentable violations surface via validate(tier) and never throw. |

Set the behavior at construction (new ArgumentEngine(arg, claims, { behavior: 'permissive' })) or at runtime (engine.setBehavior('permissive')). Switching permissive → assistive does not auto-run a global normalize() pass — the UI prompts the user explicitly before invoking it.

fromSnapshot() and fromData() accept any Structural state — there is no LOAD_GRAMMAR / STRICT_GRAMMAR split. Lower-tier violations are queryable post-load via validate(tier). The only load failure is a truly broken (non-Structural) snapshot.

API Reference

See docs/api-reference.md for the full API reference covering ArgumentEngine, PremiseEngine, standalone functions, position utilities, and types.

CLI

The package ships a command-line interface for managing arguments stored on disk.

Running the CLI

proposit-core --help

State storage

All data is stored under ~/.proposit-core by default. Override with the PROPOSIT_HOME environment variable:

PROPOSIT_HOME=/path/to/data proposit-core arguments list

The on-disk layout is:

$PROPOSIT_HOME/
  arguments/
    <argument-id>/
      meta.json          # id, title, description
      <version>/         # one directory per version (0, 1, 2, …)
        meta.json        # version, createdAt, published, publishedAt?
        variables.json   # array of TPropositionalVariable
        roles.json       # { conclusionPremiseId? }
        premises/
          <premise-id>/
            meta.json    # id, title?
            data.json    # type, rootExpressionId?, variables[], expressions[]
        <analysis>.json  # named analysis files (default: analysis.json)
  claims.json          # global claim library
  citations.json       # citation connections
  axioms.json          # axiom connections
  origins.json         # source texts, their argument links, and anchors
  forks.json           # fork provenance records

Versioning

Arguments start at version 0. Publishing marks the current version as immutable and copies its state to a new draft version. All mutating commands reject published versions.

Version selectors accepted anywhere a <version> is required:

| Selector | Resolves to | | ---------------- | -------------------------------------- | | 0, 1, … | Exact version number | | latest | Highest version number | | last-published | Highest version with published: true |

Top-level commands

proposit-core version                              Print the package version
proposit-core arguments create <title> <desc>      Create a new argument (prints UUID)
proposit-core arguments list [--json]              List all arguments
proposit-core arguments delete [--all] [--confirm] <id>   Delete an argument or its latest version
proposit-core arguments publish <id>               Publish latest version, prepare new draft
proposit-core arguments parse [text] [options]     Parse natural language into an argument via LLM
proposit-core arguments import <yaml_file>         Import an argument from YAML
proposit-core claims list [--json]                 List all claims (citation tagged [citation]; axiomatic tagged [axiom: <reasonCode>])
proposit-core claims show <claim_id> [--json]      Show all versions of a claim
proposit-core claims add [--type <t>] [--reason <code>] [--title <t>] [--body <b>]  Create a new claim ('normal' default; 'citation' for cited content; 'axiomatic' requires --reason)
proposit-core claims update <claim_id> [--title <t>] [--body <b>]  Update claim metadata (type and reasonCode are immutable)
proposit-core claims freeze <claim_id>             Freeze current version
proposit-core citations list [--json]              List all citation connections
proposit-core citations show <citation_id> [--json]  Show a single citation
proposit-core citations add --claim-id <id> --supporting-claim-id <id>  Add a citation connection (supporting claim must be type=citation)
proposit-core citations remove <citation_id>       Remove a citation connection
proposit-core axioms list [--json]                 List all axiom connections
proposit-core axioms show <connection_id> [--json] Show a single axiom connection
proposit-core axioms add --claim-id <id> --axiom-id <id>           Add an axiom connection (supporting claim must be type=axiomatic; dependent must be type=normal)
proposit-core axioms remove <connection_id>        Remove an axiom connection
proposit-core origins attach <file> --argument <id> --version <n> [--stance <s>]  Store a source text and link it to an argument version
proposit-core origins list [--json]                List stored source texts and their links
proposit-core origins show <document_id> [--json] [--text]  Show a source text, its links, and its anchors
proposit-core origins link <document_id> --argument <id> --version <n> [--stance <s>]  Link an existing source text to another argument version
proposit-core origins unlink <link_id>             Remove a link between an argument version and a source text
proposit-core origins remove <document_id>         Remove a source text (refuses while referenced)
proposit-core origins anchor add --document <id> --argument <id> --version <n> --target <type> --target-id <id> --start <n> --end <n>  Record the span an argument part derives from
proposit-core origins anchor remove <anchor_id>    Remove an anchor

Breaking change in v0.12.0. The citations command group switched from positional arguments + unlink to flag arguments + remove, matching the new axioms group and the renamed schema fields. Scripts that used citations add <citing_claim_id> <source_claim_id> or citations unlink <id> need to update to citations add --claim-id <id> --supporting-claim-id <id> and citations remove <id>.

By default delete removes only the latest version. Pass --all to remove the argument entirely. Both delete and delete-unused prompt for confirmation unless --confirm is supplied.

Axiomatic claims

Axiomatic claims (v0.12.0) represent self-evident propositions invoked as the bottom-level support for a derived claim — propositions that hold by definition, by historical convention, or by logical necessity. Create one with the --type axiomatic flag plus a required --reason <code> from one of the three preset reason codes:

• true-by-definition — the proposition is part of how a term is defined.
• historically-established — the proposition is treated as fact by long-standing convention.
• logically-required — the proposition follows from logical structure alone.

proposit-core claims add --type axiomatic --reason true-by-definition \
    --title "All bachelors are unmarried"

The reasonCode is set at creation time and is immutable — claims update rejects --reason as an unknown option. Listings tag axiomatic claims with [axiom: <reasonCode>].

Use the axioms command group to wire an axiomatic claim into a normal claim's support set. The supporting endpoint must be type=axiomatic; the dependent endpoint must be type=normal. There is no acyclicity check — axiomatic claims cannot appear on the dependent side, so cycles are structurally impossible.

proposit-core axioms add --claim-id <normal-claim-id> --axiom-id <axiomatic-claim-id>

Axiomatic claim-bound variables are forced to true at evaluation time. Passing an explicit assignment for one to analysis evaluate raises AXIOM_VARIABLE_ASSIGNMENT_FORBIDDEN before the evaluator runs. To express "this derivation should not be supported by this axiom," wrap the axiom's variable expression in the antecedent with not.

Origin data

An argument can record the source text it was built from, which of its parts derive from which span of that text, and which parts the original left unspoken.

# Store a source text and link it to an argument version.
DOC=$(proposit-core origins attach ./speech.txt --argument "$ARG" --version 0 --stance seed)

# Record that a premise derives from code points [0, 12) of that text.
proposit-core origins anchor add --document "$DOC" --argument "$ARG" \
    --version 0 --target premise --target-id "$PREMISE" --start 0 --end 12

proposit-core origins show "$DOC"

Stance. seed (the default) says the argument merely started from the source. representation asserts the argument faithfully renders it — which is what makes the absence of provenance meaningful, so it is a claim about someone else's text and never a default.

Positions count Unicode code points, not UTF-16 code units, following the Web Annotation Data Model. The fields are named startCodePoint / endCodePoint for that reason, and sliceByCodePoints is the exported helper that reads them; a plain String.prototype.slice on these offsets is wrong for any text containing an astral-plane character and right for every ASCII test. An anchor whose span does not slice out its own recorded quote is rejected, so a mis-measured anchor fails loudly instead of highlighting the wrong passage.

The stored text is normalized on the way in by the exported normalizeOriginText: every line-break form folds to LF, the byte-order mark, control characters other than LF and tab, bidirectional controls, zero-width characters, and stray variation selectors are stripped, and the result is composed to Unicode NFC and trimmed. Emoji ZWJ, keycap, CJK, Mongolian, and emoji-tag sequences survive intact. It never touches content: internal whitespace, paragraph breaks, smart quotes, dashes, case, and punctuation are left exactly as written. The function is idempotent, so an application may safely apply it at its own import boundary as well.

Because every stored anchor is an offset into text this function produced, changing its behavior later is a data migration, not a bug fix.

Each document also carries a SHA-256 digest of its normalized text, so two pastes of the same source are detectable. Two texts differing only in line-ending style, a byte-order mark, or accent composition produce the same digest.

Anchoring requires a link first: an anchor's argument version must already be linked to the document, because the link carries the stance that gives the anchor its meaning. Persist in that order — document, link, anchors.

Unspoken content. An author can mark a premise or a claim-bound variable expression as an enthymeme — content the natural-language original left for the audience to supply:

proposit-core "$ARG" latest premises update "$PREMISE" --enthymeme
proposit-core "$ARG" latest expressions mark "$PREMISE" "$EXPR" --enthymeme

The mark is always declared, never derived; nothing infers it. Passing --no-enthymeme removes the field entirely rather than storing false, which restores the entity's original checksum. Marking a premise-bound variable is reported as P-6 by validate('presentable') — its truth is derived from another premise rather than asserted, so there is nothing for a speaker to have suppressed.

Origin data lives on PropositCore as core.origins and is stored by the CLI in $PROPOSIT_HOME/origins.json.

Version-scoped commands

All commands below are scoped to a specific argument version:

proposit-core <argument_id> <version> <group> <subcommand> [args] [options]

show

proposit-core <id> <ver> show [--json]

Displays argument metadata (id, title, description, version, createdAt, published, publishedAt).

render

proposit-core <id> <ver> render

Renders the full argument with metadata. Output includes:

• Argument header — title and description
• Premises — one per line with formula display string and title (if present); conclusion marked with *
• Variables — symbol and bound claim title (or premise binding)
• Claims — ID, version, frozen status, type (normal, citation, o