Csdrhrt

Is it possible to prove statements in a Hilbert-style calculus in a semi-decidable way (only guaranteed to terminate if a proof exists) by only searching for "linear" or "linked-list"-like proof trees, described below. A "linear" proof tree is one where the a in the premises a, Cab in modus ponens must be an instantiation of an axiom schema.

Let's restrict our attention to zeroth order propositional calculi like classical logic and intuitionistic logic.

Hilbert systems have modus ponens as their only inference rule✱✱:

$$ frac{Cphipsi ;;;;text{and};;;; phi}{psi} $$

This immediately suggests a semi-decidable strategy $mathcal{S}$ for searching for proofs of $psi$ where each step is:

1. Check if $psi$ is an unconditional tautology, succeed if it is.


2. Consider an arbitrarily chosen✱ $phi$ , then check $Cphipsi$ and $phi$ and succeed if both subproblems eventually succeed.

If done as a breadth first search, $mathcal{S}$ is fantastically inefficient, but will find a proof in finite time if one exists.

So then, let's consider another strategy, $mathcal{S}'$ that has one crucial difference.

1. Check if $psi$ is an unconditional tautology, succeed if it is.


2. Consider an arbitrarily chosen✱ unconditional tautology $phi$, then check $Cphipsi$ and succeed if it eventually succeeds.

The crucial difference is that in step 2, we only consider $phi$'s that are, immediately, unconditional tautologies. So the proof tree that we're constructing is constrained to be linear in some sense.

All formulas provable by $mathcal{S}'$ are provable by $mathcal{S}$, but I don't know whether all formulas provable by $mathcal{S}$ are provable by $mathcal{S}'$ .

As a concrete example of a linear proof, I'm stealing the proof of $varphi to varphi$ called id1 on Metamath, reproduced here

CaCaa              axiom-1  (CxCyx)         #1

CaCCaaa            axiom-1  (CxCyx)         #2

CCaCCaaaCCaCaaCaa  axiom-2  (CCxCyzCCxzCyz) #3

CCaCaaCaa          mp #2#3                  #4 

Caa                mp #1#4                  #5

Here it is rewritten in a tree-like way where the left branch of every node always has depth at most 1, and everything that's provable by instantiating an axiom schema is wrapped in brackets .

       Caa

      /   

     /     

[CaCaa]   CCaCaaCaa

         /         

        /           

[CCaCCaaaCCaCaaCaa] [CaCaa]

Does every provable statement have a linear proof in, say, classical or intuitionistic logic? Will $mathcal{S}'$ find it if it exists?

✱ I'm not sure whether the variables in $phi$ should be allowed to range over all possible variables $V$ or if they can be constrained to be $mathop{FV}(psi)$, the variables appearing in the goal $psi$ . I don't know whether you need to be able to use fresh variables in the proof of an arbitrary chosen formula $psi$ or not.

✱✱ I don't know what the correct way to treat substitution of free variables is and I don't know whether a proof that uses substitution can always be rewritten into one that does not.