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)$
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) &\wedge &(B \supset C) &\wedge &(D \supset \neg C) &\wedge &(A \vee D)) &\supset (B \vee \neg C))\\<br /> <br /> \neg ( \neg((A \supset B) &\wedge &(B \supset C) &\wedge &(D \supset \neg C) &\wedge &(A \vee D)) &\vee &(B \vee \neg C))\\<br /> <br /> ((A \supset B) &, &(B \supset C) &, &(D \supset \neg C) &, &(A \vee D)) &, &\neg (B \vee \neg C))\\<br /> <br /> (\neg A \vee B) &, &(\neg B \vee C) &, &(\neg D \vee \neg C) &, &(A \vee D) &, &\neg B&, &C))\\<br /> <br /> \text{contradiction}&, &\neg B &, &\neg D&, &A &, &\neg B &, &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)$

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} \;&\{a_1, a_2, ..., a_n\} &\models A\\<br /> \text{then} \; &\{a_1, a_2, ..., a_n\} &\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\} &\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