Proving that L1 and L2 have the same theorems.

logicpropositional-calculus

[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.

Best Answer

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

Related Question