Peano Factorial • 5! = 120 proved via Resolution

Problem

Formalize factorial with successor; refute ¬fact(5, 120)

// Symbols:
//   0                // zero
//   s(x)             // successor
// Predicates:
//   add(x,y,z)       // x + y = z
//   mult(x,y,z)      // x · y = z
//   fact(n,z)        // n! = z
//
// Axioms (Horn-friendly):
// Addition:
//   A1: add(X, 0, X).
//   A2: add(X, Y, Z) -> add(X, s(Y), s(Z)).
//
// Multiplication:
//   M1: mult(X, 0, 0).
//   M2: mult(X, Y, Z) ∧ add(Z, X, Z2) -> mult(X, s(Y), Z2).
//
// Factorial:
//   F1: fact(0, s(0)).                              // 0! = 1
//   F2: fact(N, F) ∧ mult(s(N), F, Z) -> fact(s(N), Z).
//
// Goal (ground): fact(s⁵(0), s¹²⁰(0)).  (where sⁿ(0) abbreviates n successors)

We’ll show the axioms plus the negation of the goal derive ⟂ under Resolution.

Answer

Entailed. The factorial, multiplication, and addition axioms, together with ¬fact(5,120), resolve down to the base cases and yield the empty clause.

Reason Why

Resolution justification (clausal refutation, sketched)

  1. Clausify the Horn implications (move antecedents to the left as negated disjuncts):
    CA1: add(X, 0, X)
    CA2: ¬add(X, Y, Z) ∨ add(X, s(Y), s(Z))
    CM1: mult(X, 0, 0)
    CM2: ¬mult(X, Y, Z) ∨ ¬add(Z, X, Z2) ∨ mult(X, s(Y), Z2)
    CF1: fact(0, s(0))
    CF2: ¬fact(N, F) ∨ ¬mult(s(N), F, Z) ∨ fact(s(N), Z)
  2. Negate the goal and add it: ¬fact(s⁵(0), s¹²⁰(0)).
  3. Repeatedly resolve with CF2 to unfold factorial:
    ¬fact(s⁴(0), s²⁴(0)), then ¬fact(s³(0), s⁶(0)), then ¬fact(s²(0), s²(0)), then ¬fact(s(0), s(0)), finally ¬fact(0, s(0)), with intermediate obligations discharged by matching CM2/CM1/CA* to compute 5·24=120, 4·6=24, 3·2=6, 2·1=2, 1·1=1.
  4. Resolve ¬fact(0, s(0)) with CF1 to obtain ⟂ (empty clause).
  5. Therefore fact(s⁵(0), s¹²⁰(0)) follows from the axioms.

We abbreviate sⁿ(0) for readability; each multiplication step is justified by chaining CM2 with addition CA1/CA2.

Check (harness) #1

Concrete computation: 5! (Peano → integer)

Check (harness) #2

Randomized small factorials (n ≤ 6)

Compare Peano factorial with JavaScript’s numeric factorial.

Check (harness) #3

Exhaustive n ∈ {0..5}

Verify 0!..5! match 1,1,2,6,24,120.

Check (harness) #4

Base case

Check that fact(0)=1.

Check (harness) #5

Step rule

Confirm: fact(s(n)) = mult(s(n), fact(n)).

Check (harness) #6

Your data (CSV)

Provide “N: 5” (try 0..7). We compute N! as a Peano term and as a number.

Check (harness) #7

Automated Resolution trace (compressed)

Shows the refutation pattern from ¬fact(5,120) to ⟂ using CF*, CM*, CA*.