# Axiomatic Proofs

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.

• You should correct your "Negated conditional" rules, the second one doesn't make sense. As for your question, an answer would be to "start" from the bottom: look at the sentence you want to get, and work up the proof tree to see what you need to do. Another one would be "try to prove it with your natural language, and then translate the steps in your intuitive proof into formal steps" – Maxime Ramzi Oct 13 '17 at 17:14

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)$

• You used a different rule than what he called the 'MP technique'. Note that they didn't say they had conventional modus ponens... {$\phi$, ($\phi$$\rightarrow$$\psi$} $\vdash$ $\psi$. So, strangely (that modus ponens is absent from the rules of inference!), your proof doesn't work in this context. – Doug Spoonwood Oct 13 '17 at 21:48
• I mean... that modus ponens is absent from the a priori assumed rules of inference. It does exist in the system, but it's not up front as usual. – Doug Spoonwood Oct 13 '17 at 22:07
• I should have clarified: MP is in fact the only rule of inference. If I'm not mistaken, the name of the axiomatic system is "H"? – Rusty Oct 14 '17 at 13:16
• I'm confused about this example for another reason, however. I understand that, working backwards from my goal, if I use the DT I get $\phi \rightarrow (\phi \rightarrow\psi)\rightarrow\psi$ but this means from that \phi I need to prove $\phi\rightarrow\psi)\rightarrow \psi$. How to get to the formed from the latter is not clear to me, as the DT only gives me one premise, $\phi$, and doesn't seem to give me $\phi/rightarrow\psi$ as a premise – Rusty Oct 14 '17 at 13:26
• @Rusty Yeah, I couldn't imagine that your system would not have MP! Anyway, DT should work just fine here: DT says that if $\Gamma \cup \phi \vdash \psi$, then $\Gamma \vdash \phi \rightarrow \psi$, where $\Gamma$ is some set of arbitrary statements, and $\phi$ and $\psi$ are some arbitrary single statements. So, since with the first derivation I showed that $\phi, \phi \rightarrow \psi \vdash \psi$, I can use DT by taking $\Gamma = \{ \phi \}$, by taking $\phi = \phi \rightarrow \psi$, and by taking $\psi =\psi$. That is: since in DT $\phi$ is arbitrary, I can fill in anything for $\phi$. – Bram28 Oct 14 '17 at 13:52

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.