My Math Forum propositional calculus

 Abstract Algebra Abstract Algebra Math Forum

 April 12th, 2014, 08:00 PM #1 Newbie   Joined: Apr 2014 From: australia Posts: 17 Thanks: 1 propositional calculus Hi, I'm having trouble proving the following sequent using the rules of deduction in the Propositional Calculus. (P âˆ¨Q)âˆ§(P âˆ¨R) âŠ¢ P âˆ¨(Qâˆ§R) any help would be appreciated. thanks
 April 13th, 2014, 12:57 AM #2 Senior Member   Joined: Dec 2013 From: Russia Posts: 327 Thanks: 108 Are the two formulas separated by the turnstile? My browser shows just a space between them. There are many variants of rules of deduction in the propositional calculus, and none of them is the default one. Which one are you using?
 April 13th, 2014, 02:55 AM #3 Newbie   Joined: Apr 2014 From: australia Posts: 17 Thanks: 1 Yes they are separated by a syntactic turnstile (P âˆ¨Q)âˆ§(P âˆ¨R) âŠ¢ P âˆ¨(Qâˆ§R) I'm thinking to use V-Elimination, but i'm having trouble reaching the conclusion.
April 13th, 2014, 06:51 AM   #4
Senior Member

Joined: Dec 2013
From: Russia

Posts: 327
Thanks: 108

Quote:
 Originally Posted by Evgeny.Makarov There are many variants of rules of deduction in the propositional calculus, and none of them is the default one. Which one are you using?
You'd rather keep the name of the formalism and the inference rules a secret, right?

Judging by the name "v-elimination", you are working with natural deduction. The outline of the derivation is as follows. Derive P \/ Q and P \/ R by /\-elimination. Perform a \/-elimination on P \/ Q. If P, then P \/ (Q /\ R), so the conclusion is proved. Otherwise, you have an assumption Q. Perform \/-elimination on P \/ R. Again, if P, then P \/ (Q /\ R). Otherwise, you have R, and together with Q it gives Q /\ R and P \/ (Q /\ R).

 April 14th, 2014, 07:45 PM #5 Newbie   Joined: Apr 2014 From: australia Posts: 17 Thanks: 1 So this is what I have so far 1 (1) (P V Q) & (P V R) A 1 (2) P V Q 1 &E 3 (3) P A 3 (4) P V (Q & R) 3 VI 1 (5) P V R 1 &E 6 (6) Q A 7 (7) R A 6,7 ( Q & R 6, 7 &I 3,6,7 (9) P V (Q & R) 3, 8 VI then Im stuck. .
April 15th, 2014, 01:23 AM   #6
Senior Member

Joined: Apr 2014
From: Greater London, England, UK

Posts: 320
Thanks: 156

Math Focus: Abstract algebra
Quote:
 Originally Posted by kp100591 1 (1) (P V Q) & (P V R) A 1 (2) P V Q 1 &E 3 (3) P A 3 (4) P V (Q & R) 3 VI 1 (5) P V R 1 &E 6 (6) Q A 7 (7) R A 6,7 (8) Q & R 6, 7 &I 3,6,7 (9) P V (Q & R) 3, 8 VI
Thanks for your working. Now I know roughly what axioms you are using. Here is my suggestion.

$$\begin{array}{rll} 1. & (P\vee Q)\,\&\,(P\vee R) & \mathrm{(A)} \\ 2. & P\vee Q & \mathrm{(1\ \&E)} \\ 3. & P & \mathrm{(2\ A)} \\ 4. & P\vee(Q\,\&\,R) & \mathrm{(3\ \vee I)} \\ 5. & Q & \mathrm{(2\ A)} \\ 6. & P\vee R & \mathrm{(1\ \&E)} \\ 7. & P & \mathrm{(6\ A)} \\ 8. & P\vee(Q\,\&\,R) & \mathrm{(7\ \vee I)} \\ 9. & R & \mathrm{(6\ A)} \\10. & Q\,\&\,R & \mathrm{(5,9\ \&I)} \\11. & P\vee(Q\,\&\,R) & \mathrm{(10\ \vee I)} \end{array}$$

There are a number of ways to approach the study of propositional calculus, each with its own set of axioms. Another way to approach the problem would be to show that the premise and the negation of the conclusion together form an inconsistent set.

 April 15th, 2014, 07:28 AM #7 Senior Member   Joined: Dec 2013 From: Russia Posts: 327 Thanks: 108 The derivation in post #5 looks like a derivation in Fitch-style calculus, or flag notation, which is a form of natural deduction. I'll just add the necessary indentation and disjunction elimination rules to post #6. Code:  1. (P \/ Q) /\ (P \/ R) Assumption 2. P \/ Q 1, /\E 3. P Assumption 4. P \/ (Q /\ R) 3, \/I 5. Q Assumption 6. P \/ R 1, /\E 7. P Assumption 8. P \/ (Q /\ R) 7, \/I 9. R Assumption 10. Q /\ R 5, 9, /\I 11. P \/ (Q /\ R) 10, \/I 12. P \/ (Q /\ R) 6, 7-8, 9-11, \/E 13. P \/ (Q /\ R) 2, 3-4, 5-12, \/E Unfortunately, the [ code] tag does not currently use a fixed-width font, so the alignment is not perfect. You can hopefully copy-paste the derivation into a text editor with a fixed-width font. Thanks from Olinguito and kp100591
 April 16th, 2014, 03:57 AM #8 Newbie   Joined: Apr 2014 From: australia Posts: 17 Thanks: 1 thank you for your assistance

 Thread Tools Display Modes Linear Mode

 Similar Threads Thread Thread Starter Forum Replies Last Post lun123 Applied Math 1 October 21st, 2013 02:28 PM zcohen Applied Math 2 April 26th, 2012 05:35 PM summer90 Applied Math 2 January 27th, 2010 09:26 AM patel_ankz Applied Math 1 November 8th, 2008 06:43 PM Christi123 Applied Math 0 March 25th, 2008 11:39 PM

 Contact - Home - Forums - Cryptocurrency Forum - Top