2
$\begingroup$

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

Improve this question
$\endgroup$
5
  • $\begingroup$ What do you mean by $\Pi^0_2$? Do you want only formulas of the form $\forall x_1\forall x_2\cdots\forall x_n\exists y_1\cdots\exists y_m \phi(x_1,\ldots,y_1,\ldots)$, or do you want to allow combinations of such formulas as well? $\endgroup$
    – Henry Towsner
    Commented Nov 23, 2010 at 22:28
  • $\begingroup$ The sentence does not need to be in the standard form, as long as it can be converted to a $\Pi^0_2$ sentence in a automated way. $\endgroup$
    – Lucas K.
    Commented Nov 23, 2010 at 22:37
  • $\begingroup$ There are a few example of theories where the syntax is restricted; probably the most common is that PRA is often defined as outright not having quantifiers. But allowing exactly formulas equivalent to $\Pi^0_2$ seems very unnatural; for instance, your formulas wouldn't be closed under negation. I guess it might help to know what your motivation is; I have trouble believing that literally restricting the syntax to exactly the $\Pi^0_2$ formulas is the right way to accomplish it. $\endgroup$
    – Henry Towsner
    Commented Nov 23, 2010 at 22:51
  • $\begingroup$ My motivation comes from foundation of mathematics. I concluded that $\Pi^0_2$ sentences are very important. Most questions in logic are $\Pi^0_2$. Furthermore, I discovered when making a computer program, the puzzles to be solved are of $\Pi^0_2$ nature. $\Pi^0_2$ sentences can be expressed as the equivalence of two Turing programs with input. And, finally I read that $\Pi^0_2$ sentences have absoluteness, although I do not entire understand that concept. So, I was curious if one could restrict logic to these sentences. And indeed, not allowing negation in some cases. $\endgroup$
    – Lucas K.
    Commented Nov 23, 2010 at 23:00
  • $\begingroup$ In addition to my previous comment. It may look unnatural, but that depends on the view you take. If you look at actual problems, then $\Pi^0_2$ sentences are a very important set and covers almost all problems in discrete mathematics. You hardly need more arithmetic depth than that. Sentences with more depth might be also be constructed via a meta-level. So, one can also say that it is quite unnatural to allow arbitrary depth. $\endgroup$
    – Lucas K.
    Commented Nov 23, 2010 at 23:20

3 Answers 3

Reset to default
2
$\begingroup$

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

Improve this answer
$\endgroup$
0
6
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ I should add that, in general, a huge portion of proof theory is precisely concerned with the behavior of $\Pi^0_2$ sentences. $\endgroup$
    – Henry Towsner
    Commented Nov 24, 2010 at 1:27
  • $\begingroup$ Thanks for the answer and it helps me further, but I am actually looking what happens if you really limit the logic. So, any intermediate result of a theorem must be $\Pi_2$ $\endgroup$
    – Lucas K.
    Commented Nov 27, 2010 at 22:11
  • 1
    $\begingroup$ I believe the theories I mentioned qualify. They don't contain quantifiers, so all statements, including intermediate steps in a proof, are quantifier free. $\endgroup$
    – Henry Towsner
    Commented Nov 27, 2010 at 23:17
2
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ By using cut-elimination, you still have problems with the axiom scheme of induction. I think it is not proven that if the induction hypotheses is of hierarchy higher than $\Pi_2$, but the final theorem is $\Pi_2$, then there is also a prove with only requires $\Pi_2$. That is quite complicated. $\endgroup$
    – Lucas K.
    Commented Nov 27, 2010 at 22:13
  • 1
    $\begingroup$ Gentzen's cut-elimination theorem for Peano Arithmetic applies to theorems with induction on any arithmetic formula, and shows that if there is a proof in PA of a $\Pi_2$ formula then there is a proof which does not use induction on anything more complicated than a $\Delta_1$ formula (in fact, probably less, but I'm not sure of the exact strongest form of the result). $\endgroup$
    – Henry Towsner
    Commented Nov 27, 2010 at 23:22
  • $\begingroup$ That is correct, we can prove even more $\Pi_1$ sentences by having a induction for higher level of arithmetic hierarchy. If you are only interested in a system with $\Pi_2$ formulas, you should not use any assumptions which are not $\Pi_2$ also. $\endgroup$
    – Kaveh
    Commented Nov 29, 2010 at 6:12
  • $\begingroup$ @Lucas K: That is correct, we can prove even more $\Pi_1$ sentences by having a induction for higher level of arithmetic hierarchy. If you are only interested in a system with $\Pi_2$ formulas, you should not use any assumptions which are not $\Pi_2$ also. $\endgroup$
    – Kaveh
    Commented Nov 29, 2010 at 6:13
  • $\begingroup$ PS: Note that Skolemization will turn induction axioms into universal formulas so there is not a problem after Skolmization. $\endgroup$
    – Kaveh
    Commented Nov 29, 2010 at 6:15

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .