Axiomatic Proofs

Question

I have Cut Elimination and the Deduction Theorem as tools as well as three axioms: PL1, PL2 and PL3 (Sider).I also have the following tools.

Weakening: $\phi \vdash (\psi \rightarrow \phi). $
The MP Technique: $\phi \rightarrow (\psi \rightarrow \chi), \phi\rightarrow \psi \vdash \phi \rightarrow \chi.$
Transitivity: $\phi \rightarrow \psi, \psi \rightarrow \chi \vdash \phi \rightarrow \chi$
Contraposition: $\neg\psi \rightarrow \neg\phi\vdash \phi \rightarrow \psi,$ and; $\phi \rightarrow \psi \vdash \neg\psi \rightarrow \neg\phi$
Ex Falso Quodlibet: $\phi, \neg\phi \vdash \psi$
Negated Conditional: $\neg(\phi \rightarrow \psi) \vdash \phi$ and $\neg(\phi \rightarrow \psi) \vdash \psi$
Excluded Middle MP: $\phi \rightarrow \psi, \neg\phi\rightarrow\psi \vdash \psi$

I need to show that $\phi \rightarrow ((\phi \rightarrow \psi) \rightarrow \psi).$

Does anyone have any general strategy tips for going about axiomatic proofs like this? For example, in doing proofs via natural deduction or trees there are strategies to employ (e.g., always apply a rule for an existential claim first, save discharging universal claims for last, etc.).

I'm worried that the only way I con complete these proofs is by brute force which seems like it would take forever.

Answer 1

The Deduction Theorem is all you need!

First, let's show $\phi, \phi \rightarrow \psi \vdash \psi$:

1. $\phi$ Premise

2. $\phi \rightarrow \psi$ Premise

3. $\psi$ MP 1,2

By the Deduction Theorem, this means $\phi \vdash (\phi \rightarrow \psi) \rightarrow \psi$

And applying the Deduction Theorem on that, we get $ \vdash \phi \rightarrow ((\phi \rightarrow \psi) \rightarrow \psi)$

Answer 2

So, by weakening and the MP technique we have that

$\Gamma$ U {$\alpha$} $\vdash$ $\beta$ entails $\Gamma$ $\vdash$ ($\alpha$ $\rightarrow$ $\beta$), which we might call the rule of conditional introduction.

Thus, if we show that {$\phi$, ($\phi$$\rightarrow$$\psi$)} $\vdash$ $\psi$, by conditional introduction we can get to

$\vdash$ (ϕ→((ϕ→ψ)→ψ)).

Hint: Weakening allows you to put ANY formula, including a negated one, on the left side of a $\rightarrow$ formula.

More detail...

From $\phi$ and weakening it follows that ($\alpha$$\rightarrow$$\phi$). By transitivity and ($\phi$$\rightarrow$$\psi$) we have that ($\alpha$$\rightarrow$$\psi$). A similar argument allows us to show that ($\lnot$$\alpha$$\rightarrow$$\psi$) follows. Then, by the so-called excluded middle we have that $\psi$ follows.

Thus, we have {$\phi$, ($\phi$$\rightarrow$$\psi$)} $\vdash$ $\psi$, and by conditional introduction $\vdash$ (ϕ→((ϕ→ψ)→ψ)).

Conditional introduction is not necessarily the same as the rule of inference that follows from The Deduction (Meta) Theorem (depending on the author!). Sometimes The Deduction (Meta) Theorem says that $\Gamma$ U {$\alpha$} $\vdash$ $\beta$ entails $\Gamma$ $\vdash$ ($\alpha$ $\rightarrow$ $\beta$) AND it says that $\Gamma$ $\vdash$ ($\alpha$ $\rightarrow$ $\beta$) entails that $\Gamma$ U {$\alpha$} $\vdash$ $\beta$. Sometimes it just says $\Gamma$ U {$\alpha$} $\vdash$ $\beta$ entails $\Gamma$ $\vdash$ ($\alpha$ $\rightarrow$ $\beta$).

As for general strategies when you have a rule of conditional introduction, keep on making assumptions and look for ways to find contradictions, or to use what you called excluded middle (to me the excluded middle is a disjunction... what you've referred to is not a disjunction). Instead of trying to prove conditionals, break everything down into the rules of inference with the least amount of conditionals, and then use conditional introduction to get the conditionals. Or use the algorithm procedure entailed by the proof of the Deduction Theorem to convert such demonstrations of rules of inference into formal theorems. This kind of gets illustrated by my suggested proof above. I broke ϕ→((ϕ→ψ)→ψ) down into a corresponding rule of inference without so many conditionals: {$\phi$, ($\phi$$\rightarrow$$\psi$)} $\vdash$ $\psi$. So, I wanted $\psi$, so I looked for a formula and it's negation to imply $\psi$. Taking a look at weakening closely enabled me to find such.