Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

How might I go about getting some intuition on the typical axiom schemes given for propositional logic? They seem rather mysterious at first glance.

For example, these are taken from: http://en.wikipedia.org/wiki/Hilbert_system#Logical_axioms

  • $\phi \to \phi$
  • $\phi \to \left( \psi \to \phi \right)$
  • $\left ( \phi \to ( \psi \rightarrow \xi \right)) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$
  • $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$
share|improve this question
It would really help to get an idea of what is causing you problems. Do you understand the simple sentences, just not the harder ones? –  Thomas Andrews Mar 4 '13 at 14:01
@ThomasAndrews -- Not sure I follow. I understand the meaning of the axioms, in the sense that I know what the logical symbols represent. They just seem a bit arcane and mysterious -- for example, I don't have any intuition on why these, and not some other set, are used to axiomatise propositional logic. –  Matt Mar 4 '13 at 14:07
There are many other axiom system we could start out equally.. –  Berci Mar 4 '13 at 14:19
The axiom $\phi \to \phi$ is actually redundant (it can be proven from the others). See us.metamath.org/mpeuni/id.html –  Andrew Salmon Mar 4 '13 at 15:26
@AndrewSalmon Actually, the wikipedia page he links to mentions that redundancy, too. –  Thomas Andrews Mar 4 '13 at 15:30

6 Answers 6

up vote 7 down vote accepted

There are good answers already, but one note:

Another way to understand the choice of the first three axioms you quote is that they are exactly what you need in order to be able to prove the Deduction Theorem by induction on the length of the inner proof.

  • $H\to H$ takes care of a step in the original proof that just applies the hypothesis.

  • $A \to (H \to A)$ allows you to translate a step in the original proof that introduces a logical axiom.

  • $(H \to (P\to Q)) \to ((H \to P) \to (H\to Q))$ is what you need to translate an application of Modus Ponens.

Actually it turns out that $H\to H$ can be derived from the two others (though that is not particularly intuitive), so in many presentations it will be left out.

There are many different ways to complete these three axioms such that you can prove exactly all of the propositional tautologies that can be written using $\neg$ and $\to$. The one you're quoting has the advantage of being reasonably simple and intuitively obvious, while still being sufficient to allow all tautologies to be proved.

Together, the Deduction Theorem and Modus Ponens tell us a lot about how the $\to$ connective works, but it turns out there are propositional tautologies written with $\to$ alone that cannot be proved by these two ingredients. It is quite remarkable that the simple-looking fourth axiom can manage in one breath to tell us everything else there is to know about $\to$, as well as (simultaneously) everything about $\neg$ too. I don't have any good intuitive explanation of how it does that. I can just prove that it does.

share|improve this answer
This seems spot on to me. Note in particular Henning Makholm's excellent final paragraph. –  Peter Smith Mar 4 '13 at 15:43

I assume that you understand why these axioms are tautologies (i.e., true under all truth assignments) and that your question is why these were chosen, from among the infinite number of all tautologies, to serve as axioms. Several factors were involved in this choice (I think --- the choice was actually made long before I was around).

First, there was the fairly arbitrary decision to use $\to$ and $\neg$ as the primitive connectives, so that all other connectives ($\land,\lor, \iff$) are viewed as abbreviations. Had other connectives been chosen as primitive, they would have been involved in the axioms.

Second, having included $\to$ among the primitive notions, one has a very simple and widely used (since ancient times) rule of inference, namely modus ponens: From $\phi\to\psi$ and $\phi$, infer $\psi$. The desire to use this rule may well have motivated the choice of $\to$ as one of the primitive notions; the other, $\neg$, may have been motivated as the simplest thing that, together with $\to$, lets you define all the other connectives.

Third, one wants enough axioms to support, with modus ponens, a completeness theorem. That is, every tautology ought to be provable from the axioms using modus ponens. (More generally, every semantic consequence of any set $S$ of formulas ought to be deducible from $S$ and the axioms using modus ponens.) One way to find such a system of axioms is to begin with no axioms, start trying to write a proof of completeness, and gradually add axioms as you see that they are needed for your completeness proof. With extreme good luck, this might lead you to the axioms in the question. With less luck, it will lead you to a messier set of axioms, which you could then try to "clean up" by removing any redundancies, replacing complicated axioms by simpler axioms that imply the complicated ones, etc. I expect that this is how the axioms were first found. Of course, once they're found, people like me don't go through the work of rediscovering them but merely copy them from textbooks.

share|improve this answer

