Derive by modus ponens $[A\rightarrow(B\rightarrow C)]\rightarrow[(A\rightarrow B)\rightarrow(A\rightarrow C)]$

Question

How could I derive by modus ponens the formula $$[A\rightarrow(B\rightarrow C)]\rightarrow[(A\rightarrow B)\rightarrow(A\rightarrow C)]$$ from, and just from, the following axiom schemata?

1. $(A\lor A)\rightarrow A$.
2. $A\rightarrow(A\lor B)$.
3. $(A\lor B)\rightarrow(B\lor A)$.
4. $(A\rightarrow B)\rightarrow[(A\lor C)\rightarrow(B\lor C)]$.
5. If $A\rightarrow B$ and $B\rightarrow C$, then $A\rightarrow C$.
6. $A\rightarrow A$.
7. $A\leftrightarrow \neg(\neg A)$.
8. $(A\rightarrow B)\leftrightarrow(\neg B\rightarrow \neg A)$.
9. $(A\land B)\rightarrow A$ and $(A\land B)\rightarrow B$.

Answer 1

In an axiomatic system you cannot derive it at all (you need to add it as an axiom) , but if you have a natural deduction system you can derive it from nothing at all (ex nihilo)

1) It is easely proved in a natural deduction system:

1 | |______ P -> (Q -> R))                             Assumption
2 | | |____ P -> Q                                     Assumption
3 | | | |__ P                                          Assumption 
4 | | | |   Q                                          2,3 Modus ponens
5 | | | |   Q -> R                                     1,3 Modus ponens
6 | | | |   R                                          4,5 Modus ponens
. | | | <------------------------------------------------ end subproof 
7 | | |     P -> R                                     3-6 Conditional proof
. | | <-------------------------------------------------- end subproof 
8 | |      (P -> Q) -> (P  -> R)                       2-7 Conditional proof
. | | <-------------------------------------------------- end subproof 
9 | |      (P -> (Q -> R)) -> ((P -> Q) -> (P  -> R))  1-8 Conditional proof
================================
  QED

But still in an axiomatic proof it is not provable.

A bit metalogic:

If an axiomsystem is consistent (truth preserving) then you cannot proof in any way an untrue sentence.

If there is an interpretation of a system (any interpretation at all) where in all models (valuations) all axioms are always true, then all theorems are also always true.

if in an interpretation where in all models(valuations) the axioms are true but there is a model (valuation) where a formula is false then that formula is not a theorem.

Now $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ fails in Lukasiewisc 3 valued logic while all other axioms are theorems of Lukasiewisc 3 valued logic.

So the axioms are true in all valuations , but $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ is not true in some particular valuation , therefore $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ cannot be a theorem of the system.

The proof

Lukasiewicz 3 valued logic consists of the following truthtables:

       ||     ||  A ->  B || A & B || A v B || 
       || Des ||  1 2 3   || 1 2 3 || 1 2 3 || ~A  
 ----- ||-----||----------||-------||-------||--- 
 A = 1 ||  *  ||  1 2 3   || 1 2 3 || 1 1 1 || 3   
 A = 2 ||     ||  1 1 2   || 2 2 3 || 1 2 2 || 2 
 A = 3 ||     ||  1 1 1   || 3 3 3 || 1 2 3 || 1 

A formula is a tautology or theorem in this logic if and only iff in every possible valuation the formula evaluates to 1 (the true or designated value)

All given axioms do this. (check this yourself)

But $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ where $ P = Q = 2$ and $ R = 3 $ fails, it evaluates to 2

(P -> (Q -> R)) -> ((P -> Q) -> (P  -> R) )
(2 -> (2 -> 3)) -> ((2 -> 2) -> (2  -> 3) )
(2 -> (  2   )) -> ((  1   ) -> (   2   ) )
(  1          ) -> (         2            )
(               2                         )

therefore $ (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) $ is not a theorem of this logic , and therefore it can also not be a theorem of the syatem cannot be a theorem of the system.

QED

missing steps in this proof that you will think about yourself

• are the axioms always true. just a lot of work , instead of a 8 line truthtable you get a 27 line truthtable

