I'm taking course in logic. The book is available here

I don't understand why is Mendelson axiom schemas are the way they are.

For example implication creation schema

  • $φ ⇒ (ψ ⇒ φ)$

My thoughts when I see this is: "Why is ψ over there? How it got here?".

I mean, let say that $φ$ is the sentence "I love apples". Using this schema can I infer implication that "I love apples implies that if all lions are cats, then I love apples". It absolutely doesn't make sense to me.

Implication distribution is even more confusing.

  • $(φ ⇒ (ψ ⇒ χ)) ⇒ ((φ ⇒ ψ) ⇒ (φ ⇒ χ))$

Let's say that

$φ - \text{The cable is under high voltage}$

$ψ - \text{Person touches the cable}$

$χ - \text{Person will die}$

Applying this rule we get:

"If the cable is under high voltage implies that person touches the cable, then the cable is under high voltage implies that the person will die".

Which is also doesn't make any sense to me.

So does contradiction realization.

Can someone explain it to me or point me to the reading that does?

  • 5
    $\begingroup$ Step one for better understanding formal logic. Don't use real life analogies. You will be confused by the "natural language common sense" that you obtained through years of living. $\endgroup$
    – Asaf Karagila
    May 20, 2015 at 7:52
  • 2
    $\begingroup$ Regarding $φ ⇒ (ψ ⇒ φ)$, we can try with this : "if we are licensed to assert $φ$, we are also licensed to assert that $φ$ follows from an "additional" hypotheses $ψ$". $\endgroup$ May 20, 2015 at 8:56

4 Answers 4


"I love apples implies that if all lions are cats, then I love apples".

But this makes perfect sense! Suppose I am a person who loves apples. Suppose some further stuff also holds; suppose all lions are cats, I have brown hair, my favourite colour is rainbow, etc. Well, then its still the case that I love apples!

Hence, the schema $\varphi \rightarrow (\psi \rightarrow \varphi)$ basically says that if a statement $\varphi$ is true, then its still true given further hypotheses (which are denoted $\psi$).

Does that help?


Both of the rules $$\phi \to \psi \to \phi$$ and $$(\phi \to \psi \to \chi) \to (\phi \to \chi) \to (\phi \to \chi)$$ can also be validated by a different understanding of implication, related to what is known as the Curry-Howard isomorphism. Unlike the idea of making up other examples, this way lets you view the implications as something concrete in a way that is backed up by a theorem that I will quote below.

For this viewpoint, pretend that each variable represents some "type" of object, and pretend that $A \to B$ means "I have a procedure to make an object of type $B$ when given an object of type $A$". A direct statement of a variable, e.g. just "$A$", means "I have a way to produce objects of type $A$ directly".

So, for example $\phi \to \psi \to \phi$ says: If I have a way to produce objects of type $\phi$ directly, then I have a way to produce objects of type $\phi$ when given objects of type $\psi$. Namely, I just throw away the object of type $\psi$ and produce an object of type $\phi$ directly! This validates the rule.

Similarly, $$(\phi \to \psi \to \chi) \to (\phi \to \psi) \to (\phi \to \chi)$$ says:

Suppose that , when I am given an object of type $\phi$, then I have a way to produce an object of type $\chi$ when given an object of type $\psi$. Then, if I have a way to produce an object of type $\psi$ when given an object of type $\phi$, I must also have a way to produce an object of type $\chi$ when given an object of type $\phi$.

The verification is not hard: essentially, I use my object of type $\phi$ and the assumption $\phi \to \psi$ to produce an object of type $\psi$, then I use the assumption $\phi \to \psi \to \chi$ to make an object of type $\chi$.

Here is the correctness result I mentioned:

Theorem: An implication statement in propositional logic can be verified by this method if and only if it is provable in intuitionistic propositional logic.

If I recall correctly, you will find that all but one of Mendelson's axiom schemes are verifiable by this method; the one remaining one expresses double negation elimination in some way. (Unfortunately, I don't have the book, and the full list of schemes is not in the question. But this method does verify the two schemes that are listed.)

  • $\begingroup$ Add parenthesis! $\rightarrow$ is not associative. $\endgroup$ Jan 22, 2016 at 21:50
  • $\begingroup$ @YoTengoUnLCD: there is a standard convention in type theory and proof theory that $a \to b \to c$ means $a \to (b \to c)$; in other words $a \times b \to c$ corresponds to $a \to b \to c$ by Currying. The parentheses I used are exactly the ones that are needed under this convention. $\endgroup$ Jan 22, 2016 at 23:04

I agree with @Asaf Karagila. Most of the time real life analogies are confusing for understanding logic.

The implication does not correspond to the "real life" implication $\phi \Rightarrow \psi$ does not mean that $\psi$ is a consequence of $\phi$ it only states that whenever $\phi$ is true $\psi$ is also true.

The good way to understand an implication is to wonder what happen if the left part is true. For your first cases $\phi\Rightarrow (\psi\Rightarrow \phi)$ if $\phi$ is false then the implication is true; if $\phi$ is true then the implication $\psi \Rightarrow phi$ is true hence $\phi\Rightarrow (\psi\Rightarrow \phi)$ is always true.

The same reasoning will get you through the implication distribution.

  • $\begingroup$ Better to say that $\varphi \implies \psi$ does not mean that "$\varphi$ causes $\psi$" or some such. $\endgroup$ May 20, 2015 at 8:46

What you are thinking of is "from A I can deduce B". For instance, from Euclid's axioms I can deduce thar the sum of the internal angles of a triangle is a flat angle, but I can't deduce that multiples of 4 are also multiples of 2, because there's no relation between those results.

Implication is actually different: "it's not the case that A is true and B is false."

The first "if then" belongs to the realm of proofs;

The second to the realm of logical connectives, not unlike "and", "or".
Connectives just create new statements from others, and their truth depends from the truth of their parts.
Some statements are tautologies: true regardless of the truth value of its parts.
"A or not A" is the simplest; the axioms you give are other examples, as you can verify by doing truth tables.

  • $\begingroup$ Thanks, O guess I just need to check the truth tables. $\endgroup$ May 21, 2015 at 6:25
  • $\begingroup$ yes. you can still find some meaning in those statements, as other answers show, but the main reason they are true is because they are true, if i am allowed to speak tautologically about tautologies (and truth tables are the quickest way to verify their truth) $\endgroup$
    – byserpas
    May 21, 2015 at 8:25

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.