The axioms of L are:

$\mathrm {(A1)} \quad \mathscr{\left(B\to\left(C\to B\right)\right)} \\ \mathrm {(A2)} \quad \mathscr{\left(\left(B\to\left(C\to D\right)\right)\to \left(\left(B \to C \right)\to \left(B \to D \right)\right)\right) }\\ \mathrm{(A3)}\;\;\; \mathscr{\left(\left(\left(\neg C \right)\to \left(\neg B \right)\right) \;\;\to \;\left(\left(\left(\neg C \right)\to B \right)\to C \right)\right)}$

What I understand is that $\mathscr{(B \to D) = \,\left((\neg B\to B)\to B\,\right)}$ must be equal, so $\mathscr{B}$ becomes $((\neg \mathscr{B})) \to \mathscr{B})$, and $\mathscr{D}$ becomes $\mathscr{B}$

Please write the proof in details

So, I write what I know:

$$\mathscr{\left\{\left((\neg B) \to B \right)\to(C\to B)\right\}\to \left\{(((\neg B) \to B \right)\to C)\to \left(((\neg B) \to B \right)\to B)\}} \;(A2)$$

I cannot go further .

  • $\begingroup$ It's actually not possible. L has a meta-theorem that all theorems in the system begin with '(' and end with ')'. By inspection, though what you've referenced begins with '(', it does not end with ')' and thus is not provable. $\endgroup$ – Doug Spoonwood Apr 7 '18 at 2:46
  • $\begingroup$ Also, with respect to the law of Clavius, it might get pointed out that theorems of the form (($\lnot$B$\rightarrow$B) exist. However, B is always an implication or a negation when this happens. $\endgroup$ – Doug Spoonwood Apr 7 '18 at 3:01

For what I suspect would be the intended theorem, I don't know why you've started with a form of axiom 2. And I don't know why you seem to have concluded that any proof will begin with that axiom, or even have that axiom as you've used it. Let's substitute B for C in axiom (3), and please excuse me using plainer letters.


The consequent is ((($\lnot$B)$\rightarrow$B)$\rightarrow$B), which I suspect you seek to prove. The antecedent is (($\lnot$B)$\rightarrow$($\lnot$B)).

Now can you construct a proof?


I could be misunderstanding the context of your question, but it should not be the case that the two formulae $B\rightarrow D$ and $(\neg B \rightarrow B)\rightarrow B$ are equivalent, as the first is false when $B$ is true and $D$ is false, and the second is a tautology.

That being said, why does this not just follow from the truth table? You are trying to prove that something is a tautology, and there is only one atom to tabulate over.

  • $\begingroup$ Firstly, what I meant is that you must replace $\mathscr { B\; by\; ((\neg B) \; \to B\;), and\;\; D\; by B\; \;}$. I know it is a tautology, however The idea is to prove it using these axioms. This is what the question asks me to do. $\endgroup$ – Ali Mar 29 '18 at 20:17
  • $\begingroup$ A proof is a sequence of well-formed formulas which follows certain rule(s) and axiom(s) in this context. Truth tables don't involve such sequences nor appeal to such rule(s) and axiom(s). $\endgroup$ – Doug Spoonwood Apr 7 '18 at 2:41

Please allow me to use some more readable symbols.

First, let's show that $\vdash_L \varphi \rightarrow \varphi$ (ID):

$1. \varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi) \quad (A1)$

$2. (\varphi \rightarrow ((\varphi \rightarrow \varphi) \rightarrow \varphi)) \rightarrow ((\varphi \rightarrow (\varphi \rightarrow \varphi)) \rightarrow (\varphi \rightarrow \varphi)) \quad (A2)$

$3. (\varphi \rightarrow (\varphi \rightarrow \varphi)) \rightarrow (\varphi \rightarrow \varphi) \quad MP \ 1,2$

$4. \varphi \rightarrow (\varphi \rightarrow \varphi)\quad (A1)$

$5. \varphi \rightarrow \varphi \quad MP \ 3,4$

Now you can prove $\neg \varphi \rightarrow \varphi \vdash_L \varphi$:

$1. \neg \varphi \rightarrow \varphi \quad Premise$

$2. \neg \varphi \rightarrow \neg \varphi \quad ID$

$3. (\neg \varphi \rightarrow \neg \varphi) \rightarrow ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \quad (A3)$

$4. (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \quad MP 2,3$

$5. \varphi \quad MP 1,4$

By the Deduction Theorem, we therefore have $\vdash_L (\neg \varphi \rightarrow \varphi) \rightarrow \varphi $

  • $\begingroup$ Can you prove it without using the deduction theorem, and without any premises (hypothesis). In other words, Can you prove it using only the axioms. $\endgroup$ – Ali Mar 31 '18 at 11:46

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.