Révision 176
| CSL17/arithmetic.tex (revision 176) | ||
|---|---|---|
| 8 | 8 |
\forall x^\safe . \safe (\succ{} x) \\
|
| 9 | 9 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
| 10 | 10 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
| 11 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )
|
|
| 11 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )\\
|
|
| 12 |
\forall x^\safe, y^\safe . \safe(x+y)\\ |
|
| 13 |
\forall u^\normal, x^\safe . \safe(u\times x) \\ |
|
| 14 |
\forall u^\normal , v^\normal . \safe (u \smsh v) |
|
| 12 | 15 |
\end{array}
|
| 13 | 16 |
\] |
| 14 | 17 |
\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.}
|
| ... | ... | |
| 19 | 22 |
[Derived functions and notations] |
| 20 | 23 |
We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
|
| 21 | 24 |
We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively. |
| 25 |
|
|
| 26 |
Need $bit$, $\beta$ , $\pair{}{}{}$.
|
|
| 22 | 27 |
\end{definition}
|
| 23 | 28 |
|
| 24 | 29 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| ... | ... | |
| 30 | 35 |
|
| 31 | 36 |
\begin{definition}
|
| 32 | 37 |
[Quantifier hierarchy] |
| 33 |
We define: |
|
| 34 |
\begin{itemize}
|
|
| 35 |
\item $\Sigma^\safe_0 = \Pi^\safe_0 $ = sharply bounded formulae. |
|
| 36 |
\item (Increase with predicative quantifiers) |
|
| 37 |
\end{itemize}
|
|
| 38 |
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded. |
|
| 39 |
We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
|
|
| 40 |
We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
|
|
| 38 | 41 |
\end{definition}
|
| 39 | 42 |
|
| 40 | 43 |
|
| CSL17/soundness.tex (revision 176) | ||
|---|---|---|
| 30 | 30 |
% If $A$ is a $\Pi_{i}$ formula then:
|
| 31 | 31 |
\[ |
| 32 | 32 |
\begin{array}{rcl}
|
| 33 |
\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(;s,t) \\
|
|
| 33 |
\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(l;s,t) \\
|
|
| 34 | 34 |
\smallskip |
| 35 |
\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(;s,t) \\
|
|
| 35 |
\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(l;s,t) \\
|
|
| 36 | 36 |
\smallskip |
| 37 | 37 |
\charfn{}{\neg A} (l, \vec u ; \vec x, w) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
|
| 38 | 38 |
\smallskip |
| ... | ... | |
| 45 | 45 |
0 & \text{otherwise}
|
| 46 | 46 |
\end{cases} \\
|
| 47 | 47 |
\smallskip |
| 48 |
\charfn{\vec u; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
|
|
| 48 |
\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
|
|
| 49 | 49 |
\begin{cases}
|
| 50 | 50 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
| 51 | 51 |
1 & \text{otherwise}
|
| ... | ... | |
| 55 | 55 |
\end{definition}
|
| 56 | 56 |
|
| 57 | 57 |
|
| 58 |
\begin{proposition}
|
|
| 59 |
$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
|
| 60 |
\end{proposition}
|
|
| 61 |
|
|
| 58 | 62 |
\begin{definition}
|
| 59 | 63 |
[Length bounded witness function] |
| 60 | 64 |
We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.
|
Formats disponibles : Unified diff