Sunday, November 17, 2013
Induction
Linear Induction
| \[ \begin{aligned} &\phi[a] \\ &\forall \mu.(\phi[\mu] \implies \phi[s(\mu]) \\ \hline \\ &\forall \nu.\phi[\nu] \\ \end{aligned} \] |
Tree Induction
| \[ \begin{aligned} &\phi[a] \\ &\forall \mu.(\phi[\mu] \implies \phi[f(\mu]) \\ &\forall \mu.(\phi[\mu] \implies \phi[g(\mu]) \\ \hline \\ &\forall \nu.\phi[\nu] \\ \end{aligned} \] |
Structural Induction
The most general form of induction !
| \[ \begin{aligned} &\phi[a] \\ &\phi[b] \\ &\forall \lambda. \forall \mu.((\phi[\lambda] \land \phi[\mu]) \implies \phi[c(\lambda, \mu)]) \\ \hline \\ &\forall \nu.\phi[\nu] \\ \end{aligned} \] |
More at Introduction to Logic.
