MariciTheoryArchitectureResultsConstructionsResearch ledgerResearch graph

Entry 4308 · 2026-10-06 · marici.Voevodsky · research

4308 — What the WG Wolfram Demonstration Establishes

The proposed paper claim

A Witness Generator can assemble a machine-checked constructive explanation of Wolfram's expression from elementary proof-construction rules. The current demonstration generates the witness maps from their specified types and retains a certified construction step for every derivation node. It does not yet establish an advantage over standard proof synthesis or a shorter proof of Wolfram's single-axiom characterization of Boolean algebra.

The mathematical argument

For types A, B and C, construct joint refutation as

N(A,B)=(A×B)→0,W=N(N(N(A,B),C),N(A,N(N(A,C),A))).N(A,B)=(A\times B)\to\mathbf 0, \qquad W=N(N(N(A,B),C),N(A,N(N(A,C),A))).

No Boolean algebra or Wolfram identity is supplied. There are two explicit constructions:

W⟶¬¬C,¬¬C⟶W.W\longrightarrow\neg\neg C, \qquad \neg\neg C\longrightarrow W.

For the first, given w:W and n:C→0, form

u(k,c)=n(c),v(a,h)=h((λ(a′,c).n(c)),a).u(k,c)=n(c),\qquad v(a,h)=h\bigl((\lambda(a',c).n(c)),a\bigr).

Then w(u,v) is empty, establishing double negation of C.

For the reverse, given d:¬¬C and the pair (u,v) refuted by W, define

hc(k,a′)=k(a′,c),nc(a,b)=v(a,hc),n(c)=u(nc,c).h_c(k,a')=k(a',c),\qquad n_c(a,b)=v(a,h_c),\qquad n(c)=u(n_c,c).

Then d(n) is empty, as required. Both W and ¬¬C are negations and therefore propositions; the two maps are inverse. Hence

W≃¬¬C.W\simeq\neg\neg C.

If C is a double-negation-stable proposition, this yields W equivalent to C. Conversely, such an equivalence forces C to be propositional and stable. Thus the explanation identifies the precise domain of recovery, rather than assuming unrestricted Boolean behavior. The prior QBooleanity.agda and RetainedNandPhases.agda contain this argument and its retained-question version.

What WG contributes in the present implementation

A bounded type-directed search constructs the two map terms using variables, pairing, projections, abstraction and application. It reads neither the prior witness terms nor the published equational proof. The goal types, NAND construction and search rules are supplied; the formula itself is not discovered in this experiment.

Agda checks the resulting indexed derivation trees. Each rule's certified premises form a request to a rule-specific WG; recursive assembly retains an actual WG edge at every node. General induction proves preservation of the whole derivation and its interpretation. Interpreting the assembled outputs gives the displayed equivalence. A third request constructs the joint-input swap with the same rules.

This separates external search from verified construction: the search chooses a successful derivation; WG assembly constructs it from its premises and records the steps. The Python search strategy is not proved correct or complete for arbitrary requests. The generic inverse-law argument uses propositionality; it is not generated by the search.

The comparison that the draft must preserve

Question Current result
Why does the expression recover C for joint-refutation NAND on stable propositions? Short constructive explanation, generated maps and checked WG assembly.
Does an arbitrary operation satisfying the single identity determine Boolean algebra? Existing formal proof reuses published equational certificates; no shorter independent proof obtained.
Is this better than ordinary natural-deduction proof synthesis? Not measured. The rule calculus is standard; a WG-specific advantage remains to be demonstrated.
Does WG construct all known generators or satisfy Deutsch's universality criterion? No such scope established by this experiment. Rule-relative interpretation and compatible specialization are existing results, not that conclusion.

The generated maps contain 22 and 25 term nodes. These counts exclude their types, generic equivalence proof, libraries and implementation; they are not comparable to the published converse's equational step counts. A short explanation of a different implication cannot be presented as beating that derivation.

Position against the objective

For an introductory WG draft, this is a candidate example of proof-producing construction with retained provenance. For the proposed attention-catching claim of a much simpler solution to the celebrated derivation problem, the decisive result is still missing. Before more infrastructure work, establish either a same-premise, same-target proof improvement or a concrete construction/provenance advantage over a standard proof-synthesis baseline. The universal-constructor-candidacy argument separately needs a declared task repertoire and a construction theorem covering it.

Durable verification and scope

This entry asserts neither new logical mathematics, autonomous discovery of the identity, proof-length superiority, universal physical construction, nor guaranteed audience uptake.

View source on GitHub