Révision 173 CSL17/soundness.tex
| soundness.tex (revision 173) | ||
|---|---|---|
| 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 |
| 39 |
\charfn{}{A\cor B} (l, \vec u ; \vec x , w) & \dfn & \cor (; \charfn{}{A} (\vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 39 |
\charfn{}{A\cor B} (l, \vec u ; \vec x , w) & \dfn & \cor (; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 40 | 40 |
\smallskip |
| 41 |
\charfn{}{A\cand B} (l, \vec u ; \vec x , w) & \dfn & \cand(; \charfn{}{A} (\vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 41 |
\charfn{}{A\cand B} (l, \vec u ; \vec x , w) & \dfn & \cand(; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 42 | 42 |
\smallskip |
| 43 | 43 |
\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x, w) & \dfn & \begin{cases}
|
| 44 |
1 & \exists x^\safe . \charfn{}{A(x)} (\vec u ;\vec x , x, w) = 1 \\
|
|
| 44 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x, w) = 1 \\
|
|
| 45 | 45 |
0 & \text{otherwise}
|
| 46 | 46 |
\end{cases} \\
|
| 47 | 47 |
\smallskip |
| 48 | 48 |
\charfn{\vec u; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
|
| 49 | 49 |
\begin{cases}
|
| 50 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (\vec u; \vec x , x) = 0 \\
|
|
| 50 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
|
| 51 | 51 |
1 & \text{otherwise}
|
| 52 | 52 |
\end{cases}
|
| 53 | 53 |
\end{array}
|
| 54 | 54 |
\] |
| 55 |
\end{definition}
|
|
| 55 |
\end{definition}
|
|
| 56 |
|
|
| 57 |
|
|
| 58 |
\begin{definition}
|
|
| 59 |
[Length bounded witness function] |
|
| 60 |
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$.
|
|
| 61 |
\[ |
|
| 62 |
\begin{array}{rcl}
|
|
| 63 |
\Wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x) \text{ if $A$ is $\Pi_i$} \\
|
|
| 64 |
\smallskip |
|
| 65 |
\Wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B) ) \\
|
|
| 66 |
\smallskip |
|
| 67 |
\Wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B) ) \\
|
|
| 68 |
\smallskip |
|
| 69 |
\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )
|
|
| 70 |
\\ |
|
| 71 |
\smallskip |
|
| 72 |
\Wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn &
|
|
| 73 |
\forall u \leq |t(\vec u;)| . \Wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
|
|
| 74 |
\end{array}
|
|
| 75 |
\] |
|
| 76 |
\end{definition}
|
|
| 77 |
|
|
| 78 |
\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
|
|
| 79 |
|
|
| 80 |
\anupam{sharply bounded case obtained by sharply bounded lemma}
|
|
Formats disponibles : Unified diff