Affirming the consequent is a valid inference

Identifier: F:affirming-the-consequent
Proof route: search-certificate
External status: refuted
Axiom footprint: Empty

Recorded description

For all propositions p and q: if (p implies q) holds and q holds, then p holds. THIS PROPOSITION IS FALSE; the fact is recorded with status `refuted` and carries the countermodel.

Formal statement

(assert (=> (and (=> p q) q) p))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

affirming-the-consequent-countermodel

Kind: witness-replay
Status: checked

Supports: p := false, q := true satisfies the negation of the proposition, so the proposition is not a tautology

Checker command

test "$(cargo run -q -p axeyum-bench --example smtcomp_cli -- --evidence artifacts/facts/smt2/affirming-the-consequent.smt2 2>/dev/null | tail -1)" = sat

Evidence notes

Ran 2026-08-14: the file asserts the NEGATION of formal.statement and the solver reported `sat` with `kind=sat-model certified=1 arena=ok`. `arena=ok` is Evidence::check replaying the model against a fresh parse of the file -- the model is evaluated against the original assertions, not against the lowered form. The witness is p := false, q := true: then (p implies q) is true and q is true while p is false. Independently cross-checked: `z3 -smt2` on the same file also reports `sat`.

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": "Aristotle, Sophistical Refutations; catalogued as a formal fallacy ever since",
      "establishes": "that the inference is invalid, i.e. that the proposition recorded by this fact is false",
      "attribution": "standard textbook attribution; this lane did not consult the primary source, and records the citation as the received one"
    }
  ]
}