# Describing differences between “computational” and “non-computational” proofs

Is there a term that distinguishes proofs that can be performed by a straightforward computation related to the meaning of the proposition from proofs that build a tree of intermediate expressions that terminate in axioms?

Please excuse any misuse of jargon, there's bound to be some.

Consider proving the following statement in propositional calculus.

``````(1)   P ∧ Q ∧ R satisfiable
``````

It can be demonstrated by providing an explicit witness: `P`, `Q`, and `R` are all true (written `PQR` here for brevity). Let's call this proof `A`.

``````(2)   (P → Q) ∧ (Q → R) → (Q → R) tautology
``````

In this setting, the truth of `(2)` can be proven by case analysis by examining each of `ε`, `P`, `Q`, `R`, `PQ`, `PR`, `QR`, `PQR` using truth tables. Let's call this proof `G`

We can also prove the truth of this statement by building it up from intermediate statements. Here, we're using another predicate as scaffolding, `⊢`. `⊢` is a variadic predicate that means "if each expression on the left is true, then the expression on the right is true". This new predicate is just there for convenience, our rules of inference, by design, can only target arguments to the predicate.

Let's call the resulting proof in our refinement logic-inspired system `H`.

``````id  (11)                 R ⊢ R
I→L (12)          Q, Q → R ⊢ R
I→L (13)   P → Q, P, Q → R ⊢ R
I→R (14)      P → Q, Q → R ⊢ P → R
I∧L (15)     P → Q ∧ Q → R ⊢ P → R
I→R (16)                   ⊢ (P → Q ∧ Q → R) → (P → R)
``````

`A`, `G`, and `H` are very different sorts of proof.

The witness `A` is small. It's also directly related to the meaning of `P ∧ Q ∧ R`.

`G` feels like we're just applying an algorithm to an expression in propositional calculus that's known to work regardless of the expression. It feels very different from `A`.

`H`, likewise, feels different from `G`. We are not appealing to the truth table definitions of the logical connectives at all, but instead using a collection of inference rules. Those inference rules must respect the truth table definitions but there's still another step there.

What's the right way to describe these different kinds of proof?