Which set of axioms we choose for logic is as much an aesthetic choice as it is a mathematical choice. Things that we'd like in logic axioms are:

  1. Self-evidence - can a person interpreting each axiom see why they ought to be true?
  2. Simplicity - related to self-evidence, but simplicity has its own rewards
  3. Independence - We tend to want our axioms not to be too redundant. If Axiom C can be proved from Axiom A and Axiom B, why make C an axiom?

These are aesthetic decisions.

We often have an implicit technical goal. Essentially, when we are designing axioms, we have an idea of what the axioms represent, and we want "enough" of them to get all the sorts of results we want.

We can start with different axiom sets and get the same logic. The definition of when two axiom systems are equivalent can be a little complex, bucause one system might have a different set of symbols than another. (For example, we can do logic without $\to$ and $\land$ and get an equivalent logical system. Often, we keep redundant symbols, because the axioms become less simple and less self-evident without them.)

The most misunderstood element of standard propositional logic is the $\to$ symbol. It is often read as "implies," but that has human meaning that one statement follows from the other in some direct way. In particular, we tend to think of "implies" as having a universal quantifier on it: "($x$ is even) $\to$ ($x+2$ is even)" we read with an implicit "For all $x\dots$" at the beginning. That is not really what $\to$ means, which is one reason some axioms of logic don't use the $\to$ symbol at all, or explicitly define $p\to q$ as a shorthand for $(\lnot p)\lor q$.

So you can see that not only are the axioms chosen based on aesthetics, but the set of symbols we consider fundamental are chosen likewise.

At the most absurd, we can get by with only one logical operation, and axioms on that operation, to get all of propositional logic. For example, if we defined $p*q$ to mean "both $p$ and $q$ are false" then $p*p$ would mean "$p$ is false." $(p*p)*(q*q)$ would mean "$p$ and $q$ are both true." On the other hand $(p*q)*(p*q)$ means "At least one of $p$ and $q$ is true." This violates all of the aesthetics - there is nothing about $*$ that seems intuitively "fundamental," for example, and while $\land$ and $\lor$ have some nice intuitive axioms like associativity, translating those into axioms for $*$ makes them quite ugly. That said, mathematicians are often interested in such reductions because the number of symbols necessary to understand a system is one measure of the complexity of the system.

share|improve this answer

I understand the middle two axioms as "proof combinators" originally introduced by Schonfinkel. You can consider a proof of an implication in some ways as a function that takes a proof of the antecedent to a proof of the consequent.

The first combinator is $\mathsf K : \phi \to \left( \psi \to \phi \right)$, and the way it operates is as follows: Given a proof $p$ of $\phi$ and a proof $q$ of $\psi$ then $(\mathsf Kp)q$ proves $\phi$. In fact $(\mathsf Kp)q = p$.

Similarly we have $\mathsf S : \left ( \phi \to ( \psi \rightarrow \xi \right)) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$ which operates as folows: Given a proof $p$ of $\phi \to (\psi \to \xi)$, a proof $q$ of $\phi \to \psi$ and a proof $r$ of $\phi$ then $((\mathsf Sp)q)r$ proves $\xi$. In fact $((\mathsf Sp)q)r = (pr)(qr)$.

We can prove $\phi \to \phi$ using these two, we are free to instantiate the variables however we like so I pick $\mathsf S : \left ( \phi \to ( [\psi \to \phi] \rightarrow \phi \right)) \to \left( \left( \phi \to [\psi \to \phi] \right) \to \left( \phi \to \phi \right) \right)$ and combine it with $\mathsf K : \phi \to \left( [\psi \to \phi] \to \phi \right)$ and $\mathsf K : \phi \to \left( \psi \to \phi \right)$ to get a proof of $\phi \to \phi$. For short we could call this $\mathsf I = \mathsf {SKK}$.

The $\mathsf K$ combinator gives you the ability to throw away a hypothesis you don't need, the $\mathsf S$ combinator lets you compose proofs together and reuse a proof multiple times. The ability to do these three operations on proofs covers everything you could prove constructively.

It is also interesting to note that if you throw away the types, and just consider the equational theory of the combinators you can implement every computable function out of these two combinators - just like lambda calculus or Turing machines. When you restrict the ability to put combinators together you block their ability to create infinite loops (which would not give meaningful proofs).

The final axiom $\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$ is simply the law of excluded middle: given that $\phi$ implies $\psi$, and $\psi$ is true it must be the case that $\phi$ is true.

