$(p\rightarrow q)\vee (q\rightarrow r)$ imply peirce's law in intuitionistic logic?

Question

Consider the system of intuitionistic implicational logic together with the axiom schema adding all instances of

$$(p\rightarrow q)\vee(q\rightarrow r)$$

Does that make Peirce's law true?

I have already show that Peirce's law implies the above schema. Thank you for any hint of the other direction.

Answer 1

Yes, this will imply Peirce's Law. One way to see this is to notice that $(p \to q) \lor (q \to r)$ is equivalent to the law of excluded middle which itself is maybe better known to imply Peirce's Law. For completeness, here is a direct proof using this idea:

We need to show $((a \to b) \to a) \to a$. By the assumption $(p \to q) \lor (q \to r)$ we know that $(\top \to a) \lor (a \to \bot)$, so we get two cases:

• If $\top \to a$ this means we have $a$ and therefore we can easily show $((a \to b) \to a) \to a$. (Since we can show $c \to a$ for any $c$)

• If $a \to \bot $ i.e. $\neg \, a$ we first note that we can show $(a \to b)$, since if we have $a$ it combines with $\neg \, a$ to give us $\bot$ and so we get $b$ by explosion. Now it is clear that we also get $((a \to b) \to a) \to a$, since if we assume $H : (a \to b) \to a$ we can get $a$, because we already have $(a \to b)$.

Answer 2

• Accept $(p\to q)\lor(q\to r)$ as an axiom schema.
• • Take arbitrary terms $\alpha$ and $\beta$.
• • Derive $(((\alpha\to\beta)\to\alpha)\to\alpha)\lor(\alpha\to\beta)$ from the schema.
• • • Raise $(\alpha\to\beta)\to\alpha$ as an assumption.
• • • • Derive $\alpha$ under the case $((\alpha\to\beta)\to\alpha)\to\alpha$ by modus ponens.
• • • • Derive $\alpha$ under the case $(\alpha \to\beta)$ by modus ponens.
• • • Thus deriving $\alpha$ by a proof by cases (ie disjunction elimination).
• • Deduce $((\alpha\to\beta)\to\alpha)\to\alpha$
• Therefore $((p\to q)\to p)\to p$ is also a schema under the given axiom schema.

Answer 3

The document was closed very long time ago, I just leave the main text here.

$ (p\to q)\to p,\\ \ \ \ \ by\ Hypothesis\\ \ \ \ \ ((p\to p)\to p)\lor (p\to q)\\ \ \ \ \ (i)(p\to p)\to p,\\ \ \ \ \ \ \ \ \ p\to p\\ \ \ \ \ \ \ \ \ \therefore p\\ \ \ \ \ (ii)p\to q,\\ \ \ \ \ \ \ \ \ \therefore p\\ \ \ \ \ \therefore p\\ ((p\to q)\to p)\to p $