Peano Factorial • 5! = 120 proved via Resolution

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.

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

Resolution justification (clausal refutation, sketched)

1. Clausify the Horn implications (move antecedents to the left as negated disjuncts):
   C_A1: add(X, 0, X)
   C_A2: ¬add(X, Y, Z) ∨ add(X, s(Y), s(Z))
   C_M1: mult(X, 0, 0)
   C_M2: ¬mult(X, Y, Z) ∨ ¬add(Z, X, Z2) ∨ mult(X, s(Y), Z2)
   C_F1: fact(0, s(0))
   C_F2: ¬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 C_F2 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 C_M2/C_M1/C_A* to compute 5·24=120, 4·6=24, 3·2=6, 2·1=2, 1·1=1.
4. Resolve ¬fact(0, s(0)) with C_F1 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 C_M2 with addition C_A1/C_A2.

Concrete computation: 5! (Peano → integer)

Randomized small factorials (n ≤ 6)

Compare Peano factorial with JavaScript’s numeric factorial.

Exhaustive n ∈ {0..5}

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

Base case

Check that fact(0)=1.

Step rule

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

Your data (CSV)

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

Automated Resolution trace (compressed)

Shows the refutation pattern from ¬fact(5,120) to ⟂ using C_F*, C_M*, C_A*.