φ[x := 0] → [ ∀n [ φ[x := n] → φ[x := n'] ] → ∀x φ ], 여기서 φ는 임의의 논리식이고, '는 다음수 함수입니다.

그런데 n → zero( ), succ( n )이니까 이렇게 바꿔보면 안 될까요?

∀n [ φ[x := n] → φ[x := zero( )] ] ∧ ∀n [ φ[x := n] → φ[x := succ( n )] ] → ∀x  φ.