What does it mean to prove $(P \to Q \to R) \to (P\to Q) \to P \to R$

Question

I'm reading this PDF in which it proves

$(P \to Q \to R) \to (P\to Q) \to P \to R$

using the Coq proof assistant.

However I'm a bit lost about what does this theorem means in terms of logic. I'm used to proofs of the type

$p\to q \iff p ∧ q$

and by doing a truth table.

However, such assertion makes no sense to me. For example, what does $(P\to Q) \to (Q\to R)$ could mean? IF $P$ is 'is raining' and $Q$ is 'if it rains, then the sky is blue', then what $(P\to Q)$ implying something would mean?

In order to understnd how to prove it in Coq I need to understand how the proof of that would work in math.

UPDATE

Also, why this is an axiom if I can prove it?

Answer 1

First, it helps to add some parentheses. In particular, while a statement like $P \rightarrow Q \rightarrow R$ is typically regarded as ambiguous (is it $P \rightarrow (Q \rightarrow R)$, or is it $(P \rightarrow Q) \rightarrow R$?) the parser in Coq will in such a case always parse it as if the right operation hasd precedence. In other words, it will parse it as $P \rightarrow (Q \rightarrow R)$. Accordingly, the statement you are asking about is:

$$(P \rightarrow (Q \rightarrow R)) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))$$

and that should help you to think about it.

Now, one way to think about this statement is that it represents kind of 'conditionalized Modus Ponens'. That is, this statement effectively states that if $P$ is true, then we have Modus Ponens, for within the context of $P$, we have that if we have $Q \rightarrow R$, then if we also have $Q$, then we have $R$.

This statement is one of the axioms in many axiom systems for propositional logic, and the reason is exactly as stated in the previous paragraph: it allows one to effectively apply Modus Ponens within any number of assumptions. But you really have to study those axiom systems to really appreciate that.

Answer 2

$\def\fitch#1#2{~\begin{array}{|l}#1\\\hline#2\end{array}}$

So if $P$ is true and $P→(Q→R)$ is true, and master implication is true, then everything is true by modus ponens? But how to show $P→(Q→R)$ is true? And how to show that the master implication is true? I'm confused.

No, no, no.   You don't prove $P\to (Q\to R)$.   You prove that if that is given, then $(P\to Q)\to (P\to R)$ will also be true.

What the Coq app is doing is: Assume $P\to(Q\to R)$, $P\to Q$, and $P$; and use modus ponens to derive that $R$ will be true under those hypothesi; so you may use deduction to prove the statement is a theorem of this proof system.

$$\fitch{}{\fitch{1.~P\to (Q\to R)~:\textsf{assumption}}{\fitch{2.~P\to Q\qquad\quad:\textsf{assumption}}{\fitch{3.~P\qquad\qquad\quad:\textsf{assumption}}{4.~Q\to R\qquad~~~:\textsf{modus ponens (1,3)}\\5.~Q\qquad\qquad\quad:\textsf{modus ponens (2,3)}\\6.~R\qquad\qquad\quad:\textsf{modus ponens (4,5)}}\\7.~P\to R\qquad\quad~:\textsf{deduction (3,6)}}\\8.~(P\to Q)\to(P\to R):\textsf{deduction (2,7)}}\\9.~(P\to(Q\to R))\to((P\to Q)\to(P\to R)):\textsf{deduction (1,8)}}$$

Also, why this is an axiom if I can prove it?

It is considered an axiom in some proof systems; not all.   There are many proof systems which use various axioms and rules of inference.   For instance, formal proof systems (such as used above) use very few axioms but several of rules of inference.   The statement is often not taken as an axiom in such a system, but is often a theorem (as for instance, we just proved it so in any formal system that accepts modus ponens and deduction).   However, there are other systems which have few rules of inference (often only modus ponens) but several axioms.   The statement is often taken as an axiom in such axiomatic proof systems.

When you have two proof systems where either one may prove all the axioms and justify all the rules of inference accepted in the other, then they will each be able to prove the same theorems.

---

For example, what does $(P→Q)→(P→R)$ could mean?

• $P$: There is good rain
• $Q$: The plants will grow strong.
• $R$: We will have a good harvest.
  • $P\to(Q\to R)$ If there is good rain, then we will have a good harvest if the plants will grow strong.
    • Which implies $(P\to Q)\to(P\to R)$ If having good rain means the plants will grow strong, then having good rain means we will have a good harvest.