Propositional Logic

Leary does not waste much time on the propositional portion of logic. He offers us a single definition to provide propositional rules of inference. However, this single definition in effect gives us an infinite number of propositional rules!

Here is the definition; then a few comments.

Definition: If $\Gamma$ is a finite set of -formulas, $\phi$ is an -formula, and $\phi$ is a propositional consequence of $\Gamma$, then $\langle \Gamma, \phi \rangle$ is a rule of inference of type (PC).

Here is the idea. $\phi$ is a propositional consequence of $\Gamma$ just in case it is what B&E call a ``tautological consequence" of $\Gamma$, that is, if there is no row of a joint truth table in which every sentence in $\Gamma$ is T and $\phi$ is F. (Notice that Leary's procedure on p. 59 for converting a formula $\beta$ of first-order logic into a formula $\beta_P$ of propositional logic amounts to the same thing as B&E's procedure for identifying the truth-functional form of a quantifier sentence on p. 261 of Language, Proof, and Logic.) So the above definition gives us infinitely many propositional rules of inference. These include most of B&E's rules, although as noted above it will not give us $\to$Intro or $\vee$Elim. But there will be more than enough other rules to make up for this lack!

And of course the rules we get in this way will be massively redundant. For instance, we will have the rules $\langle \{ \neg \phi\}, \phi \to \psi \rangle$ and $\langle \{\psi\}, \phi \to \psi \rangle$ and $\langle \{ \neg (\phi \wedge \neg \psi), \phi \to \psi \rangle$, as well as $\langle \{\neg \phi \vee \psi \}, \phi \to \psi \rangle$.

There is another thing that makes me uncomfortable with this way of handling propositional logic. We are working up to proving some interesting connections between the semantic relation expressed by `$\models$' and the proof-theoretic relation expressed by `$\vdash$'. In order for this to be interesting, we need to define each of these relations independently of the other. But truth tables are a semantic device, so defining propositional rules of inference in terms of truth tables makes proving soundness and completeness for the propositional part of logic basically trivial.

On the other hand, soundness and completeness results for propositional logic are fairly straightforward in any case; predicate logic is where the action's at. So although I think there is a theoretical cost to be paid for treating propositional logic in this way, perhaps it is a fairly minor price.