Why is axiomatic system needed in propositional logic?

Question

I am trying to learn propositional logic. I have read that axiomatic system is defined since there are some problems which can not be solved using truth tables. I have found such a problem in predicate logic when we use quantifiers. There we should use axioms to derive a formula which contains quantifier, since we can't construct truth table of that formula. But I am interested why we need axiomatic system in propositional logic? We can check if a formula is tautology using its truth table.

Answer 1

As you said we can check if a formula is a tautology just looking at it's truth table, anyway studying logical system (i.e. a system with has axioms and inference rules) also for propositional logic can be interesting for different reason:

• first of all there's the didactic reason: it's a simple deductive system, indeed it can be seen as just a fragment of the system for first order logic, so it helps to familiarize with deductive systems;

• a second reason it's complexity: sometimes proving the logic validity of a formula through such deductive system can be easier then proving it via truth tables, which involve calculate the truth values of a formula for all possible valuation of the variables which can become easy a troublesome for formula with huge number of variables, while in many cases writing a proof can be much easier involving just few application of inference rules.

Probably there other reasons too that I'm not remembering right now, but I reserve to myself the right to add them later. :)

Answer 2

(a) @ineff is right. Two reasons for considering deductive systems for propositional logic are

1. they can be used as toy examples, as warm-up exercises to the more serious business of considering proof-systems for quantificational, modal, and other logics,
2. they can (in some cases) deliver proofs-of-classical-validity more efficiently than hacking through a truth-table.

(b) But of course, it all depends which deductive system you look at. The OP mentions axiomatic systems. Well, here's one perfectly good axiomatic system for propositional logic (used in some books, indeed, for the propositional fragment of quantification theory):

For any truth-functional tautology $\varphi$, $\varphi$ is an axiom.

And you don't need any additional rule of inference, so all proofs in the axiomatic system are one line! That's just fine, since it is recursively decidable what's an axiom, so this is a kosher axiomatic logic which is trivially sound and complete for theorems of classical propositional logic!

(c) Let's set aside such trivialising examples, then, though they remind us that different deductive systems will have different virtues! And indeed now set aside axiomatic systems in the sense of Frege-Hilbert systems more generally (they usually don't have virtue (2) anyway). Think about Natural Deduction proof-systems of one style or another. Now there is an additional reason for being interested in these:

3 Arguably, the ND introduction and elimination rules for connectives fix their sense.

Arguably, what we grasp in pre-formally understanding logical operators is their inferential role, is how we can use them in argument (in a Wittgensteinian slogan, to ask for the meaning [of logical operators] is use for their [inferential] use). Then, in the propositional logic case, a Natural Deduction system can be thought of aiming to directly encapsulate the meaning of the connectives by laying down the inferential rules governing their use, which determine their meaning.

On this sort of view, which we owe to Gentzen, there's a kind of priority to the deduction rules in an ND system -- and it will be a non-trivial discovery that the resulting system is sound and complete with respect to a Boolean truth-functional interpretation.

Or it will be a discovery if, indeed, we accept the "classical" ND rules. But of course there are issues about that. From Gentzen's perspective, there is arguably something anomalous about the classical negation rules (failures in "harmony"). And we can worry too about the classical structural rules that allow unrestricted chaining of proofs in a way that gives us fallacies(?) of irrelevance. The details don't matter for now, just the general point

4 In considering ND systems for classical propositional logic, we can also -- in a smooth and natural way -- investigate neighbouring non-classical logics.

Answer 3

Another important use of deductive systems is in proving compactness results. As soon as you have a complete sound deductive system in which proofs are finite, you have a compactness theorem: if a formula $\phi$ follows from some infinite set of premises, then in fact it follows from some finite subset.

Compactness of propositional logic is a much weaker tool than compactness of predicate logic, but it serves as a toy example, and isn't entirely useless in its one right: it is still strong enough, for example, to express many of the compactness arguments used in combinatorics, in which one deduces an infinitary result from its finitary equivalents. For instance, the four-colour theorem for infinite planar graphs can be proved from the finite case in this way.

Of course, with this perspective, you don't really care what proof system you're using, as long as it's complete. This is one reason why unwieldy Hilbert-style systems are used: it's a frustrating amount of work to actually prove any worthwhile result within them, but it's comparatively easy to prove metalogical results like completeness.