Can This Propositional Logic Proof Be Presented More Formally?

[gnome]

I want to prove (A \supset B) \wedge (B \supset C) \wedge (D \supset \neg C) \wedge (A \vee D) \equiv (B \vee \neg C)<br />
so I have to show that \neg ( ((A \supset B) \wedge (B \supset C) \wedge (D \supset \neg C) \wedge (A \vee D)) \supset (B \vee \neg C))
is inconsistent, and I proceed as follows:

\begin{array}{ccccccccccc}\neg ( ((A \supset B) &amp;\wedge &amp;(B \supset C) &amp;\wedge &amp;(D \supset \neg C) &amp;\wedge &amp;(A \vee D)) &amp;\supset (B \vee \neg C))\\<br /> <br /> \neg ( \neg((A \supset B) &amp;\wedge &amp;(B \supset C) &amp;\wedge &amp;(D \supset \neg C) &amp;\wedge &amp;(A \vee D)) &amp;\vee &amp;(B \vee \neg C))\\<br /> <br /> ((A \supset B) &amp;, &amp;(B \supset C) &amp;, &amp;(D \supset \neg C) &amp;, &amp;(A \vee D)) &amp;, &amp;\neg (B \vee \neg C))\\<br /> <br /> (\neg A \vee B) &amp;, &amp;(\neg B \vee C) &amp;, &amp;(\neg D \vee \neg C) &amp;, &amp;(A \vee D) &amp;, &amp;\neg B&amp;, &amp;C))\\<br /> <br /> \text{contradiction}&amp;, &amp;\neg B &amp;, &amp;\neg D&amp;, &amp;A &amp;, &amp;\neg B &amp;, &amp;C<br /> <br /> \end{array}

so I end up with a contradiction showing that the original statement is correct.

Question: is there a "better", more formal way to present this proof?

 

[mathwonk]

You seem to have that screwed up. for instance in case A is false but B is true, then the left side is false but the right side is true, so they are not equivalent.




Maybe instead of the last two operational symbols being "and" , then "equivalence", they should be the opposite order, "equivalence", then "and".

i.e. the following two statements might be equivalent:

I. C implies B and B implies A, and notC implies D,

II. [either B or notC], and[ either A or D].

at least I implies II. let see... no that doesn't work either. then if B is true and A is true, but D is false, one side is true and the other is false.

 

[AKG]

Assuming I didn't make a mistake, it seems to me that what you're trying to prove is false (so you can't prove it). Make a truth table, the two sentences aren't "nearly" equivalent.

 

[gnome]

So sorry. I meant to write:

(A \supset B) \wedge (B \supset C) \wedge (D \supset \neg C) \wedge (A \vee D) \models (B \vee \neg C)<br />

as the first line.

 

[mathwonk]

what do the symbols mean? especially that one that now replaces equivalence?

 

[Eratosthenes]

I believe it is read "yields" if it is the same as |-


I've seen it used in place of the logical implication symbol so I guess they are the same thing.

 

[gnome]

The meanings are similar but not exactly the same.

According to what I've read so far, the first one, \models, is called the "semantic turnstile".
\begin{array}{lll} \text{if} \;&amp;\{a_1, a_2, ..., a_n\} &amp;\models A\\<br /> \text{then} \; &amp;\{a_1, a_2, ..., a_n\} &amp;\supset A \; \text{is a tautology}\end{array}
or we can say that A is a logical consequence of {a_1, a_2, ..., a_n}.

The other one, \vdash, I think is called the "syntactic turnstile". and
\{a_1, a_2, ..., a_n\} &amp;\vdash A
means that A can be proved from \{a_1, a_2, ..., a_n\} by using a set of syntactic rules.

But frankly, I can't say that I'm clear about exactly what the difference is between those two statements, so I'd love to hear a better explanation from someone who knows.

 

[AKG]

So sorry. I meant to write:

(A \supset B) \wedge (B \supset C) \wedge (D \supset \neg C) \wedge (A \vee D) \models (B \vee \neg C)

as the first line.

This is easy to prove. As far as I know, it should technically be written as:

\{(A \supset B) \wedge (B \supset C) \wedge (D \supset \neg C) \wedge (A \vee D)\} \models (B \vee \neg C)

since it is a set of sentences which are said to entail a conclusion sentence. I'm not sure what system of deduction you're using. The only one I'm familiar with is SD. Let's replace the premise by *.

1  | *                             Assumption
   |------------------------------
2  | | A                           Assumption
   | |----------------------------
3  | | A > B                       1 conjunction elimination
4  | | B                           2-3 conditional elimination
5  | | B v ~C                      4 disjunction introduction
   |
6  | | D                           Assumption
   | |----------------------------
7  | | D > ~C                      1 conjunction elimination 
8  | | ~C                          6-7 conditional elimination
9  | | B v ~C                      8 disjunction introduction
   |
10 | A v D                         1 conjunction elimination
11 | B v ~C                        10, 2-5, 6-9 disjunction elimination