Simple Fitch Proof

Question

after lots of googling i still do not have the answer for this problem. There are not premisses give, just the goal, which is: $$((X ∧ Y) ∨ (Y ∧ Z) ∨ (W ∧ Y)) \rightarrow Y$$

Can anyone tell me how to do that fitch proof?
I still don't understand how to start fitch proofs with no premisses.

Thank you guys!

Answer 1

The first thing that must be done is to assume the antecedent of your conclusion. The rest follows from using $\wedge$ and $\vee$ elimination.

Answer 2

This is probably the only way I can solve this with my poor student background. (:

Don't complicate it because there is really no need for it. I prefer this approach. A contradiction is a very last option when you're desperate, just like most of the other methods. Notice how simple this expression is:

$Y$ appears inside $3$ brackets $\implies$ $3$ statements in the big $\text{disjunction}$

I applied the $\text{involutarity}$ (if correct): $$\neg(\neg(P\implies R))\equiv\neg(P\land\neg R)$$

$((X\land Y)\lor (Y\land Z)\lor (W \land Y)) \implies Y\equiv \neg[(X\lor Z\lor W)\land Y\land\neg Y]\equiv\neg[(X\lor Z\lor W)\land 0]\equiv\neg 0\equiv 1\leftarrow\text{tautology}\;\blacksquare$

Answer 3

There a some provers for Fitch proofs in propositional logic:

1. Minlog from Slaney John Slaney: https://users.cecs.anu.edu.au/~jks/software/ it is a prover in minimal logic and, as option, in intuitionistic logic too. Here is the output from minlog:

 SEQUENT 1:  ((x & y) V (y & z) V (w & y)) -> y
 |- (((x & y) V (y & z)) V (w & y)) -> y

 | ((x & y) V (y & z)) V (w & y)   ASSUMPTION
 |  | (x & y) V (y & z)   ASSUMPTION
 |  |  | x & y   ASSUMPTION
 |  |  | x   &E
 |  |  | y   &E
 |  | 
 |  |  | y & z   ASSUMPTION
 |  |  | y   &E
 |  |  | z   &E
 |  | y   vE
 | 
 |  | w & y   ASSUMPTION
 |  | w   &E
 |  | y   &E
 | y   vE
(((x & y) V (y & z)) V (w & y)) -> y   arrow_I

2. Michel Levy's prover: http://teachinglogic.univ-grenoble-alpes.fr/DN/ here is its output:

1    assume x & y + y & z + w & y.
2      assume x & y + y & z.
3        assume x & y.
4          y.                                              &E2 3
5        therefore x & y => y.                             =>I 3,4
6        assume y & z.
7          y.                                              &E1 6
8        therefore y & z => y.                             =>I 6,7
9        y.                                                +E 2,5,8
10     therefore x & y + y & z => y.                       =>I 2,9
11     assume w & y.
12       y.                                                &E2 11
13     therefore w & y => y.                               =>I 11,12
14     y.                                                  +E 1,10,13
15   therefore x & y + y & z + w & y => y.                 =>I 1,14

3. Last, FLiP is a very nice proof checker written by Jonathan Jacky in Python and also available here. With FLiP-1.2,the command

python -i -m flip.logic.fol_session

import that rules that are defined by Richard Kaye in The Mathematics of Logic and the usual disjunction elimination rule is not defined, but replaced by a disjunction elimination right and a disjunction elimination left. If I am not mistaken, the classical rule of double negation elimination seems necessary to prove some theorems with Kaye's rules implemented in FLiP (see Kaye's book, p. 72). For example, in FLiP this theorem of this post is proved as follows (where p,q,r,e replace respectively x,y,z,w):

|((p & q) v (q & r)) v (e & q)  (1)  Assumption
||~q                      (2)  Assumption
|||e & q                  (3)  Assumption
|||q                      (4)  And-Elimination (Left) (3)
|||F                      (5)  Contradiction (4) (2)
||~(e & q)                (6)  Reductio Ad Absurdum (3) (5)
||(p & q) v (q & r)       (7)  Or-Elimination (Right) (1) (6)
|||q & r                  (8)  Assumption
|||q                      (9)  And-Elimination (Right) (8)
|||F                     (10)  Contradiction (9) (2)
||~(q & r)               (11)  Reductio Ad Absurdum (8) (10)
||p & q                  (12)  Or-Elimination (Right) (7) (11)
||q                      (13)  And-Elimination (Left) (12)
||F                      (14)  Contradiction (13) (2)
|~~q                     (15)  Reductio Ad Absurdum (2) (14)
|q                       (16)  Not-Elimination (15)
(((p & q) v (q & r)) v (e & q)) -> q (17)  Implication-Introduction (1) (16)