Use similar idea, but everything should be built from links and references

[konard]

We need to find a way to build everything need to reason about types and so on based on idea of https://softwarefoundations.cis.upenn.edu/sf-3.2/Logic.html expressed in pure links/references (and fully defined), that in addition to already supported features. So everything that is working continue to work, we just add a way to override/redefine in other terms these root constructs.

[netkeep80]

Implementation comment for issue #97

I think this issue should be treated not as an additional experimental feature, but as a foundational implementation task for the prover/kernel.

The current RML design already moves in the right direction: it treats operators, truth constants, ranges, valence, aggregators, type facts, lambda facts, and proof links as configurable runtime data. The self-bootstrap layer also starts encoding grammar, evaluator, type layer, operators, and metatheorem checker as links.

However, there is still an important gap between:

1. RML as a host-implemented configurable prover/metalogic engine, and
2. RML as a links/references-grounded formal-system constructor whose own root constructs are explicit and redefinable.

This issue is about closing that gap.

Core problem

Right now many foundational notions are still implicitly imported from the host implementation or from external mathematical traditions:

• numeric literals;
• natural numbers / real-like decimal values;
• truth ranges such as [0, 1];
• arithmetic operations +, -, *, /;
• comparison operations <, <=;
• equality and definitional equality;
• aggregation functions such as avg, min, max, product, probabilistic_sum;
• logical connectives and, or, not, both, neither;
• type-like notions such as Type, Prop, Pi, lambda, apply;
• contexts, substitution, freshness, normalization, conversion;
• inductive/coinductive declarations;
• proof objects and tactic links.

This is acceptable as a bootstrap stage. But if RML wants to be a true meta-logic / universal formal-system constructor, then these constructs must eventually be either:

1. explicitly defined in terms of links/references;
2. explicitly declared as trusted external primitives;
3. or parameterized so that a user can replace/redefine them with another foundation.

Otherwise RML remains configurable at the object-logic level, but not fully grounded at the meta-logic level.

Why this matters for the prover

A prover cannot be foundationless.

Even if RML accepts arbitrary user axioms, the act of accepting and checking them already presupposes a metatheory:

• what counts as a well-formed expression;
• what counts as a rule;
• what counts as a proof object;
• what counts as applying a rule correctly;
• what counts as equality between expressions;
• what counts as substitution;
• what counts as a bound variable;
• what counts as a type;
• what counts as a value;
• what counts as a successful proof replay.

If these notions are implemented directly in JS/Rust and are not representable/redefinable in .lino, then they form the actual trusted foundation of the system.

That is not necessarily bad, but it should be explicit. The prover needs a precise boundary between:

• host-trusted implementation primitives;
• RML-level encoded rules;
• pure links/references definitions;
• object-logic axioms supplied by the user.

Without this distinction, it is easy to say “RML can host any axiom system”, while still silently relying on an unformalized mixture of type theory, set-theoretic collections, real/decimal arithmetic, many-valued algebra, and host-language equality.

Suggested implementation direction

I suggest treating this issue as a structured refactoring/extension of the prover around a new concept:

Root construct registry

Every root construct currently used by the evaluator, type checker, proof replay checker, tactic engine, or metatheorem checker should have a machine-readable declaration of its status.

For example:

(root-construct Type
  (status host-primitive)
  (kind universe-form)
  (implemented-by typed-kernel)
  (planned-as links-definition))

(root-construct Pi
  (status host-primitive)
  (kind binder)
  (depends-on Type substitution freshness context)
  (planned-as links-definition))

(root-construct and
  (status configurable-operator)
  (default-aggregator avg)
  (depends-on truth-value aggregator clamp quantize))

(root-construct natural-number
  (status external-or-undefined)
  (used-by valence universe-level arithmetic indexing)
  (needs-definition yes))

The exact syntax can be different, but the prover should internally distinguish these categories.

Required work items

1. Inventory all root constructs

Create an explicit list of all constructs that are currently treated as primitive or semi-primitive by the implementation.

At minimum:

Syntax / LiNo layer

• reference;
• link;
• list node;
• leaf node;
• AST node;
• parser output;
• canonical printing;
• structural equality of ASTs.

Evaluation layer

• numeric literal;
• symbol;
• definition form;
• probability assignment;
• query;
• range;
• valence;
• truth constant;
• operator table;
• aggregator table;
• arithmetic context;
• logical context;
• clamping;
• quantization.

Logic layer

