logics restricted in arithmetic hierarchy - MathOverflow most recent 30 from http://mathoverflow.net 2013-06-19T05:28:36Z http://mathoverflow.net/feeds/question/47150 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/47150/logics-restricted-in-arithmetic-hierarchy logics restricted in arithmetic hierarchy Lucas K. 2010-11-23T21:42:13Z 2010-11-27T23:16:13Z <p>Hello, I would like to know if this already has been researched.</p> <p>There has been lot of research done, where logics are limited. They are often limited in the axioms or inference rules, which makes them weaker.</p> <p>However, I am interested if someone has researched logics that are limited in arithmetic hierarchy. I am interested in a system that has only sentences of <code>$\Pi^0_2$</code>.</p> <p>Has someone worked that out?</p> <p>Lucas</p> http://mathoverflow.net/questions/47150/logics-restricted-in-arithmetic-hierarchy/47171#47171 Answer by Henry Towsner for logics restricted in arithmetic hierarchy Henry Towsner 2010-11-24T01:25:53Z 2010-11-27T23:16:13Z <p>There are some theories which, in essence, have only $\Pi^0_2$ formulas, in a way which I think captures what you're trying to capture. These theories are actually entirely quantifier free, but they allow free variables. A proof of some statement like $\phi(x,t)$ where $t$ is a term containing $x$ free is then viewed as a proof that $\forall x\exists y\phi(x,y)$. This only makes sense if you expect your witness $y$ to be given explicitly by a term, but that's often true, and will certainly be true if the kinds of things you're thinking about are Turing machines and discrete math.</p> <p>Primitive recursive arithmetic is sometimes presented like this, and Godel's theory T (a theory of functionals) has this form as well. T is very similar to the $\lambda$-calculus, and I believe some theories of $\lambda$-calculus are also presented in the same way.</p> http://mathoverflow.net/questions/47150/logics-restricted-in-arithmetic-hierarchy/47347#47347 Answer by Kaveh for logics restricted in arithmetic hierarchy Kaveh 2010-11-25T17:53:12Z 2010-11-25T17:53:12Z <p>You can Skolemize a theory to get a universal theory which is a conservative extension of the original theory. By Gentzen's cut-elimination theorem, any formula provable in this theory has a proof where all formulas are subformulas of the theorem and axioms of the theory. If you are proving a $\Pi_2$ formula, all formulas in the proof will be $\Pi_2$.</p> <p>$\Pi_2$ sentences are extensively studied in proof theory, they are closely related to the provably total functions of the theory.</p> http://mathoverflow.net/questions/47150/logics-restricted-in-arithmetic-hierarchy/47376#47376 Answer by François G. Dorais for logics restricted in arithmetic hierarchy François G. Dorais 2010-11-25T21:27:04Z 2010-11-25T21:27:04Z <p>$\Pi_2$ statements can be modeled in the form of a "question and answer." Specifically, the statement $(\forall a \in A)(\exists b \in B)\phi(a,b)$ can be thought of as follows: $A$ is a set of questions, $B$ is a set of answers, and $\phi(a,b)$ determines whether $b$ is a correct answer to question $a$. It turns out that this scenario lends itself to interpreting Girard's Linear Logic. This is described in detail by Andreas Blass in <a href="http://www.math.lsa.umich.edu/~ablass/qa.pdf" rel="nofollow">Questions and Answers &mdash; A Category Arising in Linear Logic, Complexity Theory, and Set Theory</a>; in fact, Andreas Blass has <a href="http://www.math.lsa.umich.edu/~ablass/ll.html" rel="nofollow">several papers on the subject</a>.</p>