Negation exchanges the two quantifiers

Identifier: F:quantifier-negation-duality
Proof route: smt-term-level
External status: proved
Axiom footprint: axeyum-solver.bool-simplification-normalizer, axeyum-rewrite.alpha-and-duality-equivalence, classical-two-valued-bool-semantics, smtlib-first-order-quantifier-semantics

Recorded description

Over any domain and any predicate P: not (for all x, P(x)) is equivalent to (there exists x with not P(x)), and not (there exists x with P(x)) is equivalent to (for all x, not P(x)).

Formal statement

(assert (and (= (not (forall ((x U)) (P x))) (exists ((x U)) (not (P x)))) (= (not (exists ((x U)) (P x))) (forall ((x U)) (not (P x))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

quantifier-negation-duality-bool-simplification

Kind: unsat-certificate
Status: checked

Supports: Over any domain and any predicate P: not (for all x, P(x)) is equivalent to (there exists x with not P(x)), and not (there exists x with P(x)) is equivalent to (for all x, not P(x)).

Checker command

test "$(cargo run --release -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/neg-quantifier-negation-duality.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-bool-simplification certified=1 recheck=na arena=ok`. This fact was `open` earlier the same day (`kind=unknown ... ms=18`); the lane `quant-duality` closed it. WHAT THE CERTIFICATE IS, precisely, because the route name could mislead: it is NOT exhaustive evaluation -- the carrier sort U is uninterpreted and cannot be enumerated. It is `Evidence::UnsatBoolSimplification`, a refutation by the small checked propositional normalizer in `axeyum-solver/src/bool_simplify.rs`, which treats every quantified subformula as an OPAQUE ATOM and instantiates, skolemizes and expands nothing. The one thing it now knows about quantifiers is when two of them are the same formula written differently -- `axeyum_rewrite::alpha_equivalent`, which decides equality up to bound-variable renaming (the SMT-LIB front end mints a fresh arena symbol per binder, so the four `x`s in this file are four distinct symbols) and up to the negation duality itself, by carrying a negation parity through the walk. Under those two facts both conjuncts of the asserted `and` normalize to `true`, the outer `not` to `false`, and the assertion is refuted. It trusts neither the bit-blaster, the CNF encoder, nor the SAT solver: nothing was blasted. `arena=ok` means `Evidence::check` re-ran that normalizer against a FRESH PARSE of the file, independent of anything the producing solve held in memory. Independently cross-checked: `z3 -smt2` (4.13.3) on the same file also reports `unsat`.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum lane `quant-duality`, 2026-08-14: `quant.negation_duality.v1` and `eq.alpha_equivalent.v1` in the canonicalizer, plus the matching alpha/duality predicate in the `bool_simplify` certificate checker",
  "source": "authored from the S:logic-and-proof strand of the math-education concept graph; statement written here, not copied",
  "prior_art": [
    {
      "oracle": "z3 -smt2 artifacts/facts/smt2/neg-quantifier-negation-duality.smt2",
      "result": "unsat",
      "date": "2026-08-14",
      "establishes": "the proposition is valid; recorded when only OUR route failed to see it, and kept as the independent cross-check now that it does"
    }
  ]
}