• is the system truthpreserving? this proof is based on a system that uses modus ponens ($ \vdash A, \vdash A \to B $ then $ \vdash B $ ) as inference rule, the system doesn't have this rule it has the hypothetical syllogism inference rule ($ \vdash A \to B , \vdash B \to C $ then $ \vdash A \to C $ ) to me it looks that the hypothectical syllogism inference rule is equivalent or a bit weaker than the modus ponens inference rule, but this is in need of a proof is $ A \to (( A \to B ) \to B) $ provable a theorem in the system

• what is the differece between an interpretation and a model? (an interpretation is a logic or logical system itself, a model is a particular valuation)

• but these are things the op may think about

two posters that disagree with me, while i can proof they are wrong.

Answer 2

In my answer below, we can find a "modern" reconstruction of PM's system of propositional logic.

Here we have, with the help of Wiki Principia Mathematica propositional logic , the original proof of PM's

*2.77 --- $(p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$.

---

We establish first some useful theorems :

*(2.05) --- $\vdash (q \rightarrow r) \rightarrow [(p \rightarrow q) \rightarrow (p \rightarrow r)]$ --- from Sum with the substitution : $\lnot p/p$.

*(2.06) --- $\vdash (p \rightarrow q) \rightarrow [(q \rightarrow r) \rightarrow (p \rightarrow r)]$ --- from Comm with the substitution : $q \rightarrow p/p; p \rightarrow q/q; p \rightarrow r/r$ and (*2.05) by modus ponens

We call the above theorems : Syll

*(2.36) --- $\vdash (q \rightarrow r) \rightarrow [(p \lor q) \rightarrow (r \lor p)]$ - from Syll with the subst $p \lor q/p; p \lor r/q; r \lor p/r$ and Perm by mp, followed by Sum and Syll

*(2.37) --- $\vdash (q \rightarrow r) \rightarrow [(q \lor p) \rightarrow (p \lor r)]$ - from Sum, Perm and Syll

*(2.38) --- $\vdash (q \rightarrow r) \rightarrow [(q \lor r) \rightarrow (r \lor p)]$ - from Sum, Perm and Syll

---

Now we write the derivation of (*2.77) :

*2.53 --- $\vdash (p \lor q) \rightarrow (\lnot p \rightarrow q)$.

From (*2.12) [i.e. $\vdash p \rightarrow \lnot \lnot p$] and Syll (*2.38), with the substitution $q/p; p/q; \lnot \lnot p/r$, and mp and definition of $\rightarrow$.

*2.6 --- $\vdash (\lnot p \rightarrow q) \rightarrow ((p \rightarrow q) \rightarrow q)$.

Proof

$\vdash (\lnot p \rightarrow q) \rightarrow ((\lnot p \lor q) \rightarrow (q \lor q))$ --- from Syll (*2.38) with the subst $q/p; \lnot p/q; q/r$

$\vdash [(\lnot p \lor q) \rightarrow (q \lor q)] \rightarrow [(\lnot p \lor q) \rightarrow q]$ --- from Taut, Sum and mp

$\vdash (\lnot p \rightarrow q) \rightarrow ((\lnot p \lor q) \rightarrow q)$ --- from the two formulas above by Syll (*2.06). Using the abbreviation of $\rightarrow$ we arrive at the final version of the theorem.

*2.62 --- $\vdash (p \lor q) \rightarrow ((p \rightarrow q) \rightarrow q)$ --- from (*2.53) and (*2.6) by Syll.

*2.621 --- $\vdash (p \rightarrow q) \rightarrow ((p \lor q) \rightarrow q)$ --- from (*2.62) with Comm and mp.

*2.73 --- $\vdash (p \rightarrow q) \rightarrow [((p \lor q) \lor r) \rightarrow (q \lor r)]$ --- from (*2.621) and (*2.38), with the substitution : $p \lor q/q; q/r; r/p$ and Syll.

*2.74 --- $\vdash (q \rightarrow p) \rightarrow [((q \lor p) \lor r) \rightarrow (p \lor r)]$ --- from (*2.73) with the substitution : $q/p; p/q$.

Note. We need several steps of Perm and Assoc to get from : $((q \lor p) \lor r)$ to $(p \lor (q \lor r))$ inside the formula. We write the first one.

From : $(q \rightarrow p) \rightarrow [((q \lor p) \lor r) \rightarrow (p \lor r)]$ we apply Comm to get : $((q \lor p) \lor r) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$; then we use Assoc and Syll to get : $(r \lor (q \lor p)) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$; and so on, until we arrive at : $(p \lor (q \lor r)) \rightarrow [(q \rightarrow p) \rightarrow (p \lor r)]$.

At the end of the transformations, we apply again Comm :

*2.74 --- $\vdash (q \rightarrow p) \rightarrow [(p \lor (q \lor r)) \rightarrow (p \lor r)]$.

From (*2.74) with the substitution $\lnot q/q$ and (*2.53), with Syll, we get :

$\vdash (q \lor p) \rightarrow [((p \lor (\lnot q \lor r)) \rightarrow (p \lor r)]$.

Using Perm and Syll and the definition of $\rightarrow$ we arrive at the final version :

*2.75 --- $\vdash (p \lor q) \rightarrow [(p \lor (q \rightarrow r)) \rightarrow (p \lor r)]$.

From *2.75 by Comm we derive :

*2.76 --- $\vdash (p \lor (q \rightarrow r)) \rightarrow ((p \lor q) \rightarrow (p \lor r))$.

From *2.76, with the substitution : $\lnot p/p; q/q; r/r$ we get :

*2.77 --- $\vdash (p \rightarrow (q \rightarrow r)) \rightarrow ((p \rightarrow q) \rightarrow (p \rightarrow r))$.

---

Appendix. We prove the “missing” axiom : Assoc (*1.05) that has been proved to be derivable from the others PM’s axioms by Bernays (in addition to the other four axioms, we will use only Syll) :

$\vdash (p \lor (q \lor r)) \rightarrow ((p \lor q) \lor r))$;

Proof

$\vdash r \rightarrow (p \lor r)$ --- Add (*1.3)

$\vdash r \rightarrow (p \lor r) \rightarrow [q \lor r \rightarrow q \lor (p \lor r)]$ --- from Sum (*1.6) with subst $r/q;p \lor r/r; q/p$

$\vdash q \lor r \rightarrow q \lor (p \lor r)$ --- modus ponens

$\vdash p \lor (q \lor r) \rightarrow p \lor [q \lor (p \lor r)]$ --- from Sum with the subst $p/p; q \lor r/q; q \lor (p \lor r)/r$ and mp

(A) --- $\vdash p \lor (q \lor r) \rightarrow [q \lor (p \lor r)] \lor p$ --- by Perm (*1.4) and Syll (*2.05)

$\vdash p \rightarrow (r \lor p)$ --- Add

$\vdash p \lor r \rightarrow q \lor (p \lor r)$ --- from above with substitution : $p \lor r/p; q/r$

$\vdash p \rightarrow (p \lor r)$ --- from Add (*1.3) and Perm (*1.4) by Syll (*2.05)

$\vdash p \rightarrow q \lor (p \lor r)$ --- from the last two by Syll

$\vdash [q \lor (p \lor r)] \lor p \rightarrow ([q \lor (p \lor r)] \lor [q \lor (p \lor r)])$ --- from the last by Syll

(B) --- $\vdash [q \lor (p \lor r)] \lor p \rightarrow [q \lor (p \lor r)]$ --- from the last using Taut and Syll.

Finally, from (A) and (B) by Syll :

$\vdash p \lor (q \lor r) \rightarrow (q \lor (p \lor r))$.

Having used only (*2.05) in the proof of Assoc, we can use Assoc to prove Comm (*2.04) :

$\vdash (p \rightarrow (q \rightarrow r)) \rightarrow (q \rightarrow (p \rightarrow r))$ --- from Assoc with the substitution : $\lnot p/p; \lnot q/q; r/r$.

Now, having proved Comm, we can go on from (*2.06).

Answer 3

According to Willemien's answer above, it is not possible to prove it from the proposed axiom system.

It is provable in Principia Mathematica system (which uses the first four axioms and modus ponens) due to the introduction of the abbreviation :

$p \supset q =_{def} \lnot p \lor q$.

This is a "simplified" proof [see (T9) below], following Peter Andrews, An Introduction to Mathematical Logic and Type Theory : To Truth Through Proof (1986).

Preliminaries

I will call the four Axioms as (Ax1)-(Ax4) [see Russell-Bernays axiom system with negation and disjunction] and the five following results as (R5)-(R9).

I will introduce the definition :

$A \rightarrow B$ stands for $\lnot A \lor B$. [*1.01]

We can have also : $A \land B$ stands for $\lnot (\lnot A \lor \lnot B)$ [*3.01], and $A \leftrightarrow B$ stands for $(A \rightarrow B) \land (B \rightarrow A)$ [*4.01].

The axioms will be stated in the primitive form as :

(Ax1’). $\lnot (A\lor A) \lor A$ --- (Taut) [*1.2]

(Ax2’). $\lnot A \lor (A\lor B)$ --- (Add) [*1.3]

(Ax3’). $\lnot (A\lor B) \lor (B\lor A)$ --- (Perm) [*1.4]

(Ax4’). $\lnot (\lnot A \lor B) \lor [\lnot (A\lor C) \lor (B\lor C)]$ --- (Sum) [*1.5]

The original versions will be derived using the definition of $\rightarrow$.

As inference rules, we will use only modus ponens [*1.1], formulated using the definition of $\rightarrow$ as :

from $A$ and $A \rightarrow B$, $B$ may be inferred;

and the substitution rule :

for a propositional variable any formula may be substituted.

I will call (R5) as Syll [*2.06].

About (R7 - Double Negation) : $\vdash A\leftrightarrow \neg(\neg A)$, we are able to prove it as (T2) and (T3), and we really need only : $\vdash A\rightarrow \neg(\neg A)$.

About (R8) and (R9), they will not be used in the proofs below.

From (Ax4) we derive the rule :

(R10). If $\vdash (A\rightarrow B)$ and $\vdash (A\lor C)$, then $\vdash (B\lor C)$ .

From (Ax3) we derive the rule :

(R11). If $\vdash (A\lor B)$, then $\vdash (B\lor A)$.

---

Initial theorems

(T1). $\vdash A \lor \lnot A$. [*2.11]

Proof

$\vdash ((A \lor A) \rightarrow A) \rightarrow [((A \lor A) \lor \lnot A) \rightarrow (A \lor \lnot A)]$ --- from (Ax4) with the subst: $A \lor A/A; A/B; \lnot A/C$

$\vdash (A \lor A) \rightarrow A$ --- (Ax1)

$\vdash ((A \lor A) \lor \lnot A) \rightarrow (A \lor \lnot A)$ --- by MP

$\vdash (A \lor A) \lor \lnot A $ --- from (Ax2’) with the subst $A/A; A/B$ using (Ax3) and Syll

$\vdash A \lor \lnot A$ --- by MP.

(T2). $\vdash A \rightarrow \lnot \lnot A$. [*2.12]

Proof

From (T1) with the subst : $\lnot A/A$ and the definition of $\rightarrow$.

(T3). $\vdash \lnot \lnot A \rightarrow A$. [*2.14]

Proof

$\vdash (\lnot A \rightarrow \lnot \lnot \lnot A) \rightarrow ((\lnot A \lor A) \rightarrow (\lnot \lnot \lnot A \lor A))$ --- (Ax4)

$\vdash \lnot A \lor A \rightarrow (\lnot \lnot \lnot A \lor A)$ --- from (T2) with the subst $\lnot A/A$ by MP

$\vdash \lnot \lnot A \rightarrow A$ --- with (Ax3) and Syll by MP, and definition of $\rightarrow$.

(T4). If $\vdash A \rightarrow C$ and $\vdash B \rightarrow C$, then $\vdash (A \lor B) \rightarrow C$.

Proof

$\vdash B \rightarrow C$ --- assumed

$\vdash B \lor A \rightarrow C \lor A$ --- (Ax4) and MP

$\vdash B \lor A \rightarrow A \lor C$ --- (Ax3) and Syll

$\vdash A \lor B \rightarrow A \lor C$ --- (Ax3) and Syll

$\vdash A \rightarrow C$ --- assumed

$\vdash A \lor C \rightarrow C \lor C$ --- (Ax4) and MP

$\vdash A \lor B \rightarrow C \lor C$ --- Syll

$\vdash C \lor C \rightarrow C$ --- (Ax1)

$\vdash A \lor B \rightarrow C$ --- Syll

(T5). If $\vdash A \rightarrow C$ and $\vdash \lnot A \rightarrow C$, then $\vdash C$. [*2.61]

Proof

By (T4) with the subst : $\lnot A/B$ and (T1) and MP.

(T6). If $\vdash A \rightarrow C$, then $\vdash A \rightarrow (C \lor B)$ and $\vdash A \rightarrow (B \lor C)$.

Proof

$\vdash A \rightarrow B$ --- assumed

$\vdash A \rightarrow (C \lor B)$ --- (Ax2) and Syll

$\vdash A \rightarrow (B \lor C)$ --- (Ax3) and Syll

(T7). $\vdash [(A \lor B) \lor C] \rightarrow [A \lor (B \lor C)]$. [*2.32]

Proof

1) $\vdash A \rightarrow [A \lor (B \lor C)]$ --- from (R6) and (T6)

