5
$\begingroup$

Let $\mathcal{L}$ be a recursive first-order theory, with a deductive system $\Xi$ (for instance, Hilbert-Ackerman proof system). Let $\phi$ be a formula and let $l=(\psi_1, \ldots, \psi_n=\phi)$ be a sequence of formulas.

  • Question 1: Suppose we what want to discuss the (asymptotical) computational complexity cost of checking wether $l$ constitutes a proof for the pair $(\mathcal{L}, \Xi)$. What are the relevant numerical parameters, depending on $L$, involved in such a complexity function, and to which complexity class it belongs (P, NP, etc)?

  • Question 2: How much the complexity of verifying $l$ is a proof changes if we change the deductive system (Gentzen's style, for instance), or consider a suitable higer-order theory, or etc?

I apologize in advance about question 2, I hope it makes sense (albeit it is a somewhat non-rigorous question).

The motivation of these questions are the very famous work of Gödel, On the lenght of proofs, and naturally, P=NP? problem.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

Your setup doesn't provide any complexity restrictions on determining whether a formula is an axiom or not, beyond demanding that this is computable. Thus, you won't be able to limit the complexity of proof verification either.

Determining the axioms is going to be the only issue, though. Any reasonable proof system will make verifiying proofs a polynomial-time problem relative to an oracle for the axioms. Typically, quadratic time would do: You read through the proof step by step, check whether the pre-requisites are really there; and if so, if the deduction step matches the rules.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thank you very much. This is great. Since you pointed out, and I neglected, if we consider some canonical axiom system (ZFC, PA, Groups, modules, etc), the axioms can be decided polynomially, right? $\endgroup$
    – jg1896
    Commented Jul 12, 2020 at 17:52
  • 1
    $\begingroup$ Yes, for those examples deciding the axioms is easy. Take for instance ZFC. There are finitely many special axioms, and then the axioms schema replacement and separation. Checking whether a given formula is an instace of the schema is just a pattern-matching issue. $\endgroup$
    – Arno
    Commented Jul 12, 2020 at 18:02

You must log in to answer this question.

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