• true;
• false;
• unknown;
• undefined;
• not;
• and;
• or;
• both;
• neither;
• =;
• !=.

Numeric layer

• natural number;
• decimal number;
• real-like interval;
• finite valence;
• midpoint;
• ordering;
• addition;
• subtraction;
• multiplication;
• division;
• min/max;
• product;
• average;
• probabilistic sum.

Type/kernel layer

• Type;
• Prop;
• universe level;
• Pi;
• forall;
• lambda;
• apply;
• subst;
• fresh;
• context;
• type fact;
• type membership;
• type query;
• definitional equality;
• beta reduction;
• alpha-renaming;
• normalization;
• WHNF/NF;
• convertibility.

Inductive/coinductive layer

• inductive declaration;
• constructor;
• eliminator;
• motive;
• recursor;
• positivity;
• coinductive declaration;
• corecursor;
• guardedness/productivity.

Proof/prover layer

• proof object;
• proof replay;
• rule name;
• derivation tree;
• tactic;
• rewrite;
• simplification;
• induction tactic;
• exact;
• external SMT/ATP trusted node.

Metatheory layer

• mode declaration;
• input/output positions;
• totality;
• coverage;
• termination;
• structural decrease;
• subterm;
• recursive call;
• metatheorem report.

Each entry should say whether it is:

• host-primitive;
• host-derived;
• encoded-as-links;
• links-defined;
• user-configurable;
• external-trusted;
• planned.

2. Separate object-level axioms from meta-level foundations

RML can host arbitrary object theories, but the hosting mechanism itself must have a foundation.

For example, a user may define a custom logic, but the prover still needs its own notion of:

• syntax;
• rule application;
• derivation;
• substitution;
• equality;
• proof replay.

These should not be confused with axioms of the object theory.

The implementation should therefore separate:

Foundation / metatheory:
  what makes RML itself work

Object theory:
  axioms and rules provided by the user

Runtime configuration:
  selected truth range, valence, aggregators, operator meanings

External trust:
  host arithmetic, SMT, ATP, parser, etc.

This separation should be visible both in documentation and in internal data structures.

3. Define a minimal proof-object substrate

For this issue, the prover needs a small explicit representation of proof objects as links.

Possible direction:

(proof-object P)
(judgement J)
(rule R)
(premise P J)
(conclusion P J)
(applies P R)

For example:

(rule reflexivity
  (conclusion (= x x)))

(rule symmetry
  (premise (= x y))
  (conclusion (= y x)))

(rule transitivity
  (premise (= x y))
  (premise (= y z))
  (conclusion (= x z)))

The important part is not this exact syntax, but that the prover should eventually be able to distinguish:

• a proof object as data;
• a proof rule as data;
• a proof replay step;
• a trusted host decision;
• an object-level axiom;
• a derived theorem.

Currently proof replay validates rule names and shapes. For #97, this should evolve into explicit links-level rule declarations that can be inspected and eventually checked by RML itself.

4. Add explicit foundation descriptors for numeric domains

The numeric layer is especially important.

RML currently uses numeric truth values, arithmetic, ranges, valence, clamping, quantization, and aggregators. This silently assumes a numeric domain.

But which domain is it?

• IEEE-754 floats?
• rounded decimals?
• rationals?
• computable reals?
• abstract ordered semiring?
• finite lattice?
• user-provided algebra?
• host-trusted numeric oracle?

For a many-valued logic, this is not an implementation detail. It is part of the semantics.

I suggest adding an explicit numeric-domain descriptor:

(numeric-domain decimal-12
  (status host-primitive)
  (supports + - * / < <=)
  (rounding decimal-precision-12)
  (ordered yes))

(truth-domain default-truth
  (carrier decimal-12)
  (range 0 1)
  (valence continuous)
  (clamp enabled)
  (quantize disabled))

Then alternative domains could be introduced later:

(numeric-domain finite-boolean
  (carrier (finite-set false true))
  (order false < true))

(numeric-domain finite-kleene
  (carrier (finite-set false unknown true))
  (order false < unknown < true))

(numeric-domain rational-interval
  (carrier rational)
  (range 0 1))

This would make explicit whether the logic is using real-like arithmetic, finite lattices, or something else.

5. Make aggregators first-class definitions

Currently aggregators such as avg, min, max, product, and probabilistic_sum behave like built-in semantic choices.

For #97, they should become first-class declarations:

(aggregator min
  (domain truth-value-list)
  (codomain truth-value)
  (definition ...))

(aggregator product
  (domain truth-value-list)
  (codomain truth-value)
  (requires multiplication)
  (requires numeric-domain))

(aggregator probabilistic_sum
  (domain truth-value-list)
  (codomain truth-value)
  (definition (1 - product (map (lambda x (1 - x)) values))))

If an aggregator is still implemented in host code, mark it:

(aggregator avg
  (status host-primitive)
  (trusted yes))

This allows the system to move gradually from host-defined aggregators to links-defined aggregators.

6. Clarify equality layers

RML currently has several different equality-like notions:

• structural equality of links/ASTs;
• numeric equality;
• explicit assigned equality;
• definitional equality / convertibility;
• object-level equality inside hosted theories.

These should be separated.

Suggested explicit layers:

structural-equality:
  same normalized link/AST shape

assigned-equality:
  source-level assertion installed into environment

numeric-equality:
  equality in the selected numeric domain

definitional-equality:
  equality after reduction/normalization/conversion

object-equality:
  equality symbol of a hosted object theory

These should not all collapse into one = without metadata. The prover should know which equality rule is being used in each derivation.

Possible proof rule names:

(rule structural-eq-intro ...)
(rule assigned-eq-use ...)
(rule numeric-eq-decide ...)
(rule beta-convert ...)
(rule definitional-eq ...)
(rule object-eq-axiom ...)

This is crucial for proof replay and soundness explanations.

7. Make Type, Prop, Pi, and lambda status explicit

The current typed kernel imports a lot of type-theoretic structure.

That is fine, but for #97 the system should be explicit:

• Are Type and Prop primitive?
• Is Pi primitive?
• Is lambda primitive?
• Is substitution primitive?
• Is beta-reduction primitive?
• Is alpha-renaming primitive?
• Is universe stratification primitive?
• Is Type : Type allowed as object-level assumption, or part of the meta-kernel?

A possible intermediate solution:

(type-kernel cic-like-fragment
  (status host-implemented)
  (constructs Type Prop Pi lambda apply subst fresh)
  (conversion beta)
  (universes stratified)
  (allows Type:Type yes-in-dynamic-mode)
  (soundness relative-to runtime-configuration))

Then later:

(type-kernel links-defined-fragment
  (status links-defined)
  (constructs ...)
  (rules ...))

This lets the current prover remain usable while making the foundational status honest.

8. Distinguish “configurable operator” from “defined construct”

Runtime redefinition is not the same thing as foundational definition.

For example:

(and: min)

selects an aggregator, but it does not define what min, truth values, ordering, or finite/continuous domains are.

Similarly:

(range: 0 1)

selects a range, but assumes numbers, order, interval endpoints, midpoint, and clamping.

For #97, RML should distinguish:

configuration:
  choosing among existing host-provided semantics

definition:
  expressing semantics inside links/references

override:
  replacing an existing root construct with another definition

reduction:
  explaining one construct in terms of more primitive constructs

This distinction is essential.

9. Add a “foundation mode” to the prover

The prover could expose different checking modes.

Current/default mode

Works as today:

Host evaluator + host kernel + configurable runtime semantics.

Explicit-trust mode

Same behavior, but every proof/report records which trusted primitives were used:

used host primitive: decimal arithmetic
used host primitive: structural equality
used host primitive: beta reduction
used aggregator: product
used external trusted solver: z3

Pure-links mode

Rejects any proof step that depends on a host primitive not defined in links.

Example:

E0XX: numeric equality used, but numeric domain is not links-defined
E0XY: aggregator product used, but multiplication is host-primitive
E0XZ: beta reduction used, but substitution is not links-defined

This would make #97 testable.

10. Add acceptance tests for #97

Possible tests:

A. Root construct inventory test

A test that fails if a built-in evaluator/kernel construct has no root descriptor.

Every built-in operator/type/kernel/proof/metatheorem primitive must appear in root-construct registry.

B. Trusted-base report test

Given a .lino program, the prover should be able to print a trust report:

Trusted primitives used:
- LiNo parser
- canonical printer
- decimal-12 arithmetic
- structural equality
- beta reduction
- aggregator product
- proof replay classifier

C. Pure-links rejection test

In pure-links mode, using arithmetic without a links-defined numeric domain should fail.

(? ((0.1 + 0.2) = 0.3))

Expected:

Rejected in pure-links mode:
numeric-domain decimal-12 is host-primitive

D. User-defined finite truth domain test

Define a Boolean or Kleene truth domain as links, then define and, or, not over it without relying on host numeric range.

E. Equality-layer test

Demonstrate that structural equality, numeric equality, assigned equality, and definitional equality are different proof rules.

F. Proof-object rule declaration test

Define a small proof system in links:

(rule refl ...)
(rule symm ...)
(rule trans ...)

Then replay a proof object against these rule declarations.

G. Override root construct test

Override a root construct in a controlled scope and verify that the prover records the new foundation.

Example:

(override equality with structural-equality-only)

or equivalent syntax.

11. Documentation changes

This issue probably needs a new document, for example:

docs/FOUNDATIONS.md

Suggested sections:

1. Current trusted base.
2. Root constructs.
3. Host primitives vs links-defined constructs.
4. Numeric domains.
5. Equality layers.
6. Type-theoretic imports.
7. Proof object substrate.
8. How to move a construct from host-primitive to links-defined.
9. Pure-links mode.
10. Relationship to Software Foundations / propositions-as-types.

The current SOUNDNESS.md already honestly states that RML does not yet claim a fully mechanised metatheory. This issue can become the implementation roadmap for turning that statement into a finer-grained, inspectable foundation.

Proposed milestone breakdown

Phase 1 — Inventory and reporting

• Add root construct registry.
• Mark all current primitives.
• Add trust report output.
• Update docs.

No semantics need to change yet.

Phase 2 — Equality and numeric-domain separation

• Split equality into explicit layers.
• Add numeric-domain descriptors.
• Mark arithmetic and aggregators as host-defined or links-defined.
• Add tests for equality provenance.

Phase 3 — Proof-object substrate

• Represent proof rules as links.
• Represent proof objects as links.
• Extend proof replay so it can consume rule declarations.
• Keep old built-in replay rules as host-trusted rules.

Phase 4 — Links-defined finite logics

• Implement Boolean/Kleene/Belnap truth domains as pure links definitions.
• Define and, or, not over those domains without relying on host decimals.
• Use this as the first nontrivial demonstration of Use similar idea, but everything should be built from links and references #97.

Phase 5 — Links-defined type/proof kernel fragment

• Define a minimal propositions-as-types fragment in links.
• Introduce Prop, implication, conjunction, disjunction, equality, evidence/proof objects.
• Keep it small, similar in spirit to Software Foundations.
• Show how existing typed-kernel forms map into this fragment or remain host primitives.

Phase 6 — Pure-links checking mode

• Add a mode where any host-primitive dependency must be rejected unless explicitly allowed.
• This becomes the practical test that RML can operate with a links-defined foundation.

Summary

This issue should not be interpreted as “add another non-standard logic feature”.

It is about making the prover honest and extensible at the foundational level.

The key implementation goal is:

Every construct used by the prover must either be defined in links/references, declared as an external trusted primitive, or be replaceable by a user-provided links-level definition.

Once this is done, RML becomes much closer to the intended architecture: not merely a configurable prover, but a formal-system constructor whose own foundations can be inspected, redefined, and eventually expressed inside RML itself.

[netkeep80]

Additional clarification for issue #97

I think the existing implementation direction is mostly right. The main missing piece is an explicit acceptance contract for what it means for a root construct to be "built from links/references" versus merely "encoded as descriptive LiNo data".

Right now RML already has a self-bootstrap layer that describes grammar, evaluator rules, type rules, operators, and metatheorem checks as links. That is an important step, but it is not yet the same thing as making those constructs foundationally replaceable or checkable by RML itself.

So I suggest sharpening this issue around the following distinction.

1. Four different statuses must not be conflated

A construct can be:

1. host-primitive — implemented directly in JS/Rust and trusted;
2. links-encoded — described as links, but still interpreted by host code;
3. links-defined — its meaning is given by link-level rules that the prover can consume;
4. user-overridden — replaced in a controlled foundation scope by a user-provided definition.

These are not equivalent.

For example, a rule in lib/self/evaluator.lino may describe beta-reduction, but unless the proof checker/evaluator can actually consume that rule as authority, beta-reduction is still host-primitive or host-derived. That is fine, but the status must be machine-visible.

A possible descriptor shape:

(root-construct beta-reduction
  (surface apply)
  (kind reduction-rule)
  (status host-primitive)
  (encoded-as self.evaluator.beta-apply)
  (depends-on substitution freshness alpha-renaming structural-equality)
  (override allowed-in-foundation-scope)
  (pure-links-ready no))

