I'm presented with a Hilbert system with just one inference rule (MP) and these axiom schemes:

$$A \supset (B \supset A)$$ $$(A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C))$$ $$A \supset (B \supset A \wedge B)$$ $$A \wedge B \supset A$$ $$A \wedge B \supset B$$ $$(A \supset C) \supset ((B \supset C) \supset (A \vee B \supset C))$$ $$A \supset A \vee B$$ $$B \supset A \vee B$$ $$(A \supset B) \supset ((A \supset \neg B) \supset \neg A)$$ $$\neg \neg A \supset A$$ $$\textbf{F} \supset A$$ $$A \supset \textbf{T}$$

How am I supposed to memorize all of them? In other words, why these particular schemes? I think I've seen examples of every one of them to be necessary for various formal proofs, but I'm curious how the authors have come up with this.

  • $\begingroup$ Practice, practice, practice. You do it enough and you will remember the axioms. Every list of three or more statements is long. Even one statement can be long. Once you've used them enough you just remember. $\endgroup$ – Asaf Karagila Jan 10 '12 at 13:23
  • 1
    $\begingroup$ Also it may help to read them as words rather than formulas, observing that they all state rather obvious (classical) logical truths. You might then even feel something is missing in the list (like a rule that has an $\lor$ at the left of its outer $\supset$). $\endgroup$ – Marc van Leeuwen Jan 10 '12 at 13:48
  • $\begingroup$ @MarcvanLeeuwen, You mean like "F implies A" and "A implies that B implies A and B"? I can also do "Lets state that both A and B. Then it's obviously A". I also realize all of these are true for any interpretation. But then how do I reformulate $(A \supset B) \supset ((A \supset \neg B) \supset \neg A)$? What does it state for? How the authors came up with such a complicated axiom? $\endgroup$ – Egor Tensin Jan 10 '12 at 14:02
  • $\begingroup$ @EgorTensin: If $A$ implies both $B$ and its negation, then $A$ cannot be true. I don't know why these rules prefer $X\subset(Y\supset Z)$ over $(X\land Y)\subset Z$. $\endgroup$ – Marc van Leeuwen Jan 10 '12 at 14:40

A list like this is not unique. What matters is that the collection of axioms is enough to prove the completeness theorem (that any sentence with no model can be proved inconsistent using these axioms and modus ponens).

It would be possible to just take every substitution instance of a tautology as an axiom, in fact, giving an infinite set of axioms. However, for various practical purposes it's nice to have a finite list that suffices. One way to obtain such a list is to take a proof of the completeness theorem and see which axioms are actually used in the proof. Clearly, these axioms will be sufficient.

Because the choice of a finite list is somewhat arbitrary, it's not really worth memorizing, unless you have to do so for an exam. You can always refer to a list when actually using the proof system. On the other hand, if you work with a particular system long enough, you will get a feel for which axioms it contains and how to use them.

Finally, you asked about the meaning of $(A \to B) \to (A \to \lnot B) \to \lnot A$. This axiom makes more sense if you uncurry it to obtain $((A \to B) \land (A \to \lnot B)) \to \lnot A$. In that form it is more clear that this is an axiom for proof by contradiction. If, under the assumption $A$, you can prove both $B$ and $\lnot B$, then this axiom allows you to conclude that $A$ is false. One small advantage of stating it in the way it is stated is to make it more compatible with modus ponens.

  • $\begingroup$ Could you please point out what you mean by "uncurrying" a formula? I'm only a bit familiar with currying functions by means of functional programming. $\endgroup$ – Egor Tensin Jan 10 '12 at 14:26
  • $\begingroup$ I am referring obliquely to the process described at en.wikipedia.org/wiki/Currying . The formula $A \land B \to C$ can be "curried" to obtain $A \to B \to C$. This use of terminology makes more sense in light of the Curry--Howard correspondence, if we think of the formulas as types. $\endgroup$ – Carl Mummert Jan 10 '12 at 14:27
  • $\begingroup$ A beautiful rationalization for items in the list, just exactly what I've been looking for. $\endgroup$ – Egor Tensin Jan 10 '12 at 14:29

To memorize them you might first rewrite all expressions in Polish notation. This means that any expression (x@y) where @ indicates any binary operation becomes @xy. ⊃ becomes a "C", ∧ a "K", ¬ a "N", and ∨ an "A". Then denote all variables as lower case letters of your choosing (so long as each instance of a lower case letter gets replaced uniformly by one other lower case letter. So, (A⊃(B⊃A)) becomes CaCba, but of course we need more than that. Since you now have letters, you can make words out of the formulas, or silly/ridiculous/absurd sentences out of the formulas as a mnemonic. For example, for CaCba you could use the mnemonic "Carrying Automobiles Causes Bad Arthritis." Or you could write CeCae with the mnemonic "Crates Eat Clams And Eels". The more ridiculous, absurd, outrageous, improbable, silly, etc. the words/sentences you come up with, the better. Anything which invokes the senses will also help. Or at least that's my experience and what the books on memory improvement I've read say.

Other than that I'd recommend seeing Carl Mummert's answer.


(A slightly different version of mnemonic than Dough Spoonwood's one):

Encrypt it! (And then draw the resulting image).

Taking the abbreviations as animal names, negation as words 'not'/'never', conjunct as any arbitrary class (say celebrities) and of course, any word that starts with para for paragraph symbol, you can create sentences such as:

Aaarvard jumps on a paraglider containing a bull standing on ant parade.
Paramilitary alligator laughs at parasite bee eating a crow in parallelogram paradise crying with paralyzing paranormal auk sitting on a bat parapet chalking parabola ape beating cattle paranoidly parachuted...


Name them.   These axioms correspond to natural deduction rules of inference (accepting these axioms can justify the rules, or accepting the rules can prove the axioms).   Well, mostly; the second axiom is something of a combination. $$\begin{array}{r:l} A \supset (B \supset A) & \text{reiteration} \\ (A \supset (B \supset C)) \supset ((A \supset B) \supset (A \supset C)) & \text{conditional elimination-and-introduction*} \\ A \supset (B \supset A \wedge B) & \text{conjunction introduction} \\ A \wedge B \supset A &\text{conjunction elimination (1)} \\ A \wedge B \supset B &\text{conjunction elimination (2)} \\ (A \supset C) \supset ((B \supset C) \supset (A \vee B \supset C))&\text{disjunction elimination } \\ A \supset A \vee B &\text{disjunction introduction (2)} \\ B \supset A \vee B &\text{disjunction introduction (1)} \\ (A \supset B) \supset ((A \supset \neg B) \supset \neg A) & \text{negation introduction} \\ \neg \neg A \supset A & \text{double negation elimination (DNE)} \\ \textbf{F} \supset A &{\text{explosion / ex falso quodlibet (EFQ)}\\\text{often written as }B\supset (\neg B\supset A)} \\ A \supset \textbf{T} & \text{struth} \end{array}$$

$$\begin{array}{|l}\text{}\hline \begin{array}{|l} A\supset(B\supset C) \\\hline \begin{array}{|l} A\supset B \\\hline \begin{array}{|l} A \\\hline B\supset C\\ B \\ C\end{array}\\ A\supset C\end{array}\\ (A\supset B)\supset(A\supset C)\end{array}\\(A\supset(B\supset C))\supset ((A\supset B)\supset (A\supset C)) \end{array}$$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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