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 six supported operators and their arities are:

| Operator | Symbol | Arity | | --------- | ------ | -------------- | | not | ¬ | unary (= 1) | | and | ∧ | variadic (≥ 2) | | or | ∨ | variadic (≥ 2) | | xor | ⊻ | 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. Core claims carry no
// text — see "No application metadata" for adding fields of your own.
const claim = core.claims.create({ id: "claim-1", type: "normal" })

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

// 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 })

// 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.

With the default type parameters, TypeScript rejects keys beyond the core fields in an object literal — core.claims.create({ type: "normal", text: "…" }) or core.arguments.create({ id, version, title }) does not compile. Widen the types to add fields of your own:

import { PropositCore } from "@proposit/proposit-core"
import type {
    TCoreArgument,
    TCoreClaim,
    TCorePremise,
    TCorePropositionalExpression,
    TCorePropositionalVariable,
} from "@proposit/proposit-core"

type TMyArgument = TCoreArgument & { title: string }
type TMyClaim = TCoreClaim & { text: string }
// Type parameters, in order: argument, premise, expression, variable, claim, …
const core = new PropositCore<
    TMyArgument,
    TCorePremise,
    TCorePropositionalExpression,
    TCorePropositionalVariable,
    TMyClaim
>()
const claim = core.claims.create({ type: "normal", text: "All men are mortal" })
const engine = core.arguments.create({
    id: "arg-1",
    version: 0,
    title: "Mortality",
})

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. Every author field takes either a personal name (givenNames, familyName, optional suffix) or a single name rendered as written ({ name }), for an organisation such as Reuters or a one-part name such as Aristotle. Reference dates other than access dates are calendar dates (CalendarDate): strings such as "1787", "1787-11" or "1787-11-22", rendered at their precision and never moved by a time zone; a source with no year renders "(n.d.)". 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 a user-interface concern for the consuming application.)
• 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" })

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

// 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 })

// 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).
// The first parameter is the derived claim's id, not the premise id.
const result = engine.populateFromCitations(claim.id, 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,
    ClaimLibrary,
    POSITION_INITIAL,
} from "@proposit/proposit-core"

// Variables stand for claims, so the engine needs a claim lookup.
const claims = new ClaimLibrary()
const claimP = claims.create({ type: "normal" })
const claimQ = claims.create({ type: "normal" })

// new ArgumentEngine(argument, claimLookup, options?). The argument is passed
// without checksum — it is computed lazily.
// Build in "permissive" behavior: in the default "assistive" behavior the
// engine tidies the tree after every mutation and removes an operator that
// has no children yet, so its children could not be attached one by one.
const eng = new ArgumentEngine({ id: "arg-1", version: 1 }, claims, {
    behavior: "permissive",
})

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

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",
    claimId: claimP.id,
    claimVersion: claimP.version,
}
const varQ = {
    id: "var-q",
    argumentId: "arg-1",
    argumentVersion: 1,
    symbol: "Q",
    claimId: claimQ.id,
    claimVersion: claimQ.version,
}

// 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,
    premiseId: premise1.getId(),
    type: "operator",
    operator: "implies",
    parentId: null,
    position: POSITION_INITIAL,
})
premise1.addExpression({
    id: "expr-p1",
    argumentId: "arg-1",
    argumentVersion: 1,
    premiseId: premise1.getId(),
    type: "variable",
    variableId: "var-p",
    parentId: "op-implies",
    position: 0,
})
premise1.addExpression({
    id: "expr-q",
    argumentId: "arg-1",
    argumentVersion: 1,
    premiseId: premise1.getId(),
    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,
    premiseId: premise2.getId(),
    type: "variable",
    variableId: "var-p",
    parentId: null,
    position: POSITION_INITIAL,
})

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

// The trees are complete: return to "assistive" behavior and tidy once.
eng.setBehavior("assistive")
eng.normalize()

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()
// 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,
    premiseId: pm.getId(),
    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. Derivation premises are also not counted among the supporting premises: survivingSupportingPremisesTrue and survivingSupportingPremiseCount range over authored support only, so a reader's answer about a claim the argument reaches only through its citation does not move them.

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, ClaimLibrary } from "@proposit/proposit-core"

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

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={() => {
                const claim = claims.create({ type: "normal" })
                engine.addVariable({
                    id: crypto.randomUUID(),
                    argumentId: "arg-1",
                    argumentVersion: 1,
                    symbol: "R",
                    claimId: claim.id,
                    claimVersion: claim.version,
                })
            }}
        >
            Add variable R
        </button>
    )
}

