Formal proof that $\vdash (\varphi \rightarrow \psi) \rightarrow (\neg \varphi \lor \psi)$.

Question

I have to prove the statement

$$\vdash (\varphi \rightarrow \psi) \rightarrow (\neg \varphi \lor \psi)$$ only using first order logical axioms (similar to the ones in the Hilbert System), modus ponens and the Deduction theorem. Does anyone know how to do this using either the Hilbert System or Axioms $L_1 - L_{11}$ from https://people.math.ethz.ch/~halorenz/4students/Literatur/FOLNutshell.pdf on page 30?

I already tried doing it using Counterposition or starting with the axiomatic system $\Phi = \{ (\varphi \rightarrow \psi) \}$ or $\Phi = \{ \varphi, \psi \}$ but none of this worked for me so far.

Edit: This was my closest attempt yet:

Starting with $\Phi = \{ \varphi, \psi \}$ we get:

$$\varphi_0: \varphi \qquad \in \Phi$$ $$\varphi_1: \psi \qquad \in \Phi$$ $$\varphi_2: \psi \rightarrow (\neg \varphi \lor \psi) \qquad \text{(using $L_7$)}$$ $$\varphi_3: \neg \varphi \lor \psi \qquad \text{(using $\varphi_1, \varphi_2$ and modus ponens)}$$

Using the Deduction Theorem twice we now get that $$\vdash \varphi \rightarrow (\psi \rightarrow (\neg \varphi \lor \psi)).$$

It looks close to what we want but honestly I think this approach is completely useless but still the closest I could get to what I wanted to prove.

Thanks for any kind of help!

Answer 1

You are right that what you did isn't really going anywhere. You can understand that by noticing that $\psi \to (\neg \varphi \to \psi)$ is a weaker statement than $(\varphi \to \psi) \to (\varphi \to \psi)$ ... and your $\neg \varphi \to (\psi \to (\neg \varphi \to \psi))$ is weaker yet! So that'll not get you to $(\varphi \to \psi) \to (\varphi \to \psi)$.

Try this as a strategy:

Assume $\varphi \to \psi$

Use axiom $L11$ to get $\varphi \lor \neg \varphi$

Now, in the case of $\varphi$, you get $\psi$ by MP, and from $\psi$ you get $\neg \varphi \lor \psi$ by axiom $L7$

And in the case that $\neg \varphi$ you get $\neg \varphi \lor \psi$ immediately using axiom $L6$.

So using axiom $L8$, you should be able to get $\neg \varphi \lor \psi$

So that's the basic strategy. You'll just have to make it all work by applying the Deduction Theorem strategically.