Révision 254
| CSL17/tech-report/soundness.tex (revision 254) | ||
|---|---|---|
| 51 | 51 |
Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
| 52 | 52 |
\end{proposition}
|
| 53 | 53 |
|
| 54 |
\begin{definition}
|
|
| 55 |
[Length bounded characteristic functions] |
|
| 56 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A$ and a compatible typing $(\vec u ; \vec x)$ of its varables, as follows.
|
|
| 57 |
% If $A$ is a $\Pi_{i}$ formula then:
|
|
| 58 |
\[ |
|
| 59 |
\begin{array}{rcl}
|
|
| 60 |
\charfn{\vec u ; \vec x}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
|
|
| 61 |
\smallskip |
|
| 62 |
% \charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
|
|
| 63 |
% \smallskip |
|
| 64 |
\charfn{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\
|
|
| 65 |
\smallskip |
|
| 66 |
\charfn{\vec u ; \vec x}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \orfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) ) \\
|
|
| 67 |
\smallskip |
|
| 68 |
\charfn{\vec u ; \vec x}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \andfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) )
|
|
| 69 |
% \end{array}
|
|
| 70 |
% \quad |
|
| 71 |
% \begin{array}{rcl}
|
|
| 72 |
\\ \smallskip |
|
| 73 |
\charfn{\vec u ; \vec x}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
|
|
| 74 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
|
|
| 75 |
0 & \text{otherwise}
|
|
| 76 |
\end{cases} \\
|
|
| 77 |
\smallskip |
|
| 78 |
\charfn{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn &
|
|
| 79 |
\begin{cases}
|
|
| 80 |
0 & \exists x^\sigma. \charfn{\vec u ; \vec x}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
|
| 81 |
1 & \text{otherwise}
|
|
| 82 |
\end{cases}
|
|
| 83 |
\end{array}
|
|
| 84 |
\] |
|
| 85 |
\end{definition}
|
|
| 54 | 86 |
|
| 87 |
|
|
| 55 | 88 |
We will use the programs $\charfn{}{}$ in the witness functions we define below.
|
| 56 | 89 |
Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Sigma^\safe_{i}$.
|
| 57 | 90 |
For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'. |
| ... | ... | |
| 154 | 187 |
|
| 155 | 188 |
|
| 156 | 189 |
|
| 190 |
For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.
|
|
| 157 | 191 |
|
| 192 |
\begin{proof}
|
|
| 193 |
Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$. |
|
| 194 |
We define the function $f$ inductively, by considering the various final rules of $\pi$. |
|
| 195 |
|
|
| 196 |
|
|
| 197 |
\paragraph*{Negation}
|
|
| 198 |
Can assume only on atomic formulae, so no effect. |
|
| 199 |
|
|
| 200 |
\paragraph*{Logical rules}
|
|
| 201 |
Pairing, depairing. Need length-boundedness. |
|
| 202 |
|
|
| 203 |
If we have a left conjunction step: |
|
| 204 |
\[ |
|
| 205 |
\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}
|
|
| 206 |
\] |
|
| 207 |
By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that, |
|
| 208 |
\[ |
|
| 209 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)
|
|
| 210 |
\quad \implies \quad |
|
| 211 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))
|
|
| 212 |
\] |
|
| 213 |
for some polynomial $p$. |
|
| 214 |
% |
|
| 215 |
We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$. |
|
| 216 |
|
|
| 217 |
|
|
| 218 |
Right disjunction step: |
|
| 219 |
\[ |
|
| 220 |
\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }
|
|
| 221 |
\] |
|
| 222 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. |
|
| 223 |
Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that: |
|
| 224 |
\[ |
|
| 225 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)
|
|
| 226 |
\quad \implies \quad |
|
| 227 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))
|
|
| 228 |
\] |
|
| 229 |
for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH). |
|
| 230 |
We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.
|
|
| 231 |
\paragraph*{Quantifiers}
|
|
| 232 |
\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
|
|
| 233 |
|
|
| 234 |
|
|
| 235 |
|
|
| 236 |
Sharply bounded quantifiers are generalised versions of logical rules. |
|
| 237 |
\[ |
|
| 238 |
\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar \Delta, A(u) }
|
|
| 239 |
\] |
|
| 240 |
By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that: |
|
| 241 |
\[ |
|
| 242 |
\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )
|
|
| 243 |
\quad \implies \quad |
|
| 244 |
\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
|
|
| 245 |
\] |
|
| 246 |
with $|f|\leq q(|l|)$. |
|
| 247 |
|
|
| 248 |
By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....
|
|
| 249 |
|
|
| 250 |
We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w )$.
|
|
| 251 |
|
|
| 252 |
|
|
| 253 |
Right existential: |
|
| 254 |
\[ |
|
| 255 |
\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}
|
|
| 256 |
\] |
|
| 257 |
Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form. |
|
| 258 |
|
|
| 259 |
|
|
| 260 |
\paragraph*{Contraction}
|
|
| 261 |
Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula. |
|
| 262 |
|
|
| 263 |
\[ |
|
| 264 |
\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}
|
|
| 265 |
\] |
|
| 266 |
|
|
| 267 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss. |
|
| 268 |
We define: |
|
| 269 |
\[ |
|
| 270 |
f^\pi_A ( \vec u ; \vec x , \vec w ) |
|
| 271 |
\quad \dfn \quad |
|
| 272 |
\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(\vec u ; \vec x , \vec w) ) , f_1(\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w) )
|
|
| 273 |
\] |
|
| 274 |
|
|
| 275 |
|
|
| 276 |
\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }
|
|
| 277 |
\paragraph*{Induction}
|
|
| 278 |
Corresponds to safe recursion on notation. |
|
| 279 |
Suppose final step is (wlog): |
|
| 280 |
\[ |
|
| 281 |
\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
|
|
| 282 |
\] |
|
| 283 |
\anupam{need to say in normal form part that can assume induction of this form}
|
|
| 284 |
For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}
|
|
| 285 |
|
|
| 286 |
Now, by the inductive hypothesis, we have functions $h_i$ such that: |
|
| 287 |
\[ |
|
| 288 |
\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x , \vec w)
|
|
| 289 |
\quad \implies \quad |
|
| 290 |
\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x , h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )
|
|
| 291 |
\] |
|
| 292 |
First let us define $ f$ as follows: |
|
| 293 |
\[ |
|
| 294 |
\begin{array}{rcl}
|
|
| 295 |
f (0 , \vec u ; \vec x, \vec w, w ) & \dfn & w\\ |
|
| 296 |
f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & |
|
| 297 |
h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w )) |
|
| 298 |
\end{array}
|
|
| 299 |
\] |
|
| 300 |
where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$. |
|
| 301 |
\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.}
|
|
| 302 |
|
|
| 303 |
Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$. |
|
| 304 |
|
|
| 305 |
\paragraph*{Cut}
|
|
| 306 |
If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position. |
|
| 307 |
Otherwise it is a `raisecut': |
|
| 308 |
\[ |
|
| 309 |
\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe . A(x) }{ \normal (u) , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }
|
|
| 310 |
\] |
|
| 311 |
In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as: |
|
| 312 |
\[ |
|
| 313 |
\vec f^\pi ( \vec u , \vec v ; \vec x , \vec w ) |
|
| 314 |
\quad \dfn \quad |
|
| 315 |
\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w ) |
|
| 316 |
\] |
|
| 317 |
\end{proof}
|
|
| 318 |
|
|
| 319 |
|
|
| 320 |
|
|
| 321 |
|
|
| 322 |
|
|
| 323 |
|
|
| 158 | 324 |
Now we can prove the soundness result: |
| 159 | 325 |
|
| 160 | 326 |
\begin{proof}
|
| CSL17/tech-report/main.tex (revision 254) | ||
|---|---|---|
| 1 |
\documentclass[a4paper]{amsart}
|
|
| 1 |
\documentclass[a4paper]{article}
|
|
| 2 | 2 |
|
| 3 | 3 |
\usepackage{amsmath}
|
| 4 | 4 |
\usepackage{amsthm}
|
| ... | ... | |
| 14 | 14 |
\usepackage[lutzsyntax]{virginialake}
|
| 15 | 15 |
\input{ph-macros}
|
| 16 | 16 |
|
| 17 |
\begin{document}
|
|
| 17 | 18 |
|
| 18 |
\title[Polynomial hierarchy in an unbounded arithmetic]{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic}
|
|
| 19 |
\title{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic}
|
|
| 19 | 20 |
|
| 20 | 21 |
\author{Patrick Baillot}
|
| 21 | 22 |
\author{Anupam Das}
|
| 22 | 23 |
|
| 23 | 24 |
|
| 24 |
\begin{document}
|
|
| 25 | 25 |
|
| 26 |
|
|
| 26 | 27 |
\maketitle |
| 27 | 28 |
|
| 28 | 29 |
\begin{abstract}
|
| ... | ... | |
| 64 | 65 |
|
| 65 | 66 |
\newpage |
| 66 | 67 |
\appendix |
| 67 |
\input{appendix-arithmetic}
|
|
| 68 |
|
|
| 68 | 69 |
%%\input{pv-theories}
|
| 69 |
%\input{appendix-sequent-calculus}
|
|
| 70 |
%\input{appendix-soundness}
|
|
| 70 |
\input{appendix-sequent-calculus}
|
|
| 71 |
|
|
| 71 | 72 |
\input{appendix-completeness}
|
| 72 | 73 |
|
| 73 | 74 |
\end{document}
|
| CSL17/tech-report/appendix-soundness.tex (revision 254) | ||
|---|---|---|
| 1 |
\section{Proof of soundness}
|
|
| 1 |
%\section{Proof of soundness}
|
|
| 2 | 2 |
|
| 3 |
\begin{definition}
|
|
| 4 |
[Length bounded characteristic functions] |
|
| 5 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A$ and a compatible typing $(\vec u ; \vec x)$ of its varables, as follows.
|
|
| 6 |
% If $A$ is a $\Pi_{i}$ formula then:
|
|
| 7 |
\[ |
|
| 8 |
\begin{array}{rcl}
|
|
| 9 |
\charfn{\vec u ; \vec x}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
|
|
| 10 |
\smallskip |
|
| 11 |
% \charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
|
|
| 12 |
% \smallskip |
|
| 13 |
\charfn{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\
|
|
| 14 |
\smallskip |
|
| 15 |
\charfn{\vec u ; \vec x}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \orfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) ) \\
|
|
| 16 |
\smallskip |
|
| 17 |
\charfn{\vec u ; \vec x}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \andfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) )
|
|
| 18 |
% \end{array}
|
|
| 19 |
% \quad |
|
| 20 |
% \begin{array}{rcl}
|
|
| 21 |
\\ \smallskip |
|
| 22 |
\charfn{\vec u ; \vec x}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
|
|
| 23 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
|
|
| 24 |
0 & \text{otherwise}
|
|
| 25 |
\end{cases} \\
|
|
| 26 |
\smallskip |
|
| 27 |
\charfn{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn &
|
|
| 28 |
\begin{cases}
|
|
| 29 |
0 & \exists x^\sigma. \charfn{\vec u ; \vec x}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
|
| 30 |
1 & \text{otherwise}
|
|
| 31 |
\end{cases}
|
|
| 32 |
\end{array}
|
|
| 33 |
\] |
|
| 34 |
\end{definition}
|
|
| 35 |
|
|
| 36 |
For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.
|
|
| 37 |
|
|
| 38 |
\begin{proof}
|
|
| 39 |
Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$. |
|
| 40 |
We define the function $f$ inductively, by considering the various final rules of $\pi$. |
|
| 41 |
|
|
| 42 |
|
|
| 43 |
\paragraph*{Negation}
|
|
| 44 |
Can assume only on atomic formulae, so no effect. |
|
| 45 |
|
|
| 46 |
\paragraph*{Logical rules}
|
|
| 47 |
Pairing, depairing. Need length-boundedness. |
|
| 48 |
|
|
| 49 |
If we have a left conjunction step: |
|
| 50 |
\[ |
|
| 51 |
\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}
|
|
| 52 |
\] |
|
| 53 |
By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that, |
|
| 54 |
\[ |
|
| 55 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)
|
|
| 56 |
\quad \implies \quad |
|
| 57 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))
|
|
| 58 |
\] |
|
| 59 |
for some polynomial $p$. |
|
| 60 |
% |
|
| 61 |
We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$. |
|
| 62 |
|
|
| 63 |
|
|
| 64 |
Right disjunction step: |
|
| 65 |
\[ |
|
| 66 |
\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }
|
|
| 67 |
\] |
|
| 68 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. |
|
| 69 |
Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that: |
|
| 70 |
\[ |
|
| 71 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)
|
|
| 72 |
\quad \implies \quad |
|
| 73 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))
|
|
| 74 |
\] |
|
| 75 |
for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH). |
|
| 76 |
We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.
|
|
| 77 |
\paragraph*{Quantifiers}
|
|
| 78 |
\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
|
|
| 79 |
|
|
| 80 |
|
|
| 81 |
|
|
| 82 |
Sharply bounded quantifiers are generalised versions of logical rules. |
|
| 83 |
\[ |
|
| 84 |
\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar \Delta, A(u) }
|
|
| 85 |
\] |
|
| 86 |
By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that: |
|
| 87 |
\[ |
|
| 88 |
\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )
|
|
| 89 |
\quad \implies \quad |
|
| 90 |
\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
|
|
| 91 |
\] |
|
| 92 |
with $|f|\leq q(|l|)$. |
|
| 93 |
|
|
| 94 |
By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....
|
|
| 95 |
|
|
| 96 |
We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w )$.
|
|
| 97 |
|
|
| 98 |
|
|
| 99 |
Right existential: |
|
| 100 |
\[ |
|
| 101 |
\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}
|
|
| 102 |
\] |
|
| 103 |
Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form. |
|
| 104 |
|
|
| 105 |
|
|
| 106 |
\paragraph*{Contraction}
|
|
| 107 |
Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula. |
|
| 108 |
|
|
| 109 |
\[ |
|
| 110 |
\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}
|
|
| 111 |
\] |
|
| 112 |
|
|
| 113 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss. |
|
| 114 |
We define: |
|
| 115 |
\[ |
|
| 116 |
f^\pi_A ( \vec u ; \vec x , \vec w ) |
|
| 117 |
\quad \dfn \quad |
|
| 118 |
\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(\vec u ; \vec x , \vec w) ) , f_1(\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w) )
|
|
| 119 |
\] |
|
| 120 |
|
|
| 121 |
|
|
| 122 |
\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }
|
|
| 123 |
\paragraph*{Induction}
|
|
| 124 |
Corresponds to safe recursion on notation. |
|
| 125 |
Suppose final step is (wlog): |
|
| 126 |
\[ |
|
| 127 |
\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
|
|
| 128 |
\] |
|
| 129 |
\anupam{need to say in normal form part that can assume induction of this form}
|
|
| 130 |
For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}
|
|
| 131 |
|
|
| 132 |
Now, by the inductive hypothesis, we have functions $h_i$ such that: |
|
| 133 |
\[ |
|
| 134 |
\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x , \vec w)
|
|
| 135 |
\quad \implies \quad |
|
| 136 |
\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x , h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )
|
|
| 137 |
\] |
|
| 138 |
First let us define $ f$ as follows: |
|
| 139 |
\[ |
|
| 140 |
\begin{array}{rcl}
|
|
| 141 |
f (0 , \vec u ; \vec x, \vec w, w ) & \dfn & w\\ |
|
| 142 |
f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & |
|
| 143 |
h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w )) |
|
| 144 |
\end{array}
|
|
| 145 |
\] |
|
| 146 |
where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$. |
|
| 147 |
\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.}
|
|
| 148 |
|
|
| 149 |
Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$. |
|
| 150 |
|
|
| 151 |
\paragraph*{Cut}
|
|
| 152 |
If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position. |
|
| 153 |
Otherwise it is a `raisecut': |
|
| 154 |
\[ |
|
| 155 |
\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe . A(x) }{ \normal (u) , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }
|
|
| 156 |
\] |
|
| 157 |
In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as: |
|
| 158 |
\[ |
|
| 159 |
\vec f^\pi ( \vec u , \vec v ; \vec x , \vec w ) |
|
| 160 |
\quad \dfn \quad |
|
| 161 |
\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w ) |
|
| 162 |
\] |
|
| 163 |
\end{proof}
|
|
| 164 |
|
|
| CSL17/tech-report/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}
|
| CSL17/tech-report/intro.tex (revision 254) | ||
|---|---|---|
| 55 | 55 |
%Then we describe an encoding of sequences which will be instrumental in the proof of our result. |
| 56 | 56 |
We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and give our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we sketch the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
|
| 57 | 57 |
|
| 58 |
We are able to include only brief accounts of our technical results in this paper due to space constraints, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively.
|
|
| 59 |
More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
|
|
| 58 |
% We are able to include only brief accounts of our technical results in this paper due to space constraints, in particular for our soundness and completeness results, Thms.~\ref{sect:soundness} and \ref{thm:completeness} respectively.
|
|
| 59 |
% More detailed proofs can be found in the technical report \cite{BaiDas17:fph-techreport}.
|
|
| 60 | 60 |
|
| 61 | 61 |
|
| 62 | 62 |
% \patrick{
|
| CSL17/tech-report/appendix-arithmetic.tex (revision 254) | ||
|---|---|---|
| 1 |
\section{Appendix: remaining axioms of $\basic$}\label{appendix:arithmetic}
|
|
| 2 |
|
|
| 3 |
We give here the list of remaining axioms of $\basic$, which are directly inspired by the $\basic$ theory of Buss's bounded arithmetic \cite{Buss86book}:
|
|
| 4 |
%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
|
| 5 |
|
|
| 6 |
|
|
| 1 |
%\section{Appendix: remaining axioms of $\basic$}\label{appendix:arithmetic}
|
|
| 2 |
% |
|
| 3 |
%We give here the list of remaining axioms of $\basic$, which are directly inspired by the $\basic$ theory of Buss's bounded arithmetic \cite{Buss86book}:
|
|
| 4 |
%%$\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
|
| 5 |
% |
|
| 6 |
% |
|
| 7 | 7 |
$$ |
| 8 | 8 |
%\begin{equation}
|
| 9 | 9 |
\begin{array}{l}
|
Formats disponibles : Unified diff