R-and-i-induction-principle
Recursion and Induction: The Induction Principle
The Induction Principle allows one to derive an arbitrary formula, ψ, from
- Base Case :
(implies (and (not q_1) … (not q_k)) ψ), and
- Induction Step(s) : For each 1≤i≤k,
(implies (and q_i ψ/σ_{i,1} … ψ/σ_{i,h_i})
ψ),
provided that for terms m, q_1,...q_k, and substitutions
σ_{i,j} (1≤i≤k, 1≤j≤h_i), the following are
theorems:
- Ordinal Conjecture :
(o-p m), and
- Measure Conjecture(s) : For each 1≤i≤k and 1≤j≤h_i,
(implies q_i (o< m/σ_{i,j} m)).
Next: Relations Between
Recursion and Induction (or Table of Contents)
