# Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L.

Find propositional formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ is a theorem of L.

So every axiom is a theorem of L so I thought there would be some way to write $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ in terms of some variables $p_1, p_\ldots$ so that it is one of the axioms;

(A1) $(\phi \rightarrow ( \psi \rightarrow \phi))$

(A2) $((\phi \rightarrow (\psi \rightarrow \chi))\rightarrow((\phi \rightarrow \psi)\rightarrow(\psi \rightarrow \chi)))$

(A3) $(((¬\phi) \rightarrow (¬\psi)) \rightarrow (\psi \rightarrow \phi))$

But I am not sure how to do that or if it is even the correct approach. Thanks

By trying to use A3 I have got $((p_1 \rightarrow (p_2 \rightarrow p_3)) \rightarrow ((p_1 \rightarrow p_2) \rightarrow (p_1 \rightarrow p_3)))$ but I expect that is totally wrong.

• If it is a theorem of $L$ then it must be always true, just make a truth table and see, which conditions $\phi$ must satisfy. – derivative Apr 23 '14 at 11:22
• @GitGud I am not sure whether you created formal-proofs tag, but this is the oldest question I found which has this tag. If you created this tag, could you have a look at a post about this tag on meta? Thanks! – Martin Sleziak Oct 8 '14 at 13:00
• @MartinSleziak I did create it. Thanks, I'll have a look. – Git Gud Oct 8 '14 at 14:45

Axioms are frmulated with schematic letters. In :

(A1) $(A→(B→A))$

$A$ and $B$ are variable in the metalanguage which stay for formulae; we may replace them with formulae whatever and we will get always an instance of the axiom.

Thus, if $\varphi$ and $\psi$ are formulae, as suggested by Git Gud, the following are both instances of (A1) :

$\vdash (\varphi → (\psi → \varphi))$

and

$\vdash (\lnot \psi →(\psi → \lnot \psi))$.

The first one has been obtained with the subst of the formula $\varphi$ in place of the schematic letter $A$ and with $\psi$ in place of $B$.

The second one with the subst of the formula $\lnot \psi$ in place of the schematic letter $A$ and with $\psi$ in place of $B$.

The only care we must take is that substitution must be uniform (as per comment of Hunan Rostomyan) i.e. we must replace each occurences of, let say, $A$ with the same formula.

Looking at the first axiom, it's enough to require that $\phi=\left(\neg \psi\right)$, so let $\phi=(\neg p)$ and $\psi =p$.

• can you just say that? because initially thats what I thought but then I didn't think you could do that. so would the answer be; $(p_1 \rightarrow ((¬p_1) \rightarrow p_1))$ ? Or am I understanding it wrong? – ZZS14 Apr 23 '14 at 10:59
• The axioms are closed under uniform substitution, so that wouldn't work. Would it? – Hunan Rostomyan Apr 23 '14 at 10:59
• @HunanRostomyan I don't know what you're talking about, I've never heard of uniform substitution. – Git Gud Apr 23 '14 at 11:00
• @HunanRostomyan You are correct, I just don't see how it contradicts anything of what I've said. We want to find formulas $\phi$ and $\psi$ such that $(\phi \rightarrow (\psi \rightarrow (¬\psi)))$ holds. Axiom 1 with $\phi=\neg p$ and $\psi = p$ yields $(\underbrace{(\neg p)}_{\phi}\to (\underbrace{p}_{\psi}\to \underbrace{(\neg p)}_{\phi =\neg \psi}))$. – Git Gud Apr 23 '14 at 11:21
• ((¬p) →(p → (¬p))) is a substitution instance of (ϕ→(ψ→ϕ)) (or one can obtain ((¬p) →(p → (¬p))) from (ϕ→(ψ→ϕ)) by substitution). Since (uniform) substitution consists of a truth-preserving transformation, and (ϕ→(ψ→ϕ)) is an axiom it follows by the soundness meta-theorem that ((¬p) →(p → (¬p))) is a tautology. – Doug Spoonwood Apr 23 '14 at 21:57

Interesting question and I think there are three options:

• $\phi \equiv (\psi \rightarrow (¬\psi)$ (for example if $\phi$ is $\psi \rightarrow \lnot \psi)$ but simple equality is enough.

• $\lnot \phi$ is a theorem , then you get impossible antecedent.

• $\psi \rightarrow \lnot\psi$ is a theorem, what will be the case if $\lnot\psi$ is a theorem , then you get true concequent.

Each of these three off course stands for an infinite number of formulas so have a pick.

What is "(ϕ→(ψ→(¬ψ)))"? It is a conditional.

What do we know about all conditionals? They have an antecedent and a consequent.

What is the antecedent of (ϕ→(ψ→(¬ψ))), and what is it's consequent? The antecedent is ϕ and the consequent is (ψ→(¬ψ).

So, how might we make (ϕ→(ψ→(¬ψ))) into a theorem? Well, all tautologies are theorems by the completeness theorem. So, how might we make (ϕ→(ψ→(¬ψ))) into a tautology?

Well, let's suppose we substituted ϕ with (ψ→(¬ψ)). We would then have the well-formed formula [(ψ→(¬ψ))→(ψ→(¬ψ))]. Thus we might substitute ϕ with (p→(¬p)) and ψ with p to obtain a formula which is a theorem of L.