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.
 A: Looking at the first axiom, it's enough to require that $\phi=\left(\neg \psi\right)$, so let $\phi=(\neg p)$ and $\psi =p$.
A: 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.
A: 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.
A: 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.