Inserting an expression into the tree

insertExpression(expression, leftNodeId?, rightNodeId?) splices a new node above nodes already in the tree. The new expression inherits the anchor node's current slot in the tree (leftNodeId ?? rightNodeId). A premise has exactly one root, so a new node cannot first be added loose and then spliced in; to add a new node and a new operator together, use wrapExpression(operator, newSibling, leftNodeId?, rightNodeId?), which puts the operator in the existing node's slot with the existing node and the new sibling as its children.

// Extend  P → Q  into  (P ∧ R) → Q  by wrapping expr-p1 in an `and`.
const claimR = claims.create({ type: "normal" })
eng.addVariable({
    id: "var-r",
    argumentId: "arg-1",
    argumentVersion: 1,
    symbol: "R",
    claimId: claimR.id,
    claimVersion: claimR.version,
})
premise1.wrapExpression(
    {
        id: "op-and",
        argumentId: "arg-1",
        argumentVersion: 1,
        premiseId: premise1.getId(),
        type: "operator",
        operator: "and",
        parentId: null, // set by wrapExpression
    },
    {
        id: "expr-r",
        argumentId: "arg-1",
        argumentVersion: 1,
        premiseId: premise1.getId(),
        type: "variable",
        variableId: "var-r",
        parentId: null, // set by wrapExpression
    },
    "expr-p1" // the existing node, which becomes the left child
)

// In assistive behavior a formula buffer is added between → and ∧.
console.log(premise1.toDisplayString()) // (((P ∧ R)) → Q)

Removing expressions

removeExpression(id, deleteSubtree) with deleteSubtree: true removes the expression and its entire descendant subtree (with false, it removes only the expression and promotes its single child). The method does not collapse the parent itself; in the default assistive behavior the post-mutation tidying (AN-3) then collapses ancestor operators left with fewer than two children:

• 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.

In permissive behavior the under-filled operator stays and is reported by validate('evaluable') (E-1).

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

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-15 — 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 xor 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 | | Standard 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 / xor | 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 | | Changing an expression-bound variable's binding fields, or its kind, via updateVariable | Throws — rebase the response to re-point it | | Stored variable with more than one kind of reference (claim, premise, expression) | Fails to load — VAR_BINDING_AMBIGUOUS |

Variables — detected by validation

| Invalid construction | Error code | Severity | | ----------------------------------------------------------------------- | -------------------------- | -------- | | Premise-bound variable references an empty premise of the same argument | 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 |

Response arguments

A response carries respondsTo and answers that argument through links (see docs/api-reference.md). A reader's agreement with a response's links is carried into the argument it answers with carryAnswers and mergeCarriedInput; a link that cannot be carried exactly is reported, never thrown on (see "Carrying a reader's answers" there).

| Invalid construction | What happens / code | | -------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------ | | respondsTo naming the argument itself | Throws on construction; fails to load — S-15 (ARG_RESPONDS_TO_ITSELF) | | Expression-bound variable in a standard argument, or bound into another argument | Throws; fails to load — S-15 (ARG_EXPRESSION_BINDING_OUTSIDE_RESPONSE) | | bindVariableToExpression outside a response, on another version, or refused by canBind() | Throws | | setConclusionPremise on a response | Throws | | setExtras given respondsTo | Throws | | evaluate / checkValidity on a response | ok: false — ARGUMENT_IS_RESPONSE | | Response stored with a conclusion | Loads; E-8 (Evaluable). clearConclusionPremise() clears it | | Two variables binding the same expression in the same aspect | Loads; E-9 (Evaluable) | | Binding on another version of the argument answered | Loads; E-10 (Evaluable); validateLinks reports LINK_VERSION_MISMATCH | | Bound expression absent from the target snapshot; inference binding on a non-operator | validateLinks reports it; checkLink and checkResponseCoherent answer invalid | | rebaseResponse missing a decision, or with one it cannot carry out | Throws; the response is unchanged |

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, true) | The expression's subtree is deleted. In assistive behavior, ancestor operators with 0 remaining children are then deleted and operators with 1 remaining child promote that child into their slot (operator collapse); in permissive behavior they are left for validate('evaluable') to report. |

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. Response arguments are a library feature that the CLI does not store: no command creates one, and its storage keeps no respondsTo or expression-bound variables.

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 names: analysis-1.json, analysis-2.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-