# Question regarding the proof 3.3 in the Principia Mathematica

As far as I can understand, the key of PM is to make sure there are no leaps and gaps when making inferences. In other words, all the premises and rules of inferences should be explicitly enumerated with the exception of ❊1.11. I wonder , in the proof of ❊3.3, why Syll is omitted in the first and third step but is mentioned in the last step?

• This is not a question. Can you please explain why this belongs here, and what kind of answer you're expecting? Jan 4, 2014 at 12:04
• @iphigenie: The last sentence can be easily rewritten as a question.
– DBK
Jan 4, 2014 at 16:04
• @DBK: Thanks. I have rephrased it as a question. Jan 4, 2014 at 18:45
• George, Metamath is a good companion to have in your journey through PM. I wouldn't be surprised if 3.3, in a more pleasant notation, were found among the 1000s of proofs on that website. So check that out. Feb 3, 2014 at 19:55

lets first rewrite Russels proof in in modern notation:

``````Id(*3.01) = |- (((P & Q) -> R) -> (~(~P v ~Q) -> R)
transp                         -> (~R -> (~P v ~Q))
Id (*1.01)                     -> (~R -> (P -> ~Q))
comm                           -> (P -> (~R -> ~Q))
transP.syll                    -> (P -> (Q -> R))) |-. prop
``````

I do think Russel uses the rule of syllogism (|- P -> Q, |- Q -> R => |- P -> R ) without mentioning it, because it just makes the proof unnescesary complicated.

to add them to the proof it becomes

``````Id(*3.01)   = |- (((P & Q) -> R)   -> (~(~P v ~Q) -> R)
transp      = |- (~(~P v ~Q) -> R) -> (~R -> (~P v ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (~R -> (~P v ~Q))
Id (*1.01)  = |- (~R -> (~P v ~Q)) -> (~R -> (P -> ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (~R -> (P -> ~Q))
comm        = |- (~R -> (P -> ~Q)) -> (P -> (~R -> ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (P -> (~R -> ~Q))
transP.syll = |- (P -> (~R -> ~Q)) -> (P -> (Q -> R)))
--syllogism-- |- (((P & Q) -> R)   -> (P -> (Q -> R)))
``````

it just makes the proof 4 lines longer and much less whitespace, but if you find it better then do it this way (ps but even here don't you want to go back to the axioms?

• Thanks, @Willemien. At this stage what is obvious the authors is a big gap to me. That is why I think it is worth while to labour through the first five chapters. Hopefully I will be able to "see" what the authors "see" afterwards. Feb 4, 2014 at 9:05

The proof is based on a "chain" of conditionals; thus, we need Syll.

In the third step, in order to move from :

⊢ (p.q ⊃ r) ⊃ ( ~r ⊃ (p ⊃ ~q) ) --- (3)

to :

⊢ (p.q ⊃ r) ⊃ (p ⊃ ( ~r ⊃ ~q) ) --- (4)

we have to build up the "chain" :

(3) --- ⊢( ~r ⊃ (p ⊃ ~q) ) ⊃ (p ⊃ ( ~r ⊃ ~q) ) --- by Comm --- (4) --- by Syll.

All the proof today will be greatly simplified by use of to Deduction Theorem; it is missing in PM because it was discovered independently by Tarski and Herbrand during the '30s.

• P.S. I think that a more proper place for this kind of questions is math.stackexchange. Jan 4, 2014 at 16:02
• Thanks, @Mauro ALLEGRANZA. My goal here is to retrace the mental journey of Whitehead and Russell. That is why I use the first edition. What they set out to prove is not as important as the process of their proofs. I think you are right, I need to move it to math.stachexchange Jan 4, 2014 at 18:50
• I really like your comment. @Mauro ALLEGRANZA Thanks for providing the historical context. I don't know if anyone from math community has this kind calibre. Jan 4, 2014 at 19:27
• In PM, @Mauro ALLEGRANZA'S step 3 would be ❊2.16 Transp. As of chapter three, PM hasn't produced anything like Deduction Theorem yet, it makes do with ❊1.11, a Pp.(primitive proposition): when both Phi(x) and Phi(x) -> Psi(x) can be asserted, then Psi(x) can be asserted. Jan 4, 2014 at 20:08
• I confirm you that Deduction Theorem is not present in PM : it was stated for the first time during the '30s. *1.11 is more like a version of Modus Ponens for formulae with free variables. Jan 5, 2014 at 10:06