2) $\vdash B \rightarrow (B \lor C)$ --- from (R6) and (T6)

3) $\vdash B \rightarrow [A \lor (B \lor C)]$ --- from 2) by (T6)

4) $\vdash (A \lor B) \rightarrow [A \lor (B \lor C)]$ --- from 1) and 3) by (T4)

5) $\vdash C \rightarrow (B \lor C)$ --- from (R6) and (T6)

6) $\vdash C \rightarrow [A \lor (B \lor C)]$ --- from 5) by (T6)

7) $\vdash [(A \lor B) \lor C] \rightarrow [A \lor (B \lor C)]$ --- from 4) and 6) by (T4)

(T8). If $\vdash (A \lor B) \lor C$, then $\vdash A \lor (B \lor C)$.

Proof

From (T7).

---

Main theorem

(T9). If $\vdash (A \rightarrow B)$ and $\vdash A \rightarrow (B \rightarrow C)$, then $\vdash A \rightarrow C$.

Proof

1) $\vdash A \rightarrow B$ --- assumed

2) $\vdash A \rightarrow (B \rightarrow C)$ --- assumed

3) $\vdash \lnot A \lor (\lnot B \lor C)$ --- by definition of $\rightarrow$

4) $\vdash (\lnot B \lor C) \lor \lnot A$ --- from 3) by (R11)

