Révision 265
| CSL17/tech-report/arithmetic.tex (revision 265) | ||
|---|---|---|
| 210 | 210 |
% |
| 211 | 211 |
%\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
|
| 212 | 212 |
|
| 213 |
\anupam{Need vector $\vec y^\safe$?}
|
|
| 214 |
|
|
| 213 | 215 |
\begin{remark}
|
| 214 | 216 |
Notice that $\rais$ looks similar to the $K$ rule from the calculus for the modal logic $S4$ (which subsumes necessitation), and indeed we believe there is a way to present these results in such a framework. |
| 215 | 217 |
However, the proof theory of first-order modal logics, in particular free-cut elimination results used for witnessing, is not sufficiently developed to carry out such an exposition. |
| ... | ... | |
| 231 | 233 |
\todo{Proof: Patrick? The final two should require PIND.}
|
| 232 | 234 |
|
| 233 | 235 |
\patrick{Actually statement 4 is nearly trivial from axiom 27 (for which I corrected the sorts). Maybe you meant something else?
|
| 236 |
\anupam{I actually changed those sorts from the submitted version: I really think axiom 27 should be $\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x$, i.e.\ with the recursion on the normal variable. That way we can do induction on it. Statement 4 is meant to state the recursive property for the safe argument, which we can prove by induction on the normal argument, $u$.}
|
|
| 234 | 237 |
|
| 235 | 238 |
For statement 3 I replaced the quantifications $\safe$ by $\normal$, otherwise I don't know how to prove it. But I think we need the stronger statement with $\safe$, so probably we should add it as an additional axiom.} |
| 239 |
\anupam{Rather, I do not know how you would prove the current version: we cannot induct on $\exists v^\normal$ from axiom 27 as I state it. For the previous version I would just do induction on $u$ in $(u = 0 \cor \exists x^\safe.\ u = \succ{} x )$. }
|
|
| 236 | 240 |
\end{example}
|
| 237 | 241 |
\begin{proof}
|
| 238 | 242 |
\begin{itemize}
|
| CSL17/tech-report/soundness.tex (revision 265) | ||
|---|---|---|
| 166 | 166 |
[Proof interpretation] |
| 167 | 167 |
\label{lem:proof-interp}
|
| 168 | 168 |
From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma \seqar \Delta$ |
| 169 |
there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
|
|
| 169 |
there are $\bc (\charfn{}{i-1})$ functions $ f^\pi_B (\vec u ; \vec x , \vec w)$ for $B\in\Delta$ such that
|
|
| 170 | 170 |
% such that, for any $l, \vec u ; \vec x , w$, we have: |
| 171 | 171 |
\[ |
| 172 | 172 |
% \vec a^\nu = \vec u , |
| ... | ... | |
| 195 | 195 |
|
| 196 | 196 |
|
| 197 | 197 |
\paragraph*{Negation}
|
| 198 |
Can assume only on atomic formulae, so no effect. |
|
| 198 |
Suppose $\pi$ ends with a right negation step: |
|
| 199 |
\[ |
|
| 200 |
\vlinf{\rigrul{\cnot}}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \cnot A , \Delta }{\normal (\vec u) , \safe (\vec x) , \Gamma , A\seqar \Delta}
|
|
| 201 |
\] |
|
| 202 |
Notice that, since $\pi$ is in De Morgan form, we have that $A$ is atomic ($s\leq t$) and so, in particular, $\Pi^\safe_{i-1}$.
|
|
| 203 |
So we can simply set the witness for both $A$ and $\cnot A$ to $0$. |
|
| 204 |
Namely, if $\vec f (\vec u ; \vec x , \vec w , w )$ is obtained by the inductive hypothesis, then we may set $f^\pi_B ( \vec u ; \vec x , \vec w) \dfn f_B (\vec u ;\vec x , \vec w , 0)$ for $B\in \Delta$, and $f^\pi_A (\vec u ; \vec x , \vec w) \dfn 0$. |
|
| 205 |
The bounding polynomial remains the same. |
|
| 199 | 206 |
|
| 200 | 207 |
\paragraph*{Logical rules}
|
| 201 | 208 |
Pairing, depairing. Need length-boundedness. |
Formats disponibles : Unified diff