NAND defines negation, conjunction and disjunction

Identifier: F:nand-functional-completeness
Proof route: smt-term-level
External status: proved
Axiom footprint: axeyum-ir.bool-evaluator, classical-two-valued-bool-semantics

Recorded description

Writing NAND(a, b) for not (a and b): not p equals NAND(p, p); p and q equals NAND(NAND(p, q), NAND(p, q)); p or q equals NAND(NAND(p, p), NAND(q, q)).

Formal statement

(assert (and (= (not p) (not (and p p))) (= (and p q) (not (and (not (and p q)) (not (and p q))))) (= (or p q) (not (and (not (and p p)) (not (and q q)))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

nand-functional-completeness-term-level

Kind: exhaustive-enumeration
Status: checked

Supports: Writing NAND(a, b) for not (a and b): not p equals NAND(p, p); p and q equals NAND(NAND(p, q), NAND(p, q)); p or q equals NAND(NAND(p, p), NAND(q, q)).

Checker command

test "$(cargo run -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-nand-functional-completeness.smt2 2>/dev/null | tail -1)" = unsat

Evidence notes

Ran 2026-08-14: the file asserts the NEGATION of formal.statement and the solver reported `unsat` with `kind=unsat-term-level certified=1 arena=ok`. `unsat-term-level` is exhaustive evaluation of the 4 Boolean assignments by the axeyum-ir evaluator alone -- it trusts neither the bit-blaster, the CNF encoder, nor the SAT solver. `arena=ok` means Evidence::check re-ran that enumeration against a FRESH PARSE of the file, independent of anything the producing solve held in memory. Independently cross-checked: `z3 -smt2` on the same file also reports `unsat`.

Provenance

{
  "date": "2026-08-14",
  "established_by": "facts-logic lane, axeyum SAT/SMT front door",
  "source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
  "prior_art": [
    {
      "citation": "H. M. Sheffer (1913), 'A Set of Five Independent Postulates for Boolean Algebras', Transactions of the AMS 14",
      "establishes": "the single-connective basis now called the Sheffer stroke; C. S. Peirce had the result in unpublished work of 1880",
      "attribution": "standard textbook attribution; this lane did not consult the primary source, and records the citation as the received one"
    }
  ]
}