0

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?

3

I think it is not correct to use the terms 'computational' and 'non-computational' as you do in the title. The propositional calculus is decidable and proving anything in it can be performed in a computational fashion. All of your examples are therefore computational and could be performed by a theorem prover.

You are right to say there are different kinds of proof going on in your examples. The standard approach to logic involves distinguishing between syntax and semantics. Syntax is concerned with the rules for writing and manipulating symbols. The rules of natural deduction are syntactical. Your third example is of this kind: you are using rules to manipulate the symbols but there is no appeal to what the symbols mean or what truth values they might have. Semantics is concerned with properties such as truth, reference and satisfaction, among others. Truth tables are a technique that involves combining the possible truth values of sentences to see whether arguments are valid or sentences are satisfiable. Your first two examples are of this kind.

The turnstile symbol (⊢) is conventionally used as you do here for the syntactic consequence or proof relation. The double turnstile (⊨) is conventionally used for semantic consequence. The propositional calculus is provably sound and complete, so any argument that is syntactically valid is also semantically valid and vice versa. So anything that you can prove using natural deduction rules can also be proved by truth tables and vice versa. Both can be automated, so neither would be correctly described as non-computational.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.