Mixing
Proving De Morgan's Law with Natural Deduction
$begingroup$
Here is my attempt, but I'm really not sure if I've done it right;
as I'm just about getting the hang of Natural Deduction technique.
Have I done it correctly? If not, where did I make errors and how should I do it?
Thank you in advance!
Sorry for the bad image quality; I'm bad at taking pictures.
logic propositional-calculus natural-deduction
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
$endgroup$
|
show 3 more comments
$begingroup$
Here is my attempt, but I'm really not sure if I've done it right;
as I'm just about getting the hang of Natural Deduction technique.
Have I done it correctly? If not, where did I make errors and how should I do it?
Thank you in advance!
Sorry for the bad image quality; I'm bad at taking pictures.
logic propositional-calculus natural-deduction
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
$endgroup$
1
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
1
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52
|
show 3 more comments
$begingroup$
Here is my attempt, but I'm really not sure if I've done it right;
as I'm just about getting the hang of Natural Deduction technique.
Have I done it correctly? If not, where did I make errors and how should I do it?
Thank you in advance!
Sorry for the bad image quality; I'm bad at taking pictures.
logic propositional-calculus natural-deduction
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
$endgroup$
Here is my attempt, but I'm really not sure if I've done it right;
as I'm just about getting the hang of Natural Deduction technique.
Have I done it correctly? If not, where did I make errors and how should I do it?
Thank you in advance!
Sorry for the bad image quality; I'm bad at taking pictures.
logic propositional-calculus natural-deduction
logic propositional-calculus natural-deduction
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
asked Feb 26 '15 at 8:39
HaxifyHaxify
150116
150116
1
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
1
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52
|
show 3 more comments
1
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
1
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52
1
1
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
1
1
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52
|
show 3 more comments
3 Answers
3
active
oldest
votes
$begingroup$
In the second part lines 2 and 7 are redundant, instead assume line 3.
Edit: As noticed by @GitGud, in the first part, line 6 must be $negneg p (neg I)$. So you need to add another line to get $p$ by $(negneg E)$. Similar correction for line 10.
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
$endgroup$
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
add a comment |
$begingroup$
Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.
Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.
{1} 1. ¬P ∨ ¬Q premise
{2} 2. P ∧ Q assumption for proof by contradiction
{2} 3. P 2 ∧E
{2} 4. Q 2 ∧E
{5} 5. ¬P assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5} 6. P ∧ ¬P 3,5 ∧I
{7} 7. ¬Q assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7} 8. Q ∧ ¬Q 4,7 ∧I
{1,2} 9. (P ∧ ¬P) ∨ (Q ∧ ¬Q) 1,5,6,7,8 Discharge 5,7 i.e. ⊥
{1} 10. ¬(P ∧ Q) 2,9 proof by contradiction, discharge 2
Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).
11 Feb:
Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!
edited Feb 21 at 6:11
Frank Hubeny
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
$endgroup$
add a comment |
$begingroup$
The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:
The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.
As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.
The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
protected by Community♦ Feb 1 at 17:08
Thank you for your interest in this question.
Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).
Would you like to answer one of these unanswered questions instead?
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
In the second part lines 2 and 7 are redundant, instead assume line 3.
Edit: As noticed by @GitGud, in the first part, line 6 must be $negneg p (neg I)$. So you need to add another line to get $p$ by $(negneg E)$. Similar correction for line 10.
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
$endgroup$
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
add a comment |
$begingroup$
In the second part lines 2 and 7 are redundant, instead assume line 3.
Edit: As noticed by @GitGud, in the first part, line 6 must be $negneg p (neg I)$. So you need to add another line to get $p$ by $(negneg E)$. Similar correction for line 10.
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
$endgroup$
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
add a comment |
$begingroup$
In the second part lines 2 and 7 are redundant, instead assume line 3.
Edit: As noticed by @GitGud, in the first part, line 6 must be $negneg p (neg I)$. So you need to add another line to get $p$ by $(negneg E)$. Similar correction for line 10.
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
$endgroup$
In the second part lines 2 and 7 are redundant, instead assume line 3.
Edit: As noticed by @GitGud, in the first part, line 6 must be $negneg p (neg I)$. So you need to add another line to get $p$ by $(negneg E)$. Similar correction for line 10.
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
edited Feb 26 '15 at 23:08
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
answered Feb 26 '15 at 8:44
LoMaPhLoMaPh
8211916
8211916
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
add a comment |
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
Oh, I see it. Thank you! Are other parts all fine?
$endgroup$
– Haxify
Feb 26 '15 at 8:51
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
$begingroup$
They seem legit.
$endgroup$
– LoMaPh
Feb 26 '15 at 9:08
add a comment |
$begingroup$
Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.
Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.
{1} 1. ¬P ∨ ¬Q premise
{2} 2. P ∧ Q assumption for proof by contradiction
{2} 3. P 2 ∧E
{2} 4. Q 2 ∧E
{5} 5. ¬P assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5} 6. P ∧ ¬P 3,5 ∧I
{7} 7. ¬Q assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7} 8. Q ∧ ¬Q 4,7 ∧I
{1,2} 9. (P ∧ ¬P) ∨ (Q ∧ ¬Q) 1,5,6,7,8 Discharge 5,7 i.e. ⊥
{1} 10. ¬(P ∧ Q) 2,9 proof by contradiction, discharge 2
Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).
11 Feb:
Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!
edited Feb 21 at 6:11
Frank Hubeny
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
$endgroup$
add a comment |
$begingroup$
Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.
Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.
{1} 1. ¬P ∨ ¬Q premise
{2} 2. P ∧ Q assumption for proof by contradiction
{2} 3. P 2 ∧E
{2} 4. Q 2 ∧E
{5} 5. ¬P assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5} 6. P ∧ ¬P 3,5 ∧I
{7} 7. ¬Q assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7} 8. Q ∧ ¬Q 4,7 ∧I
{1,2} 9. (P ∧ ¬P) ∨ (Q ∧ ¬Q) 1,5,6,7,8 Discharge 5,7 i.e. ⊥
{1} 10. ¬(P ∧ Q) 2,9 proof by contradiction, discharge 2
Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).
11 Feb:
Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!
edited Feb 21 at 6:11
Frank Hubeny
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
$endgroup$
add a comment |
$begingroup$
Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.
Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.
{1} 1. ¬P ∨ ¬Q premise
{2} 2. P ∧ Q assumption for proof by contradiction
{2} 3. P 2 ∧E
{2} 4. Q 2 ∧E
{5} 5. ¬P assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5} 6. P ∧ ¬P 3,5 ∧I
{7} 7. ¬Q assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7} 8. Q ∧ ¬Q 4,7 ∧I
{1,2} 9. (P ∧ ¬P) ∨ (Q ∧ ¬Q) 1,5,6,7,8 Discharge 5,7 i.e. ⊥
{1} 10. ¬(P ∧ Q) 2,9 proof by contradiction, discharge 2
Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).
11 Feb:
Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!
edited Feb 21 at 6:11
Frank Hubeny
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
$endgroup$
Just a little uncomfortable with step 6 of part 2, i.e., using three steps (1,4,5) to assert a contradiction - seems like too much intuition for my liking. If possible, would like to limit myself to just the { φ ∧ ¬φ } form of contradiction. Minimal intuition - an object cannot be both itself and not itself at the same time.
Is the following possible instead? {n}, where n is a natural number, denotes underlying dependencies.
{1} 1. ¬P ∨ ¬Q premise
{2} 2. P ∧ Q assumption for proof by contradiction
{2} 3. P 2 ∧E
{2} 4. Q 2 ∧E
{5} 5. ¬P assumption, 1st disjunct of ¬P ∨ ¬Q
{2,5} 6. P ∧ ¬P 3,5 ∧I
{7} 7. ¬Q assumption, 2nd disjunct of ¬P ∨ ¬Q
{2,7} 8. Q ∧ ¬Q 4,7 ∧I
{1,2} 9. (P ∧ ¬P) ∨ (Q ∧ ¬Q) 1,5,6,7,8 Discharge 5,7 i.e. ⊥
{1} 10. ¬(P ∧ Q) 2,9 proof by contradiction, discharge 2
Since step 10 is an outcome of the premise alone, therefore (¬P ∨ ¬Q) ⊢ ¬(P ∧ Q).
11 Feb:
Just an additional comment after some thought. Citing steps 1 (¬P ∨ ¬Q), 4(P) and 6(Q) to justify a contradiction is implicitly claiming that (¬P ∨ ¬Q) is in contradiction with (P ∧ Q) (i.e. conjunction of steps 4 and 6). But this contradiction is the very thing we're trying to prove. That's why I wasn't comfortable previously. Glad for comments/correction if any. Thanks!
edited Feb 21 at 6:11
Frank Hubeny
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
edited Feb 21 at 6:11
Frank Hubeny
5312519
edited Feb 21 at 6:11
Frank Hubeny
5312519
edited Feb 21 at 6:11
Frank Hubeny
5312519
5312519
answered Feb 1 '16 at 8:05
WeiWei
133
answered Feb 1 '16 at 8:05
WeiWei
133
answered Feb 1 '16 at 8:05
WeiWei
133
133
add a comment |
add a comment |
$begingroup$
The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:
The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.
As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.
The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
$begingroup$
The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:
The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.
As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.
The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
$endgroup$
add a comment |
$begingroup$
The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:
The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.
As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.
The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
$endgroup$
The issue that @Wei brought up appears the most critical. Here is a proof imitating the script as much as possible:
The blue boxes on lines 6 and 10 show that the justification would be indirect proof (IP) not negation introduction. @LoMaPh offers a different suggestion for fixing that.
As LoMaPh points out one could skip lines 16 and 25, but it is not incorrect to leave them as they are.
The issue @Wei brought up is critical and is fixed in the red box. One needs to explicitly do a disjunction elimination on both disjuncts in line 15.
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
answered Feb 21 at 5:51
Frank HubenyFrank Hubeny
5312519
5312519
add a comment |
add a comment |
protected by Community♦ Feb 1 at 17:08
Thank you for your interest in this question.
Because it has attracted low-quality or spam answers that had to be removed, posting an answer now requires 10 reputation on this site (the association bonus does not count).
Would you like to answer one of these unanswered questions instead?
1
$begingroup$
I have found at least two mistakes (four actually, but two of them are repeated). And I suspect the whole thing might not be formally correct (even though you essentially got the process right) depending on a detail: what exactly is the meaning of $equiv$?
$endgroup$
– Git Gud
Feb 26 '15 at 9:14
$begingroup$
@GitGud It's used when two propositional formulas are equivalent; where every truth-value assignment gives same result for both propositional formulas. Could you tell me which parts are mistakes? Thank you!
$endgroup$
– Haxify
Feb 26 '15 at 9:24
$begingroup$
Then you can't give a formal proof of $neg (pland q)equiv neg plor neg q$ because this is a meta-statement. Note that $neg (pland q)leftrightarrow neg plor neg q$ and $neg (pland q)equiv neg plor neg q$ are different kind of objects. I'm still trying to get a sense of the meaning of the symbols you're using before explaining exactly what I mean because I don't want to go into unnecessary details, that's why I'm being a little vague.
$endgroup$
– Git Gud
Feb 26 '15 at 9:36
$begingroup$
@GitGud Because of the soundness of Natural Deduction, to prove $varphiequivpsi$ (i.e. $varphivDashpsi$ and $psivDashvarphi$), we can instead prove $varphivdashdashvpsi$.
$endgroup$
– LoMaPh
Feb 26 '15 at 22:15
1
$begingroup$
@LoMaPh Nothing wrong with that. But even though it isn't explicitly stated, the body of the question suggests the OP wants a formal a proof, I could be wrong. What is actually wrong is step $6$, the justification is not $bot text I$ (there's no way that's a badly written $neg$) and it should be $neg neg p$. Same thing on step 10.
$endgroup$
– Git Gud
Feb 26 '15 at 22:52