# Complicated Logic Proof involving Tautology and Law of Excluded Middle

I'm having great difficulty solving the following problem, and even figuring out where to start with the proof. $$\neg A\lor\neg(\neg B\land(\neg A\lor B))$$ Please see the following examples of how to do proofs, I would appreciate it if you could attempt to give me guidance using the tools and the line numbers that it cites similar to those below:

This is a sample proof:

This is another sample proof (law of excluded middles):

-
What logic are you using ? –  mercio Apr 3 '11 at 10:04
@chandok, This is First order logic. And it is about formal proofs and boolean logic. –  KerxPhilo Apr 3 '11 at 11:10

first of all the statement is true (checking truth values for $A$ and $B$), even though ive now given two incorrect answers... here we go again!

\begin{align} & \neg A \lor \neg (\neg B \land (\neg A \lor B))\\ & =\neg A \lor \neg [(\neg B \land \neg A) \lor (\neg B \land B)]\\ & =\neg A \lor \neg [(\neg B \land \neg A) \lor FALSE]\\ & =\neg A \lor \neg(\neg B\land\neg A)\\ & =\neg A\lor(B\lor A) \text{ using } \neg(X\land Y)=\neg X\lor\neg Y\\ & =TRUE \end{align}

formalize this in whatever system youre using, you might have to prove a few things beforehand...

-
Could you please elaborate further. I'm sorry, but I am having a very hard time comprehending your answer. Thank you so much for your support. –  KerxPhilo Apr 3 '11 at 8:01
How do you get $TRUE$ from $\lnot[(\lnot B\land\lnot A)\lor FALSE]$ ? –  Apostolos Apr 4 '11 at 12:20

Seems like assuming the negation would give you a contradiction:

use ~ for 'negation', and & for 'and'; then your negated assumption becomes:

A&(~B&(~A\/B)) (Assumption)

From which you get:

~B&(~A\/B) (By & elimination)

I think you can show from here that your (negated) assumption leads to a contradiction, by arguing by cases, from ~A\/B, and showing neither case is possible.

Now, ~A\/B follows using a second & elimination. Show neither ~A nor B is possible from the premises in your negated statement. Then from ~A\/B and ~(~A) and ~B, a contradiction to your negated assumption follows.

Edit: this may be much simpler, tho yoyo's answer may be better than mine in that he gives a direct proof, and mine is by contradiction:

Assume the negation of your statement:

i)A& (~B&(~A\/B))

ii)Conclude A, by detachment.

iii)Conclude ~A by detachment inside of parenthesis.

iv)Negation of 'i)' follows by contradiction A&~A

Where detachment--more precisely, &-detachment-- is the rule that allows us to conclude either A, or B, from a statement A&B. To show it is a valid rule, you can either use a truth table to show it is a tautology/logical truth, derive it from the empty set of premises (this is the definition of theorem I am more familiar with), or,equivalently, show that the negation of either of :(A&B-->A) or of (A&B-->A), is a contradiction.For the second approach, assume A&B, and just conclude A (seems tautological, but it works; many of these arguments in sentence logic seem tautological anyway), or transform the implication A&B->A into the equivalent statement ~(A&B)\/A == ~A\/~B\/A== ~A\/A\/B==(~A\/A)\/B (I'm using here the result that A->B is truth-functionally equiv. to ~A\/B), which is a tautology.

-
What do you mean by detachment? –  KerxPhilo Apr 3 '11 at 8:07
KerxPhilo: I mean that from an expression A&B, we can "detach" either A or B. More precisely, I mean –  gary Apr 3 '11 at 23:36
erxPhilo: I mean that from an expression A&B, we can "detach" either A or B. More precisely, that: i) A&B->A , and ii)A&B-> B, In my proof, specifically, from A&(~B&(~A\/B), we can "detach" either the 'A' on the left, or the expression '(~B&(~A\/B))' to the right of the '&'. Since we have another '&' in the parenthesis '(~B&(~A\/B))', we can detach either '~B'or '~A\ /B' –  gary Apr 3 '11 at 23:48
Sorry for the choppy formatting in the above comments, KerxPhilo. I edited my answer to incorporate everything into the answer. –  gary Apr 4 '11 at 3:28