Révision 178 CSL17/arithmetic.tex
| arithmetic.tex (revision 178) | ||
|---|---|---|
| 59 | 59 |
\end{definition}
|
| 60 | 60 |
|
| 61 | 61 |
|
| 62 |
\begin{definition}
|
|
| 62 |
\begin{definition}\label{def:ariththeory}
|
|
| 63 | 63 |
Define the theory $\arith^i$ consisting of the following axioms: |
| 64 | 64 |
\begin{itemize}
|
| 65 | 65 |
\item $\basic$; |
| ... | ... | |
| 215 | 215 |
\end{equation}
|
| 216 | 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 | 217 |
|
| 218 |
Similarly the $\rais$ inference rule of Def. \ref{} is represented by the rule:
|
|
| 218 |
Similarly the $\rais$ inference rule of Def. \ref{def:ariththeory} is represented by the nonlogical rule:
|
|
| 219 | 219 |
\[ |
| 220 | 220 |
\begin{array}{cc}
|
| 221 |
\vlinf{\rais}{}{ \Gamma , \Sigma' \seqar \Delta' , \Pi }{ \{\Gamma , \Sigma_i \seqar \Delta_i , \Pi \}_{i \in I} }
|
|
| 221 |
\vlinf{\rais}{}{ \Gamma \seqar \forall \vec x^\normal . \exists y^\normal . A , \Pi }{ \Gamma \seqar \forall \vec x^\normal . \exists y^\safe . A, \Pi }
|
|
| 222 | 222 |
\end{array}
|
| 223 | 223 |
\] |
| 224 |
The sequent calculus for $\arith^i$ is that of Fig. \ref{fig:sequentcalculus} extended with nonlogical rules for the axioms of $\basic$, $\cpind{\Sigma^\safe_i } $ and $\rais$.
|
|
| 224 | 225 |
\subsection{Free-cut free normal form of proofs}
|
| 225 | 226 |
\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
|
| 226 | 227 |
|
| ... | ... | |
| 246 | 247 |
\label{thm:free-cut-elim}
|
| 247 | 248 |
Given a system $\mathcal{S}$, any $\mathcal{S}$-proof $\pi$ can be transformed into a $\system$-proof $\pi'$ with same end sequent and without any free-cut.
|
| 248 | 249 |
\end{theorem}
|
| 249 |
\todo{state as a corollary a suitable subformula property.}
|
|
| 250 |
% \begin{proposition}
|
|
| 251 |
% |
|
| 252 |
% \end{proposition}
|
|
Formats disponibles : Unified diff