0

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? enter image description here

  • This is not a question. Can you please explain why this belongs here, and what kind of answer you're expecting? – iphigenie Jan 4 '14 at 12:04
  • @iphigenie: The last sentence can be easily rewritten as a question. – DBK Jan 4 '14 at 16:04
  • @DBK: Thanks. I have rephrased it as a question. – George Chen Jan 4 '14 at 18:45
  • 1
    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. – Hunan Rostomyan Feb 3 '14 at 19:55
1

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. – George Chen Feb 4 '14 at 9:05
2

Your comment is right.

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.

  • 2
    P.S. I think that a more proper place for this kind of questions is math.stackexchange. – Mauro ALLEGRANZA Jan 4 '14 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 – George Chen Jan 4 '14 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. – George Chen Jan 4 '14 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. – George Chen Jan 4 '14 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. – Mauro ALLEGRANZA Jan 5 '14 at 10:06

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.