How to demystify the axioms of propositional logic?
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)$
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.
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.
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:
- Self-evidence - can a person interpreting each axiom see why they ought to be true?
- Simplicity - related to self-evidence, but simplicity has its own rewards
- 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.
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).