can we a prove ⊢ (α → α) → (α → α)

Question

The system L0 is defined as follows:

Axioms: A1 (α → (β → α))

A2 2. (α → (β → γ) → ((α → β) → (α → γ))

A3 ((¬β → ¬α) → ((¬β → α) → β))

In one of my problem sheets, I am told that I am allowed to use the following theorem: if

⊢ (α → α)

⊢ (α → α) → (α → α)

My attempt to solve/prove the second one ⊢ (α → α) → (α → α) choose 2 axioms which match.

α →α

β→α

γ→α

(α → (α → α) → ((α → α) → (α → α))

I'm struggling to see an obvious way of proving the theorem.

Is it provable? And if so, can you point me in the right direction?

Thanks a lot!

Answer 1

Here is a proof of $\alpha \to \alpha$:

\begin{array}{lll} 1 & (\alpha \to ((\alpha \to \alpha) \to \alpha) \to ((\alpha \to (\alpha \to \alpha)) \to (\alpha \to \alpha)) &A2\\ 2 & \alpha \to ((\alpha \to \alpha) \to \alpha & A1\\ 3 & (\alpha \to (\alpha \to \alpha)) \to (\alpha \to \alpha)& MP \ 1,2\\ 4 & \alpha \to (\alpha \to \alpha) & A1\\ 5 & \alpha \to \alpha & MP \ 3,4\\ \end{array}

To get a proof of $(\alpha \to \alpha) \to (\alpha \to \alpha)$, simply substitute $\alpha \to \alpha$ for $\alpha$ in the previous proof:

\begin{array}{lll} 1 & ((\alpha \to \alpha) \to (((\alpha \to \alpha) \to (\alpha \to \alpha)) \to (\alpha \to \alpha)) \to (((\alpha \to \alpha) \to ((\alpha \to \alpha) \to (\alpha \to \alpha))) \to ((\alpha \to \alpha) \to (\alpha \to \alpha))) &A2\\ 2 & (\alpha \to \alpha) \to (((\alpha \to \alpha) \to (\alpha \to \alpha)) \to (\alpha \to \alpha) & A1\\ 3 & ((\alpha \to \alpha) \to ((\alpha \to \alpha) \to (\alpha \to \alpha))) \to ((\alpha \to \alpha) \to (\alpha \to \alpha))& MP \ 1,2\\ 4 & (\alpha \to \alpha) \to ((\alpha \to \alpha) \to (\alpha \to \alpha)) & A1\\ 5 & (\alpha \to \alpha) \to (\alpha \to \alpha) & MP \ 3,4\\ \end{array}

Notice how you can always do this substitution trick: once you have proving something using some statements variables, you can always substitute any complex statement for those variables. That is, once you have proven that $\vdash \alpha \to \alpha$, then you can immediately conclude that $\vdash (\alpha \to \alpha) \to (\alpha \to \alpha)$ without having to write out an actual derivation.

Answer 2

A logical axiom is a schema (plural: schemata, or schemas) i.e. a "template" that we can use to produce infinitely many formulas all having the same patter.

Thus, all the following formulas are instances of the axiom schema A.1 :

$p \to (q \to p), p \to (p \to p), (p\to q) \to (r \to (p \to q))$, etc.

The same holds for theorems, i.e. logical (schematic) formulas derived from axioms.

Thus $\vdash \alpha \to \alpha$ is again a schema, meaning that every instance of it is derivable in the calculus :

$p \to p, q \to q, (p \to q) \to (p \to q), (p \to p) \to (p \to p)$, etc.

---

The proof of $\vdash \alpha \to \alpha$ is quite simple :

1) $\vdash \alpha \to ((\beta \to \alpha) \to \alpha)$ --- Ax.1

2) $\vdash \alpha \to(\beta \to \alpha)$ --- Ax.1

3) $\vdash (1) \to ((2) \to (\alpha \to \alpha))$ --- Ax.2

4) $\vdash \alpha \to \alpha$ --- from 3), 1) and 2) by Modus Ponens twice.

---

---

For an alternative approach, see the post A Logical Axiom that is Not a Schema.

Answer 3

The other answers show how to prove $P\to P$ and then set $P\equiv(\alpha\to\alpha)$. This works, of course.

But your particular goal can be reached faster with the axioms you have:

• $(\alpha\to(\alpha\to\alpha))$
• $(\alpha\to(\alpha\to\alpha))\to((\alpha\to\alpha)\to(\alpha\to\alpha))$

are instaces of your axioms 1 and 2, respectively.

Now use Modus Ponens once and you're done.