share|improve this answer
That is not the law of the excluded middle. That is the law of contraposition: given that $\neg\phi$ implies $\neg\psi$ and $\psi$ is true, it must be tbe case that $\phi$ is true. –  Cameron Buie Mar 4 '13 at 15:12
it is equivalent –  user58512 Mar 4 '13 at 15:14
I wouldn't say that everything provable constructively is provable using $S$ and $K$ alone. In constructive logic one also needs to take $\lor$ and $\land$ as primitive, and accordingly, one needs more axioms. –  Zhen Lin Mar 4 '13 at 15:15
@ZhenLin, yes I'm just referring to simple type propositions. Obviously you need introduction and elimination rules for sums, products, natural numbers etc. to prove things about those, but our language doesn't have those. –  user58512 Mar 4 '13 at 15:18
@user58512: I knew that contraposition followed from excluded middle, but didn't know that the reverse held. Can you give me a reference to look into that? Still, your verbal translation is incorrect. Implication is not a symmetric operator, as your phrasing would indicate. –  Cameron Buie Mar 4 '13 at 15:27

I'd like to offer another view. In the presence of modus ponens, if we have an axiom of the form $\phi_1\to(\ldots(\phi_n\to\psi)\ldots)$, we can convert it into an admissible rule: $\phi_1, \ldots \phi_n \vdash \psi$. (And in the presence of the deduction theorem we can do the reverse.) Let's see what happens when we convert our axioms into such rules:

$\phi \to \phi$

This axiom (although provable from the next two) converts to $$\phi\vdash\phi$$ This represents a fundamental property of any reasonable logic calculus: Any proposition is provable from itself.

$\phi \to ( \psi \to \phi )$

Converts to $$\phi, \psi \vdash \phi$$ This expresses another core structural rule of most logic calculi - the monoticity of entailment, also called the weakening rule. It means that we can freely add additional hypotheses to a proof.

$\left ( \phi \to ( \psi \rightarrow \xi )\right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$

Converts to $$\phi\to(\psi \rightarrow \xi), \phi\to\psi, \phi \vdash \xi$$ This expresses the concept of the most general way of proving an implication with two premisses. If we know $\phi$, a way to prove $\psi$ from $\phi$, then we can discharge both premisses of $\phi\to(\psi \rightarrow \xi)$ to prove $\xi$.

If we specialize this axiom to $$\left ( \phi \to ( \psi \rightarrow \xi )\right) \to \left(\psi \to \left( \phi \to \xi \right) \right)$$ it expresses the exchange structural rule - we can always swap premisses. (We can do this specialization, because the previous axioms tells us that if we have $\psi$ we can always prove $\phi\to\psi$ from it, and then use the original axiom.)

Another possible specialization of this axiom is $$\left (( \psi \rightarrow \xi )\right) \to \left( \left( \phi \to \psi \right) \to \left( \phi \to \xi \right) \right)$$ (Again, we can always prove $\left ( \phi \to ( \psi \rightarrow \xi )\right)$ from $\psi \rightarrow \xi$ using the second axiom.) This expresses the composition of implications.

So this third axiom generalizes (in the presence of the second) both implication composition and exchange of premisses.

$\left ( \lnot \phi \to \lnot \psi \right) \to \left( \psi \to \phi \right)$

To be honest, I don't know any nice interpretation of the rule. It completely expresses the relationship between $\to$ and $\lnot$, in the presence of the other axioms (without this axiom, we get an intuitionistic logic for implication).

share|improve this answer
Thanks, great answer! –  Matt Mar 7 '13 at 11:24
I feel fairly confident you can't "specialize" Self-Distribution or Frege or whatever you want to call it, to the law of commutation. You need simplification also, and then you're not specializing one axiom to another. –  Doug Spoonwood Aug 21 '13 at 4:53

If you put these into words you can read them as follows:

"ϕ→ϕ" "If ϕ, then ϕ".

"ϕ→(ψ→ϕ)" "If ϕ, then if ψ, then ϕ."

"(ϕ→(ψ→ξ))→((ϕ→ψ)→(ϕ→ξ))" "If, if ϕ, then if ψ, then ξ, then if, if ϕ, then ψ, then if ϕ, then ξ."

"(¬ϕ→¬ψ)→(ψ→ϕ)" "If, if not ϕ, then not ψ, then if ψ, then ϕ".

share|improve this answer
Yes, I know how to translate the symbols into words; that's not the question, though. –  Matt Oct 2 '14 at 8:07

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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