2. Add a construct dependency graph

The root construct registry should not be a flat list only. It should also form a dependency graph.

Example:

(root-construct Pi
  (kind binder)
  (depends-on Type context substitution freshness alpha-renaming))

(root-construct definitional-equality
  (kind equality-layer)
  (depends-on normalization beta-reduction structural-equality))

(root-construct and
  (kind truth-operator)
  (depends-on truth-domain aggregator clamp quantize))

Then the prover can answer:

Why was this query accepted?
Which root constructs were used?
Which of them are host-trusted?
Which of them are links-defined?
Which user override changed the result?

This would make #97 testable rather than only philosophical.

3. Overrides must be scoped, not global mutation

The issue mentions override / redefine in other terms. I think this must be scoped by a named foundation, not performed as unrestricted global mutation.

Suggested direction:

(foundation default-rml
  (uses decimal-12-arithmetic)
  (uses rml-equality)
  (uses rml-typed-kernel))

(foundation finite-boolean-links
  (defines truth-domain boolean-truth-domain)
  (defines true boolean-true)
  (defines false boolean-false)
  (defines not boolean-not)
  (defines and boolean-and)
  (defines or boolean-or))

(with-foundation finite-boolean-links
  (? (and true false)))

This avoids ambiguity when one file imports another file that changes foundational semantics. Proof objects and query results should record the active foundation scope.

4. Separate object theory axioms from foundation rules

A user object theory may contain arbitrary axioms. But the mechanism that checks object-theory proofs still has its own foundation.

So the system should explicitly distinguish:

foundation rule:
  used by RML to parse/check/evaluate/replay proofs

object-theory axiom:
  user-provided assumption inside a hosted theory

runtime configuration:
  selected truth range, valence, aggregators, operator table

external trusted oracle:
  SMT/ATP/parser/host arithmetic/etc.

This matters because otherwise a user can appear to "override equality" while actually only overriding object-level equality, leaving structural equality, numeric equality, and definitional equality untouched in the host kernel.

5. Equality needs an explicit layered contract

The symbol = currently covers several different relations. For #97 these should be separated in proof provenance:

structural-equality
assigned-equality
numeric-equality
definitional-equality / convertibility
object-level equality

A proof should not merely say:

(by equality ...)

It should say which equality layer was used:

(by structural-equality ...)
(by numeric-equality decimal-12 ...)
(by assigned-equality source-form-id ...)
(by beta-conversion ...)
(by object-equality object-theory-id ...)

This is probably one of the most important soundness requirements for the issue.

6. Define a minimal first milestone

The smallest useful PR for this issue does not need to implement pure self-hosting. It can be only inventory + reporting.

Acceptance criteria for the first milestone:

• every evaluator/kernel/proof/metatheory primitive has a root-construct descriptor;
• every descriptor has a status: host-primitive, host-derived, links-encoded, links-defined, user-configurable, external-trusted, or planned;
• the CLI can print a trust/foundation report for a .lino file;
• tests fail when a new built-in construct is added without a descriptor;
• equality proof rules report the specific equality layer used.

Example output:

Foundation report:
  active foundation: default-rml

Host trusted:
  - LiNo parser
  - canonical printing
  - structural equality
  - decimal-12 arithmetic
  - beta reduction
  - substitution
  - proof replay classifier

Links encoded:
  - evaluator rules
  - operator declarations
  - type-layer rules

Runtime configured:
  - truth range: [0, 1]
  - valence: continuous
  - and: avg
  - or: max

Source axioms:
  - ((p = true) has probability 0.7)

This would give immediate value without breaking current behavior.

7. Suggested strict modes

After the registry exists, add modes gradually:

default mode:
  current behavior; host primitives allowed silently

explicit-trust mode:
  current behavior, but all host primitive dependencies are reported

foundation-strict mode:
  host primitives are allowed only if the active foundation declares them

pure-links mode:
  reject any step depending on a construct that is not links-defined

Pure-links mode should probably start very small. A good first demonstration would be a finite Boolean or Kleene truth domain defined entirely through links, with and, or, and not defined over that finite carrier without relying on decimal truth ranges.

8. Clarify the relation to Software Foundations

The useful idea from Software Foundations is not that there is no kernel. Coq still has a trusted kernel. The useful idea is that many logical forms can be reduced to a smaller, explicit substrate and then manipulated as ordinary formal objects.

