|
Post by Eugene 2.0 on Feb 20, 2021 0:40:09 GMT
Thesis: (p⊃(q⊃r))⊃(p&q⊃r))
Axioms: • p⊃(q⊃p) (I) • (p⊃(q⊃r))⊃((p⊃q)⊃(p⊃r)) (II) • p&q⊃p (III) • p&q⊃q (IV)
Methods: modus ponens
1. (p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme of A2/ 2. ((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r)))⊃(p⊃(q⊃r))⊃( (p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme of A1/ 3. (p⊃(q⊃r))⊃((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /1, 2 MP/ 4. (p⊃(q⊃r))⊃((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r)))⊃((p⊃(q⊃r))⊃((p&q)⊃(p⊃(q⊃r))⊃((p⊃(q⊃r))⊃(p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme of A2/ 5. (p⊃(q⊃r))⊃((p&q)⊃(p⊃(q⊃r))⊃((p⊃(q⊃r))⊃(p&q⊃p)⊃(p&q⊃(q⊃r))) /3, 4 MP/ 6. (p⊃(q⊃r))⊃((p&q)⊃(p⊃(q⊃r)) /scheme of A1/ 7. (p⊃(q⊃r))⊃(p&q⊃p)⊃(p&q⊃(q⊃r)) /6, 5 MP/ 8. (p&q⊃p)⊃((p⊃(q⊃r))⊃(p&q⊃p)) /scheme of A1/ 9. p&q⊃p /scheme of A3/ 10. (p⊃(q⊃r))⊃(p&q⊃p)) /9, 8 MP/ 11. (p&q⊃(q⊃r)) /10, 7 MP/ 12. (p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r)) /scheme of A2/ 13. (p&q⊃q)⊃(p&q⊃r) /11, 12 MP/ 14. p&q⊃q /scheme of A3/ 15. p&q⊃r /14, 13 MP/ 16. (p&q⊃r)⊃((p⊃(q⊃r))->(p&q⊃r)) /scheme of A1/ (p⊃(q⊃r))⊃(p&q⊃r)) /15, 16 MP/
I hope someone will re-check it, because I'm so exhausted proving such formulas. I've found the way to prove schemes like this, but I can't be certain about it. Anyway, I hope you'll enjoy this proof.
|
|
|
Post by Eugene 2.0 on Feb 21, 2021 23:53:15 GMT
Proving The Law of Transportation. Take II
The previous one was false at the step #10. New two axioms are required too.
The thesis: (p⊃(q⊃r))⊃(p&q⊃r))
Axioms:
• p⊃(q⊃p) (I) • (p⊃(q⊃r))⊃((p⊃q)⊃(p⊃r)) (II) • p&q⊃p (III) • p&q⊃q (IV) • ((p⊃q)&(q⊃r))⊃(p⊃r) (V) • p⊃(q⊃(p&q)) (VI)
A rule: modus ponens
1. (p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme A2/ 2. ((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r)))⊃(p⊃(q⊃r))⊃( (p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme A1/ 3. (p⊃(q⊃r))⊃((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))) /1, 2 MP/ 4. (p⊃(q⊃r))⊃((p&q⊃(p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r)))⊃((p⊃(q⊃r))⊃((p&q)⊃(p⊃(q⊃r))⊃((p⊃(q⊃r))⊃(p&q⊃p)⊃(p&q⊃(q⊃r))) /scheme A2/ 5. (p⊃(q⊃r))⊃((p&q)⊃((p⊃(q⊃r))⊃((p⊃(q⊃r))⊃(p&q⊃p)⊃(p&q⊃(q⊃r))) /3, 4 MP/ 6. (p⊃(q⊃r))⊃((p&q)⊃(p⊃(q⊃r)) /scheme A1/ 7. (p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r)) /6, 5 MP/ 8. (p⊃(q⊃r))⊃((p&q⊃p)⊃(p&q⊃(q⊃r))⊃((p⊃(q⊃r))⊃(p&q⊃p))⊃((p⊃(q⊃r))⊃((p&q⊃(q⊃r))) /scheme А2/ 9. ((p⊃(q⊃r))⊃(p&q⊃p))⊃((p⊃(q⊃r))⊃((p&q⊃(q⊃r)) /7, 8 МР/ 10. (p&q⊃p)⊃((p⊃(q⊃r))⊃(p&q⊃p)) /scheme А1/ 11. (p&q⊃p) /scheme А3/ 12. (p⊃(q⊃r))⊃(p&q⊃p)) /11, 10 MP/ 13. (p⊃(q⊃r))⊃((p&q⊃(q⊃r)) /12, 9 МР/ 14. (p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r)) /scheme A2/ 15. (p⊃(q⊃r))⊃((p&q⊃(q⊃r))⊃((p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r))⊃(((p⊃(q⊃r))⊃((p&q⊃(q⊃r))&((p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r))) /scheme А6/ 16. (p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r))⊃(((p⊃(q⊃r))⊃((p&q⊃(q⊃r))&((p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r)) /13, 15 МР/ 17. ((p⊃(q⊃r))⊃((p&q⊃(q⊃r))&((p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r)) /14, 16 МР/ 18. ((p⊃(q⊃r))⊃((p&q⊃(q⊃r))&((p&q⊃(q⊃r))⊃((p&q⊃q)⊃(p&q⊃r))⊃(p⊃(q⊃r))⊃(p&q⊃r)) /scheme А5/ (p⊃(q⊃r))⊃(p&q⊃r) /17, 18 MP/
It's not unimportant to pay attention to tautologies in the proof tree. If there are non-tautologies, then there's no proof. The previous proof derived (p&q⊃r), but it was absolutely impossible.
|
|