Révision 205 CSL17/soundness.tex
| soundness.tex (revision 205) | ||
|---|---|---|
| 101 | 101 |
|
| 102 | 102 |
|
| 103 | 103 |
\begin{proposition}
|
| 104 |
If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A$ is true.
|
|
| 104 |
If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.
|
|
| 105 | 105 |
\anupam{check statement, need proof-theoretic version?}
|
| 106 | 106 |
\end{proposition}
|
| 107 | 107 |
|
| ... | ... | |
| 118 | 118 |
\wit{\vec u ; \vec x}{\vee \Delta} (l, \vec u ; \vec x , f(l, \vec u ; \vec x , w))
|
| 119 | 119 |
\] |
| 120 | 120 |
\anupam{maybe want $f(\vec u \mode l ; \vec x \mode l , w)$}
|
| 121 |
\anupam{Also, perhaps split for formulae of $\Gamma$, to avoid lots of (de)coding}
|
|
| 121 | 122 |
\end{lemma}
|
| 122 | 123 |
\begin{proof}
|
| 123 | 124 |
We assume the proof, say $\pi$, is in integer positive free-cut free form, by the results from the previous section. |
| ... | ... | |
| 134 | 135 |
|
| 135 | 136 |
\paragraph*{Induction}
|
| 136 | 137 |
Corresponds to safe recursion on notation. |
| 138 |
Suppose final step is: |
|
| 139 |
\[ |
|
| 140 |
\vlinf{\pind}{}{\Gamma , \normal (t) , A(0) \seqar A(t) , \Delta}{ \left\{\Gamma , \normal (u) , A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
|
|
| 141 |
\] |
|
| 142 |
For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}
|
|
| 143 |
|
|
| 144 |
Now, by the inductive hypothesis, we have functions $h_i$ such that: |
|
| 145 |
\[ |
|
| 146 |
\wit{u , \vec u ; \vec x}{LHS} (l , u , \vec u ; \vec x , w) =1
|
|
| 147 |
\quad \implies \quad |
|
| 148 |
\wit{u , \vec u ; \vec x}{RHS} (l , u , \vec u ; \vec x , h_i (u \mode l , \vec u \mode l ; \vec x \mode l) ) =1
|
|
| 149 |
\] |
|
| 150 |
We define $ f$ as follows: |
|
| 151 |
\[ |
|
| 152 |
\begin{array}{rcl}
|
|
| 153 |
f (0 , \vec u ; \vec x, \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn & w^{A(0)} \\
|
|
| 154 |
f( \succ i u , \vec u ; \vec x , \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn &
|
|
| 155 |
h_i (u , \vec u ; \vec x , \vec w^\Gamma w^{\normal (?)}, f(u , \vec u ; \vec x , \vec w ))
|
|
| 156 |
\end{array}
|
|
| 157 |
\] |
|
| 158 |
\anupam{Must check above, could be problems in recursive case.}
|
|
| 159 |
\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}
|
|
| 137 | 160 |
\end{proof}
|
| 138 | 161 |
|
| 139 | 162 |
We are now ready to prove the soundness theorem. |
| ... | ... | |
| 150 | 173 |
\[ |
| 151 | 174 |
\vec u \mode l = \vec a \mode l |
| 152 | 175 |
\quad \implies \quad |
| 153 |
\wit{\vec u ; }{A} ( l , \vec u , f(l, \vec u;) ) =1
|
|
| 176 |
\wit{\vec u ; }{A} ( l , \vec u , f(\vec u \mode l;) ) =1
|
|
| 154 | 177 |
\] |
| 155 |
|
|
| 178 |
|
|
| 156 | 179 |
Now it suffices to choose an $l$ bigger that both all the $\vec u$ and $f(\vec u)$, which is a polynomial in $\vec u$ by the polymax bounding lemma. |
| 157 | 180 |
\end{proof}
|
| 158 | 181 |
|
Formats disponibles : Unified diff