For RML the analogous target should be:

as many RML constructs as possible should move from host-primitive to links-defined, while the remaining host-trusted base is explicit, minimal, and reported.

So the goal is not "no primitives". The goal is:

no implicit primitives.

Proposed issue-level invariant

A strong invariant for #97 could be:

Every construct used by parsing, evaluation, type checking, proof replay, tactics, metatheorem checking, or self-bootstrap must be either defined in links, encoded as links with a declared host interpreter, declared as an external trusted primitive, or explicitly marked as planned/undefined. No root construct may be used without a descriptor and a trust status.

This would make RML much closer to a real formal-system constructor: not only configurable at the object-logic level, but transparent and eventually redefinable at the meta-logic level.

[konard]

We need to make sure all described is alternative way to do logic. We just will be able to replace the foundations of logic apparatus, but it should behave essentially the same way. And traditional foundations should work by default, as well as our everything is a link (including reference) approach, which can we recorded in links notation due to its embedded referential structure.

So that should add to customizability, but backward compatibility should be fully preserved.

Make sure everything covered with unit, integration and e2e tests, and executed in CI/CD.

Use all the best practices from CI/CD templates (check full file tree to compare for all GitHub workflow and CI/CD scripts file), if the same issue is found in template report issue also in templates:

• https://github.com/link-foundation/js-ai-driven-development-pipeline-template
• https://github.com/link-foundation/rust-ai-driven-development-pipeline-template
• https://github.com/link-foundation/python-ai-driven-development-pipeline-template
• https://github.com/link-foundation/csharp-ai-driven-development-pipeline-template

We should compare all files, so we don't have more CI/CD errors in the future and reuse all the best practices from these templates.

We need to collect data related about the issue to this repository, make sure we compile that data to ./docs/case-studies/issue-{id} folder, and use it to do deep case study analysis (also make sure to search online for additional facts and data), list of each and all requirements from the issue, and propose possible solutions and solution plans for each requirement (we should also check known existing components/libraries, that solve similar problem or can help in solutions).

Please plan and execute everything in a single pull request, you have unlimited time and context, as context auto-compacts and you can continue indefinitely, until it is each and every requirement fully addressed, and everything is totally done.

[netkeep80]

Reopening note: PR #174 completed Phase 1, but the literal #97 goal is not complete yet

I think PR #174 should stay merged. It is a useful and well-scoped first step: it adds the root-construct registry, foundation declarations, scoped (with-foundation ...), (foundation-report), default backward compatibility, tests in both engines, documentation, and the case-study material.

However, after reviewing the merged implementation, I think this issue should be reopened because the original requirement is stronger than what PR #174 delivers.

The original issue says:

everything should be built from links and references (and fully defined) ... add a way to override/redefine in other terms these root constructs.

PR #174 implements the inventory / reporting / scoped host-operator rebinding layer. It does not yet implement the deeper “pure links / references / fully defined foundations” layer.

So the right status is:

PR #174 = Phase 1 complete
#97 = not fully complete yet

What PR #174 already completed

The merged PR appears to have completed these parts:

• default-rml is pre-registered and existing .lino programs continue to work without migration.
• root-construct descriptors exist and are seeded in both JS and Rust.
• foundation descriptors exist and can be registered from .lino.
• (with-foundation <name> ...) scopes operator rebinding and restores previous semantics on exit.
• (foundation-report) exposes a structured trust/foundation snapshot.
• lib/self/foundations.lino records the registry as data.
• docs/FOUNDATIONS.md documents the new surface.
• E060, E061, E062 diagnostics were added.
• JS and Rust tests cover basic registry, scoped override, nested scopes, unknown foundation errors, and report shape.
• CI was green on the final PR head.

This is valuable infrastructure and should be treated as the foundation for the next phases, not as something to undo.

Why the issue is still not complete

The current implementation mostly describes root constructs and allows a small class of host-level operator rebinding. It does not yet make the root constructs themselves links-defined.

In particular:

Current state:
  links-encoded / host-described / host-executed

Target state for #97:
  links-defined / proof-visible / optionally pure-links-checked

The important gap is that the registry currently answers:

“What does the host trust?”

but the original issue also asks:

“Can the constructs needed for logic and types be built from links/references and fully defined there?”

That second part is still open.

Remaining work

1. Equality-layer provenance

The registry now names several equality layers, but proof/evaluation output does not yet expose which layer was used.

We need explicit provenance for at least:

• structural-equality
• assigned-equality
• numeric-equality
• definitional-equality
• later: object-level equality inside a selected foundation

Target proof/trace shape:

(by structural-equality ...)
(by assigned-equality ...)
(by numeric-equality decimal-12 ...)
(by definitional-equality beta-normalization ...)

Acceptance criteria:

• A query using syntactic identity reports/proves structural-equality.
• A query using an explicit has probability equality assignment reports/proves assigned-equality.
• A numeric equality such as ((0.1 + 0.2) = 0.3) reports/proves numeric-equality.
• A beta-reduction equality reports/proves definitional-equality.
• JS and Rust output/proofs agree.

2. Numeric-domain and truth-domain enforcement

numeric-domain and truth-domain are currently mostly metadata.

For example, a boolean-classical foundation can say it uses a Boolean domain, but values such as 0.6 and 0.4 can still be used normally unless separate valence/range configuration is also applied.

We need a real domain contract.

Possible design:

(truth-domain two-valued
  (carrier false true)
  (value false 0)
  (value true 1)
  (order false true))

(numeric-domain boolean-zero-one
  (carrier 0 1)
  (closed-under min max not))

Acceptance criteria:

• A foundation can declare its carrier.
• The evaluator can optionally enforce that query values belong to the active carrier.
• Violations produce structured diagnostics, not silent coercions.
• Boolean and Kleene examples actually exercise the declared domain, not only host min/max.

3. Links-defined finite truth tables

boolean-classical and kleene-three-valued are currently implemented by binding host aggregators like min and max.

That is fine for Phase 1, but for #97 we need at least one finite logic whose connectives are defined as links.

Example direction:

(truth-value boolean false)
(truth-value boolean true)

(table boolean-and
  (case false false false)
  (case false true  false)
  (case true  false false)
  (case true  true  true))

(table boolean-or
  (case false false false)
  (case false true  true)
  (case true  false true)
  (case true  true  true))

Then a foundation should be able to bind:

(foundation boolean-links
  (truth-domain boolean)
  (defines and boolean-and)
  (defines or boolean-or)
  (defines not boolean-not))

Acceptance criteria:

• At least one Boolean foundation is genuinely links-defined.
• Its truth tables are readable as ordinary .lino data.
• The host can execute/replay these table definitions.
• The report marks these connectives as links-defined, not host-primitive.

4. Proof-object substrate as links

The issue references the Software Foundations style, where logical connectives can be introduced by definitions and rules rather than by opaque host magic.

RML needs a minimal proof-object substrate expressed as links.

Possible core vocabulary:

(judgement ...)
(rule ...)
(premise ...)
(conclusion ...)
(proof-object ...)
(applies ...)

Example target:

(rule and-intro
  (premise p)
  (premise q)
  (conclusion (and p q)))

(proof-object proof-and-p-q
  (applies and-intro proof-p proof-q))

Acceptance criteria:

• Proof rules can be represented as links.
• Proof objects can reference rule links.
• Replay can distinguish host-trusted rules from links-defined rules.
• (foundation-report) includes proof-rule dependencies.
• At least one simple proposition proof is replayed from links-defined proof rules.

5. Links-defined logical connectives

After the proof-object substrate exists, define the first small logical fragment in .lino.

Minimum fragment:

• Prop
• implication
• conjunction
• disjunction
• false/absurdity
• negation as P -> False
• equality introduction / reflexivity, or a minimal object-level equality

Acceptance criteria:

• The connectives are not merely names for host operators.
• The introduction/elimination rules are visible as links.
• A small theorem can be proved through the links-defined rules.
• The proof replay report shows which rules were host-primitive and which were links-defined.

6. Links-defined type/proof-kernel fragment

The original issue explicitly mentions “reason about types and so on”. The current typed kernel remains host-primitive.

We should not try to replace the entire kernel at once. But we should define a small fragment:

• one universe or object-level Type
• object-level Pi
• object-level lambda
• object-level apply
• beta rule as an explicit rule
• substitution/freshness dependency explicitly reported

Acceptance criteria:

• The host typed kernel remains the default.
• A small object-level type fragment can be represented in links.
• The report clearly says which parts are host-primitive and which are links-defined.
• There is at least one example where the object-level fragment checks/replays through the links-defined layer.

7. Pure-links strict mode

The registry is useful, but without enforcement it is only a report.

We need an opt-in strict mode that can reject proofs or evaluations depending on host-primitive constructs.

