36 P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i & |
36 P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \longrightarrow P_{l_i}~\vec{t}_i & |
37 \mbox{for\ } i=1,\ldots,r |
37 \mbox{for\ } i=1,\ldots,r |
38 \end{array} |
38 \end{array} |
39 \] |
39 \] |
40 |
40 |
41 The (weak) induction rules for the inductive predicates $R_1,\ldots,R_n$ are |
41 The induction principles for the inductive predicates $R_1,\ldots,R_n$ are |
42 |
42 |
43 \[ |
43 \[ |
44 \begin{array}{l@ {\qquad}l} |
44 \begin{array}{l@ {\qquad}l} |
45 R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i & |
45 R_i~\vec{p}~\vec{z}_i \Longrightarrow I_1 \Longrightarrow \cdots \Longrightarrow I_r \Longrightarrow P_i~\vec{z}_i & |
46 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
46 \mbox{for\ } i=1,\ldots,n \\[1.5ex] |
60 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
60 \bigwedge\vec{x}_i.~\vec{A}_i \Longrightarrow \left(\bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow |
61 \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i |
61 \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{k_{ij}}~\vec{s}_{ij}\right)_{j=1,\ldots,m_i} \Longrightarrow \forall P_1 \ldots P_n.~\vec{K} \longrightarrow P_{l_i}~\vec{t}_i |
62 \] |
62 \] |
63 |
63 |
64 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for |
64 where $\vec{K}$ abbreviates $K_1,\ldots,K_r$. Applying the introduction rules for |
65 $\forall$ and $\longrightarrow$ yields a proof state in which we have to prove $P_{l_i}~\vec{t}_i$ |
65 $\forall$ and $\longrightarrow$ yields a goal state in which we have to prove $P_{l_i}~\vec{t}_i$ |
66 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to meta-logic format) |
66 from the additional assumptions $\vec{K}$. When using $K_{l_i}$ (converted to the meta-logic format) |
67 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, |
67 to prove $P_{l_i}~\vec{t}_i$, we get subgoals $\vec{A}_i$ that are trivially solvable by assumption, |
68 as well as subgoals of the form |
68 as well as subgoals of the form |
69 |
69 |
70 \[ |
70 \[ |
71 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i |
71 \bigwedge\vec{y}_{ij}.~\vec{B}_{ij} \Longrightarrow P_{k_{ij}}~\vec{s}_{ij} \qquad \mbox{for\ } j=1,\ldots,m_i |