Révision 265 CSL17/tech-report/arithmetic.tex
| 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}
|
Formats disponibles : Unified diff