share
MathematicsComplicated Logic Proof involving Tautology and Law of Excluded Middle
[+4] [4] Philoxopher
[2011-04-03 00:08:24]
[ logic ]
[ https://math.stackexchange.com/questions/30584/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 a sample proof

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

enter image description here

What logic are you using ? - mercio
@chandok, This is First order logic. And it is about formal proofs and boolean logic. - Philoxopher
[+4] [2011-04-03 00:45:38] yoyo [ACCEPTED]

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. - Philoxopher
(1) How do you get $TRUE$ from $\lnot[(\lnot B\land\lnot A)\lor FALSE]$ ? - Apostolos
1
[+1] [2011-04-03 01:54:53] gary

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? - Philoxopher
KerxPhilo: I mean that from an expression A&B, we can "detach" either A or B. More precisely, I mean - gary
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
Sorry for the choppy formatting in the above comments, KerxPhilo. I edited my answer to incorporate everything into the answer. - gary
2
[+1] [2014-07-22 09:04:24] Mauro ALLEGRANZA

The "complicated" formula :

$¬A∨¬(¬B∧(¬A∨B))$

can be re-written, due to the equivalence between $P \rightarrow Q$ and $\lnot P \lor Q$, as :

$A \rightarrow \lnot ((A \rightarrow B) \land \lnot B)$.

But $P \rightarrow Q$ is also equivalent to $\lnot (P \land \lnot Q)$; so the formula it is simply :

$A \rightarrow ((A \rightarrow B) \rightarrow B)$.

Now, a Natural Deduction proof is quite easy :

(1) $A$ - assumed

(2) $A \rightarrow B$ --- assumed

(3) $B$ --- from (1) and (2) by $\rightarrow$-elimination

(4) $(A \rightarrow B) \rightarrow B$ --- from (2) and (3) by $\rightarrow$-introduction

(5) $A \rightarrow ((A \rightarrow B) \rightarrow B)$ --- from (1) and (4) by $\rightarrow$-introduction.


3
[0] [2019-07-28 20:43:36] Frank Hubeny

Here is a proof using a Fitch-style proof checker.

enter image description here

Assume the negation of what one is trying to prove on line 1 to attempt to derive a contradiction.

From lines 2 to 9, use De Morgan rule (DeM), conjunction elimination (∧E), double negative elimination (DNE) and disjunctive syllogism (DS) to simplify so one can arrive at two lines, 4 and 9, which are contradictory. That contradiction allows one to derive the goal on line 11 using indirect proof (IP).

Links to the proof checker and associated text are below.


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf


4