Possible modes:

--foundation-report
--foundation-strict
--pure-links-only
--allow-host-primitive=<name>

Possible .lino forms:

(strict-foundation pure-links)
(allow-host-primitive parser)
(allow-host-primitive canonical-printer)

Acceptance criteria:

• In strict mode, a proof depending on an unallowed host-primitive is rejected.
• The diagnostic explains the exact offending construct.
• The user can allow a small trusted boundary explicitly.
• The same strict-mode behavior exists in JS and Rust.

8. Dependency graph traversal

The registry records depends-on, but the report should also be able to show the transitive closure of dependencies for a query/proof.

Target:

Query depends on:
  and
    -> boolean-and
      -> boolean truth-domain
      -> truth-table lookup
  equality
    -> structural-equality
    -> canonical-printer

Acceptance criteria:

• foundation-report can show all constructs.
• A per-query or per-proof report can show only constructs actually used.
• Transitive dependencies are sorted deterministically.
• JS and Rust reports are byte-identical where applicable.

9. MTC/anum foundation profile

The anum_docs / MTC direction is a natural testbed for this issue because it is explicitly based on “everything is a link”.

But it should be integrated carefully as an experimental foundation profile, not as a replacement for default-rml.

Suggested form:

(foundation mtc-anum
  (description experimental-metatheory-of-links-foundation)
  (truth-domain mtc-abits)
  (root ∞)
  (abit [ start-of-meaning)
  (abit ] end-of-meaning)
  (abit 1 unit-of-meaning)
  (abit 0 zero-of-meaning))

Acceptance criteria:

• MTC/anum is opt-in.
• It does not change default RML semantics.
• It can serialize/decode a small link expression.
• The report marks it as experimental.
• The boundary between theory domain and serialization domain is explicit.

10. Documentation contract cleanup

There is a small but important contract issue: some documentation currently sounds stricter than the implementation.

For example, foundation defines entries that are not recognized as known aggregators may effectively be data-only rather than producing an error. Unknown descriptor clauses are also accepted for forward compatibility.

That may be fine, but the docs should say exactly which behavior is intended.

Acceptance criteria:

• docs/FOUNDATIONS.md clearly distinguishes:
  • data-only declarations,
  • behavior-changing declarations,
  • strict-mode declarations,
  • future/planned declarations.
• Unknown statuses/clauses/aggregators have documented behavior.
• Tests cover that documented behavior.

Suggested follow-up PR split

To keep this manageable, I suggest not doing all remaining work in one PR.

PR A — Documentation and contract alignment

• Clarify that Root-construct registry & foundation scope (#97) #174 is Phase 1.
• Clarify which foundation declarations are data-only.
• Clarify which declarations currently affect runtime behavior.
• Add tests for unknown/non-aggregator defines behavior.

PR B — Equality provenance

• Split equality proof/trace labels.
• Add JS/Rust tests.
• Update proof replay docs.

PR C — Links-defined Boolean foundation

• Add truth-domain carrier.
• Add links-defined truth tables.
• Execute/replay at least and, or, not.
• Mark these as links-defined.

PR D — Proof-object substrate

• Add minimal rule / premise / conclusion / proof-object.
• Replay one simple proof from links-defined rules.

PR E — Pure-links strict mode

• Add strict checking.
• Reject unallowed host-primitive dependencies.
• Add CLI and .lino surface.

PR F — Experimental MTC/anum foundation

• Add optional MTC/anum profile.
• Keep default-rml untouched.
• Add serialization example and report output.

Proposed updated completion condition for #97

I suggest this issue should remain open until at least the following are true:

• The current Phase 1 surface is documented as inventory/report/scoped override, not as full pure-links completion.
• Equality provenance is visible in proof/trace output.
• At least one finite logic is genuinely links-defined, not only host-aggregator-defined.
• Numeric/truth-domain declarations have an enforced mode.
• Minimal proof rules/proof objects are representable as links.
• A small logical fragment can be proved/replayed through links-defined rules.
• A pure-links strict mode can reject unallowed host primitives.
• The dependency graph can be reported per proof/query.
• Optional MTC/anum foundation profile is either implemented or explicitly moved to a separate issue.

Bottom line

PR #174 is a good Phase 1 and should be kept.

But the issue should be reopened because the original “everything built from links/references and fully defined” goal is not complete yet. The remaining work is not a bug in PR #174; it is the next set of phases that PR #174 made possible.