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.

  • $\begingroup$ 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. $\endgroup$ – derivative Apr 23 '14 at 11:22
  • $\begingroup$ @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! $\endgroup$ – Martin Sleziak Oct 8 '14 at 13:00
  • $\begingroup$ @MartinSleziak I did create it. Thanks, I'll have a look. $\endgroup$ – 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))$


$\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$.

  • $\begingroup$ 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? $\endgroup$ – ZZS14 Apr 23 '14 at 10:59
  • $\begingroup$ The axioms are closed under uniform substitution, so that wouldn't work. Would it? $\endgroup$ – Hunan Rostomyan Apr 23 '14 at 10:59
  • $\begingroup$ @HunanRostomyan I don't know what you're talking about, I've never heard of uniform substitution. $\endgroup$ – Git Gud Apr 23 '14 at 11:00
  • 1
    $\begingroup$ @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}))$. $\endgroup$ – Git Gud Apr 23 '14 at 11:21
  • 1
    $\begingroup$ ((¬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. $\endgroup$ – 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.