Révision 177 CSL17/arithmetic.tex
| arithmetic.tex (revision 177) | ||
|---|---|---|
| 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 |
|
Formats disponibles : Unified diff