| 42 |
42 |
|
| 43 |
43 |
|
| 44 |
44 |
\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
|
|
45 |
\begin{definition}\label{def:polynomialinduction}
|
|
46 |
[Polynomial induction]
|
|
47 |
The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,
|
|
48 |
\[
|
|
49 |
A(0)
|
|
50 |
\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
|
|
51 |
\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) )
|
|
52 |
\cimp \forall x^{\normal} . A(x)
|
|
53 |
\]
|
|
54 |
for each formula $A(x)$.
|
| 45 |
55 |
|
|
56 |
For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of induction axioms when $A(x) \in \Xi$.
|
| 46 |
57 |
|
|
58 |
%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
|
|
59 |
\end{definition}
|
|
60 |
|
|
61 |
|
| 47 |
62 |
\begin{definition}
|
| 48 |
63 |
Define the theory $\arith^i$ consisting of the following axioms:
|
| 49 |
64 |
\begin{itemize}
|
| 50 |
65 |
\item $\basic$;
|
| 51 |
66 |
\item $\cpind{\Sigma^\safe_i } $:
|
| 52 |
67 |
\end{itemize}
|
| 53 |
|
and an inference rule:
|
|
68 |
and an inference rule, called $\rais$:
|
| 54 |
69 |
\[
|
| 55 |
70 |
\dfrac{\forall \vec x^\normal . \exists y^\safe . A }{ \forall \vec x^\normal .\exists y^\normal . A}
|
| 56 |
71 |
\]
|
| ... | ... | |
| 174 |
189 |
%The distinction between modal and nonmodal formulae in $(R)$ induces condition 1
|
| 175 |
190 |
Conditions 2 and 3 are standard requirements for nonlogical rules, independently of the logical setting, cf.\ \cite{Beckmann11}. Condition 2 reflects the intuitive idea that, in our nonlogical rules, we often need a notion of \textit{bound} variables in the active formulas (typically for induction rules), for which we rely on eigenvariables. Condition 3 is needed for our proof system to admit elimination of cuts on quantified formulas.
|
| 176 |
191 |
|
|
192 |
%\begin{definition}
|
|
193 |
%[Polynomial induction]
|
|
194 |
%The \emph{polynomial induction} axiom schema, $\pind$, consists of the following axioms,
|
|
195 |
%\[
|
|
196 |
%A(0)
|
|
197 |
%\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{0} x) ) )
|
|
198 |
%\cimp (\forall x^{\normal} . ( A(x) \cimp A(\succ{1} x) ) )
|
|
199 |
%\cimp \forall x^{\normal} . A(x)
|
|
200 |
%\]
|
|
201 |
%for each formula $A(x)$.
|
|
202 |
%
|
|
203 |
%For a class $\Xi$ of formulae, $\cax{\Xi}{\pind}$ denotes the set of induction axioms when $A(x) \in \Xi$.
|
|
204 |
%
|
|
205 |
%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
|
|
206 |
%\end{definition}
|
| 177 |
207 |
|
|
208 |
As an example any axiom can be represented by such a nonlogical rule $(R)$, with no premise ($I=\emptyset$), $\Delta'$ equal to the axiom and $\Gamma=\Sigma'=\Pi$. For instance the axiom $\pind$ of Def. \ref{def:polynomialinduction}.
|
|
209 |
|
|
210 |
Actually $\pind$ is equivalent to the following rule:
|
|
211 |
\begin{equation}
|
|
212 |
\label{eqn:ind-rule}
|
|
213 |
\small
|
|
214 |
\vliinf{\pind}{}{ \normal(t) , \Gamma , A(0) \seqar A(t), \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{0} a) , \Delta }{ \normal(a) , \Gamma, A(a) \seqar A(\succ{1} a) , \Delta }
|
|
215 |
\end{equation}
|
|
216 |
where $I=2$ and in all cases, $t$ varies over arbitrary terms and the eigenvariable $a$ does not occur in the lower sequent of the $\pind$ rule.
|
|
217 |
|
|
218 |
Similarly the $\rais$ inference rule of Def. \ref{} is represented by the rule:
|
|
219 |
\[
|
|
220 |
\begin{array}{cc}
|
|
221 |
\vlinf{\rais}{}{ \Gamma , \Sigma' \seqar \Delta' , \Pi }{ \{\Gamma , \Sigma_i \seqar \Delta_i , \Pi \}_{i \in I} }
|
|
222 |
\end{array}
|
|
223 |
\]
|
| 178 |
224 |
\subsection{Free-cut free normal form of proofs}
|
| 179 |
225 |
\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
|
| 180 |
226 |
|