5) $\vdash \lnot B \lor (C \lor \lnot A)$ --- by (T8)

6) $\vdash B \rightarrow (C \lor \lnot A)$ --- by definition of $\rightarrow$

7) $\vdash A \rightarrow (C \lor \lnot A)$ --- from 1) and 6) by Syll

8) $\vdash \lnot A \lor (C \lor \lnot A)$ --- by definition of $\rightarrow$

9) $\vdash (C \lor \lnot A) \lor \lnot A$ --- by (R11)

10) $\vdash C \lor (\lnot A \lor \lnot A)$ --- by (T8)

11) $\vdash (\lnot A \lor \lnot A) \lor C$ --- from 10) by (Ax3)

12) $\vdash \lnot A \lor C$ --- from (Ax1) (i.e.$\vdash (\lnot A \lor \lnot A) \rightarrow \lnot A$) and (11) by (R10)

13) $\vdash A \rightarrow C$ --- by definition of $\rightarrow$.

For the original version of (*2.77), see the other answer (for most of applications, the present version suffices).

---

Additional results

(T10). $\vdash A \rightarrow (\lnot A \rightarrow B)$. [*2.24]

Proof

From (T2) and (T6) by MP.

(T11). $\vdash (A \lor B) \rightarrow (\lnot A \rightarrow B)$. [*2.53]

Proof

$\vdash (A \rightarrow \lnot \lnot A) \rightarrow ((A \lor B) \rightarrow (\lnot \lnot A \lor B))$ --- (Ax4)

$\vdash (A \lor B) \rightarrow (\lnot \lnot A \lor B)$ --- by (T2) with MP

$\vdash (A \lor B) \rightarrow (\lnot A \rightarrow B)$ --- by definition of $\rightarrow$.

(T12). $\vdash (\lnot A \rightarrow B) \rightarrow (A \lor B)$. [*2.54]

Proof

As (T11) from (T3).