logics restricted in arithmetic hierarchy - MathOverflow

logics restricted in arithmetic hierarchy

2010-11-23T21:42:13Z

Hello, I would like to know if this already has been researched.

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.

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 $\Pi^0_2$ .

Has someone worked that out?

Lucas

Answer by Henry Towsner for logics restricted in arithmetic hierarchy

2010-11-24T01:25:53Z

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.

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.

Answer by Kaveh for logics restricted in arithmetic hierarchy

2010-11-25T17:53:12Z

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$.

$\Pi_2$ sentences are extensively studied in proof theory, they are closely related to the provably total functions of the theory.

Answer by François G. Dorais for logics restricted in arithmetic hierarchy

2010-11-25T21:27:04Z

$\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 Questions and Answers — A Category Arising in Linear Logic, Complexity Theory, and Set Theory; in fact, Andreas Blass has several papers on the subject.