Révision 180 CSL17/arithmetic.tex
| arithmetic.tex (revision 180) | ||
|---|---|---|
| 12 | 12 |
\forall x^\safe, y^\safe . \safe(x+y)\\ |
| 13 | 13 |
\forall u^\normal, x^\safe . \safe(u\times x) \\ |
| 14 | 14 |
\forall u^\normal , v^\normal . \safe (u \smsh v)\\ |
| 15 |
\patrick{\forall u^\normal \safe(u) \; ?}
|
|
| 15 |
\forall u^\normal \safe(u)
|
|
| 16 | 16 |
\end{array}
|
| 17 | 17 |
\] |
| 18 | 18 |
\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}
|
| ... | ... | |
| 67 | 67 |
\item $\basic$; |
| 68 | 68 |
\item $\cpind{\Sigma^\safe_i } $:
|
| 69 | 69 |
\end{itemize}
|
| 70 |
and an inference rule, called $\rais$: |
|
| 70 |
and an inference rule, called $\rais$, for closed formulas $\exists y^\normal . A$:
|
|
| 71 | 71 |
\[ |
| 72 | 72 |
\dfrac{\forall \vec x^\normal . \exists y^\safe . A }{ \forall \vec x^\normal .\exists y^\normal . A}
|
| 73 | 73 |
\] |
| 74 |
\patrick{For $\forall \vec x^\normal . \exists y^\safe . A$ closed ?}
|
|
| 74 |
%\patrick{For $\forall \vec x^\normal . \exists y^\safe . A$ closed ?}
|
|
| 75 | 75 |
\end{definition}
|
| 76 | 76 |
\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
|
| 77 | 77 |
|
| ... | ... | |
| 115 | 115 |
%& \vlinf{\id}{}{p \seqar p}{}
|
| 116 | 116 |
%& \vlinf{\rigrul{\bot}}{}{\seqar p, \lnot{p}}{}
|
| 117 | 117 |
%& \vliinf{\cut}{}{\Gamma, \Sigma \seqar \Delta , \Pi}{ \Gamma \seqar \Delta, A }{\Sigma, A \seqar \Pi}
|
| 118 |
\vlinf{id}{}{p \seqar p}{}
|
|
| 118 |
\vlinf{id}{}{\Gamma, p \seqar p, \Delta }{}
|
|
| 119 | 119 |
& \vliinf{cut}{}{\Gamma \seqar \Delta }{ \Gamma \seqar \Delta, A }{\Gamma, A \seqar \Delta}
|
| 120 | 120 |
&& |
| 121 | 121 |
\\ |
| ... | ... | |
| 153 | 153 |
%\text{Structural:} & & & \\
|
| 154 | 154 |
%\noalign{\bigskip}
|
| 155 | 155 |
|
| 156 |
\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
|
|
| 157 |
& |
|
| 156 |
%\vlinf{\lefrul{\wk}}{}{\Gamma, A \seqar \Delta}{\Gamma \seqar \Delta}
|
|
| 157 |
%&
|
|
| 158 | 158 |
\vlinf{\lefrul{\cntr}}{}{\Gamma, A \seqar \Delta}{\Gamma, A, A \seqar \Delta}
|
| 159 |
%& |
|
| 160 |
%\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
|
|
| 159 | 161 |
& |
| 160 |
\vlinf{\rigrul{\wk}}{}{\Gamma \seqar \Delta, A }{\Gamma \seqar \Delta}
|
|
| 162 |
\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
|
|
| 161 | 163 |
& |
| 162 |
\vlinf{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, A}{\Gamma \seqar \Delta, A, A}
|
|
| 164 |
&
|
|
| 163 | 165 |
\\ |
| 164 | 166 |
\noalign{\bigskip}
|
| 165 | 167 |
\vlinf{\lefrul{\exists}}{}{\Gamma, \exists x . A(x) \seqar \Delta}{\Gamma, A(a) \seqar \Delta}
|
| ... | ... | |
| 253 | 255 |
\vlinf{}{}{\normal (s), \safe(t) \seqar \safe(s \times t) }{}
|
| 254 | 256 |
\qquad |
| 255 | 257 |
\vlinf{}{}{\normal (s), \normal(t) \seqar \safe(s \smsh t) }{}\\
|
| 256 |
\patrick{\vlinf{}{}{\normal(t) \seqar \safe(t) }{}}
|
|
| 258 |
\vlinf{}{}{\normal(t) \seqar \safe(t) }{}
|
|
| 257 | 259 |
\end{array}
|
| 258 | 260 |
\] |
| 259 | 261 |
|
Formats disponibles : Unified diff