/CSL17/tech-report/arithmetic.tex - Diff - Linear Arithmetic - Forge du Centre Blaise Pascal

Révision 262 CSL17/tech-report/arithmetic.tex

     As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae `immediately' below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
     Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
     Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers \cite{Buss86book}, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
     \[
     \vlinf{\rigrul{\forall}}{}{ \normal(\vec u) , \safe (\vec x), \Gamma \seqar \Delta , \forall x^\safe . A(x)}{\normal(\vec u ) , \safe (\vec x), \safe (x) , \Gamma \seqar \Delta, A(x)}
     \quad

Formats disponibles : Unified diff