Révision 254 CSL17/tech-report/arithmetic.tex
| arithmetic.tex (revision 254) | ||
|---|---|---|
| 42 | 42 |
\end{array}
|
| 43 | 43 |
\] |
| 44 | 44 |
Notice that we have $\normal \subseteq \safe$. |
| 45 |
A full list of our $\basic$ axioms can be found in Appendix \ref{appendix:arithmetic}.
|
|
| 46 | 45 |
|
| 46 |
Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
|
|
| 47 |
|
|
| 48 |
\input{appendix-arithmetic}
|
|
| 49 |
|
|
| 47 | 50 |
%\begin{definition}
|
| 48 | 51 |
% [Basic theory] |
| 49 | 52 |
% The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
|
| ... | ... | |
| 160 | 163 |
\begin{figure}
|
| 161 | 164 |
\[ |
| 162 | 165 |
\small |
| 163 |
\hspace{-1.5em}
|
|
| 164 |
\begin{array}{l}
|
|
| 166 |
\hspace{-4em}
|
|
| 165 | 167 |
\begin{array}{cccc}
|
| 166 | 168 |
%\vlinf{\lefrul{\bot}}{}{p, \lnot{p} \seqar }{}
|
| 167 | 169 |
%& \vlinf{\id}{}{p \seqar p}{}
|
| ... | ... | |
| 212 | 214 |
%\noalign{\bigskip}
|
| 213 | 215 |
% \vliinf{mix}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta}{\Sigma \seqar \Pi} &&&
|
| 214 | 216 |
\end{array}
|
| 215 |
\end{array}
|
|
| 216 | 217 |
\] |
| 217 | 218 |
\caption{Sequent calculus rules, where $p$ is atomic, $i \in \{ 1,2 \}$, $t$ is a term and the eigenvariable $a$ does not occur free in $\Gamma$ or $\Delta$.}\label{fig:sequentcalculus}
|
| 218 | 219 |
\end{figure}
|
Formats disponibles : Unified diff