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.


4 Answers 4


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. :)


(a) Giorgio Mossa is right. Two reasons for considering deductive systems for standard truth-functional 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 (not just a trick but actually used in some books for the propositional fragment of quantification theory):

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

And for pure propositional logic 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, which makes it a kosher axiomatic logic -- and one which is trivially sound and complete for theorems of classical propositional logic!

(c) But let's set aside such trivialising examples, 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). Let's concentrate on 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.

(d) Or that 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 (so-called 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. But the details don't matter for now, just the following 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 that arguably avoid some shortcomings of the classical paradigm.

  • $\begingroup$ Your trivial system needs a bit of work to be as strong as standard proposition logic: at the moment $p\vee p \vdash p$ is false, for example. $\endgroup$ Jan 11, 2013 at 9:49
  • $\begingroup$ @ChrisEagle Yes, thanks, I should have explicitly said (and now do say!) it's sound and complete for theorems not consequences. [There's an obvious correlate which is sound and complete for consequence for finite sets of premisses, and we could then add a definition of consequence for infinite sets of premisses which builds in compactness.] $\endgroup$ Jan 11, 2013 at 10:19

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.

  • $\begingroup$ We can prove compactness theorems by going via soundness/completeness results for a finitary proof systems. But should we? :-) Compactness is a purely semantic property and so some will say it "ought"(!?) to be proved, as it can be, by a purely semantic argument ... $\endgroup$ Jan 11, 2013 at 10:27

Truth tables are local to the logical semantics used. For example, if you use a truth table for a two-valued logical semantics, it shows that the well-formed formula is always true with that two-valued semantics.

On the other hand, axiomatic systems are not local to the logical semantics used. If you prove something, you've shown that it doesn't hold only for those semantics, but any semantics where the axioms get satisfied. You've shown that the formula holds for several models. This is comparable to how if you use the axioms of Boolean algebra to prove an equation, you've shown more than if you had just used the 0-1 Boolean algebra, and didn't have the result that the 0-1 Boolean algebra can get used to show equations true for larger algebras.

So, if the motivation for a logic in part consists to address more than one possible semantics, an axiomatic system can be preferable.

Additionally, if you study non-classical logic and have seen some formal proofs (or can tell a formal proof would be simple enough to produce) in classical logic, you can reuse those proofs for the non-classical logic where all of the axioms and rules of inference in the classical logic proof also hold in the nonclassical logic. Thus, if the motivation for studying classical logic in part lies in being in a better position to study nonclassical logic, axiomatic systems can be preferable to truth tables.

For example, if you have take a usual proof of CCpCqrCCpqCpr in classical logic, you might find that it only uses the axioms CpCqp and CCpCqrCCpqCpr. But, that proof implies that CCpCqrCCpqCpr is also a theorem in intuitionist logic, minimal logic, and the pure implicaional calculus.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .