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:
R are all true (written
PQR here for brevity). Let's call this proof
(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
PQR using truth tables. Let's call this proof
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
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)
H are very different sorts of proof.
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
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?