[From "Introduction to Mathmatical logic" by Elliott Mendelson,exercise 1.58]

Axioms of $L_1$:
(A1) $B \rightarrow (C \rightarrow B)$
(A2) $(B \rightarrow (C \rightarrow D)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow D))$
(A3) $(\lnot C \rightarrow \lnot B ) \rightarrow ((\lnot C \rightarrow B) \rightarrow C)$

only rule of inference is $MP$

Axiom system of $L_2$:
(B1) $(\lnot B \rightarrow B) \rightarrow B$
(B2) $B \rightarrow (\lnot B \rightarrow C)$
(B3) $(B \rightarrow C) \rightarrow ((C \rightarrow D) \rightarrow (B \rightarrow D))$

only rule of inference is $MP$

I have to prove that $L_1$ and $L_2$ have the same theorems.For that I have to prove that the axioms of $L_1$ can be proven from axioms of $L_2$ and vice-versa (both systems have the same inferences so I don't have to worry about that).I was able to prove the axioms of $L_2$ from the axioms $L_1$ (in $L_1$) , but failed at proving the axioms of $L_1$ from the axioms of $L_2$ (in $L_2$).

The theorems I was able to derive in $L_2$ so far were:-
(1) $\vdash_{L_2} B \rightarrow B$
(2) $B \rightarrow C, C \rightarrow D \vdash_{L_2} B \rightarrow D$
(3) $B \rightarrow C \vdash_{L_2} ((C \rightarrow D) \rightarrow (B \rightarrow D))$
(4) $\vdash_{L_2}(\lnot B \rightarrow B) \rightarrow (\lnot B \rightarrow C)$
(5) $\vdash_{L_2}B \to (\lnot B \to B)$
(6) $\vdash_{L_2}(B \to C) \to ((\lnot B \to B) \to C)$
(7) $\vdash_{L_2}((\lnot B \to B) \to C) \to (B \to C)$
(8) $\vdash_{L_2}B \to ((B \to D) \to (\lnot B \to D))$
(9) $\vdash_{L_2}\lnot (B \to B) \to (B \to B)$
(10) $\vdash_{L_2} (B\to(\lnot B \to \lnot C)) \to (((\lnot B \to \lnot C) \to (C \to B)) \to (B \to (C \to B)))$
(11) $\vdash_{L_2} ((\lnot B \to \lnot C) \to (C \to B)) \to (B \to (C \to B))$
(12) $\vdash_{L_2} (B\to(\lnot B \to \lnot C)) \to (((\lnot B \to \lnot C) \to D) \to (B \to D)))$
(13) $\vdash_{L_2} ((\lnot B \to \lnot C) \to D) \to (B \to D) $
(14) $\vdash_{L_2} ((\lnot B \to \lnot C) \to C) \to (B \to C) $
But I still am a long way from proving the axioms of $L_2$ from $L_1$ .The problem is that I have ran out of ideas about how I can manipulate the axioms of $L_2$.Can someone give me a hint about this?

Edit:I found another axiom system in another post which I will call $L_3$.

Axioms of $L_3$:
(C1) $B \to (C \to B)$
(C2) $(B \to (C \to D)) \to ((B \to C) \to (B \to D))$
(C3) $(\lnot B \rightarrow B) \rightarrow B$
(C4) $\lnot B \rightarrow (B \rightarrow C)$

idk , maybe I should try to prove (C1) and (C2) from (B3) in $L_2$ as a subgoal/lemma [Not sure if it will help me with my main problem of proving the axioms of $L_1$ from the axioms of $L_2$ (in $L_2$)].

I found a wiki article List of Hilbert systems where, $L_1$ is called "Mendelsons axiom system" and $L_2$ is called "Łukasiewicz First Axiom system".I tried to find a paper,book or article about "Łukasiewicz First Axiom system" instead of the wiki article of Hilbert systems, but the only thing I was able to get that uses "Łukasiewicz First Axiom system" was this MIT OCW lecture slide An example of usage of "Łukasiewicz First Axiom system".There, they derived $\vdash_{L_2} B \to B$ and stopped.I also tried to searching "lukaweicz" to see if someone has a similar question like mine,but the questions I found were actually about "lukaweicz third axiom system", not "lukaweicz first axiom system" an example. I will be glad if someone shows me some other reference that I can read.

  • $\begingroup$ I'd be interested to see your derivations for the theorems--- might give some hints of how to work with MP and axioms of $L_1.$ $\endgroup$
    – coffeemath
    Feb 7, 2021 at 6:36
  • 1
    $\begingroup$ You'd make life easier for us if you didn't use the same labels for different axioms. Systems L1 and L3 are (I think I recall) reasonably easy to prove equivalent, as in both we have the two axioms [A1, A2 of L1] that let us show we can add the rule DT (Dedn Thm). The same is true for L3', got by tweaking the 4th axiom of L3 by swapping $B$ and $\neg B$. Now the axioms of L2 are a subset of the axioms of L3', so it's clear exactly which proposition you need to prove in L2 [$B\to(C\to B)$]. I should add that I always find Mendelson's exercises challenging. $\endgroup$ Feb 8, 2021 at 9:13
  • $\begingroup$ @ancientmathematician ok I edited so that I use different labels for different axioms.Thanks for mentioning. $\endgroup$ Feb 8, 2021 at 9:27
  • 1
    $\begingroup$ You've done it in a very opaque way with all these subscripts! And it really would help if you didn't use different names for the same proposition. $\endgroup$ Feb 8, 2021 at 11:08
  • $\begingroup$ "You've done it in a very opaque way with all these subscripts!",I assume I did a bad job of fixing.sorry for that.Is there another way I can make it more transparent to someone who will answer my question? Also , didn't quite understood what you meant by "And it really would help if you didn't use different names for the same proposition." $\endgroup$ Feb 8, 2021 at 11:15

1 Answer 1


Example from Jan Łukasiewicz, Elements of Mathematical Logic (Pergamon Press, 1963), page 42.

Starting from your axiom (B3) $[(p \to q) \to ((q \to r) \to (p \to r))]$ with substitution: $[p \leftarrow (p \to q), q \leftarrow ((q \to r)\to(p \to r)), r \leftarrow s]$ we get:

$[((p \to q) \to ((q \to r)\to(p \to r))) \to ((((q \to r)\to(p \to r)) \to s) \to ((p \to q) \to s))]$

The antecedent is (B3) again; thus, by Modus Ponens, we get:

(T4) $(((q \to r)\to(p \to r)) \to s) \to ((p \to q) \to s)$.

In the same way (from (T4) and a suitable substitution) we get:

(T5) $[(p \to (q \to r))] \to ((s \to q) \to [p \to(s \to r)]).$

The basic "proof technique" is to identify a suitable substitution in some axiom or already proven thesis such that the result is a "big" conditional where the antecedent is an axiom or an already proven thesis and the consequent is the thesis to be proved.

We can see it in the derivation of $p \to p$ [page 45: your (1)].

From (B3) again, with substitution $[q \leftarrow (\lnot p \to q)]$ we get: $[p \to (\lnot p \to q)] \to [((\lnot p \to q) \to r) \to (p \to r)]$.

The antecedent is axiom (B2) and thus by MP we get (T9): $((\lnot p \to q) \to r) \to (p \to r)$ [that seems quite strange...].

Now, from (T9) with substitution $[q \leftarrow p, r \leftarrow p]$ we get: $((\lnot p \to p) \to p) \to (p \to p)$.

The antecedent is axiom is (B1); using MP we get: (T16) $p \to p$.

Going on, we have [page 45]: (T18) $q \to (p \to q)$ [which is (A1) of L1], and "the very important law of commutation" [page 47]: (T21) $(p \to (q \to r)) \to (q \to (p \to r))$.

Then [page 49]: (T35) $(p \to (q \to r)) \to [(p \to q) \to (p \to r)]$ [which is (A2) of L1].

Thesis 35 occurs as an axiom in the first axiom system of the sentential calculus, given by Frege in his Begriffsschrift.

The main difficulty in Łukasiewicz's original book is the lack of the $\text { Deduction Theorem}$.

Regarding axiom (A3) of L1, we can use "the very important law of double negation" [page 50]:

(T39) $\lnot \lnot p \to p$ and (T40) $p \to \lnot \lnot p$,

as well as "the four laws of transposition" [page 51]:

(T46) $(p \to q) \to (\lnot q \to \lnot p)$, etc.

What we can do now is to use (T46): $(\lnot q \to p) \vdash (\lnot p \to \lnot \lnot q)$ with (T39) and your (2) above to get:

$(\lnot q \to p) \vdash (\lnot p \to q)$.

Using it with $(\lnot q \to \lnot p)$ and (2) again we get:

$(\lnot q \to \lnot p), (\lnot q \to p) \vdash (\lnot q \to q)$.

Finally, using axiom (B1) of L2 and MP we get:

$(\lnot q \to \lnot p), (\lnot q \to p) \vdash q$.

  • 1
    $\begingroup$ Never thought of trying to get bigger theorems from smaller theorems (and "MP-ing" them). Thanks for the hint. $\endgroup$ Feb 10, 2021 at 9:39

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .