Predicate Logic Proof Method

1. ∀x(Rx→Sx)
2. ∃x(Rx&Tx)
1. Ra→Sa by 1UO
2. Ra&Ta by 2EO
3. Rx&Tx by 2EO
4. Ra&Tb by 2EO
1. ∃x(Fx&Gx)
2. ∀x(Gx→Hx)
1. Fa&Ga by 1EO
2. Ga→Ha by 2UO
3. Gx→Hx by 2UO
4. Ga→Hb by 2UO
1. ∃x(Mx&Nx)
2. ∀x(Sx→Tx)
1. ~∀x(Sx→Tx) by 1QE
2. Sa→Ta by 2UO
3. ~∃x(Mx&Nx) by 2QE
4. Ma&Na by 1EO
1. ~∀x(Fx→Gx)
2. ∃x~(Gx&Hx)
1. ~∃x(Fx→Gx) by 1QE
2. ~∃x(Gx&Hx) by 2QE
3. ∃x~(Fx→Gx) by 1QE
4. ~∀x(Gx&Hx) by 2QE
1. ∃x(Rx&Sx)
2. ~∀x(Sx→Tx)
1. Ra&Sa by 1EO
2. ~(Sa→Ta) by by 2UO
3. ∃x~(Sx→Tx) by 2QE
4. ∃x~(Sx&Tx) by 2QE
1. ~∃x(Fx&Gx)
2. ∀x(Gx→Hx)
1. ∀x~(Fx&Gx) by 1QE
2. ∀x~(Fx→Gx) by 1QE
3. ∀x(Fx→~Gx) by 1QE
4. Ga→Ha by 2UO
1. Ra&Sb
2. ∃x(Rx&Tx)
1. Ra&Ta by 2EO
2. Rc&Tc by 2EO
3. Rc&Td by 2EO
4. Rx&Tx by 2EO
1. Fa&Gb
2. ∃x~(FxvGx)
1. ~(FavGb) by 2EO
2. ~(FavGa) by 2EO
3. ~(FbvGb) by 2EO
4. ~(FcvGc) by 2EO
1. ∃x(Tx&Sx)
2. Ta→Wa
1. Ta&Sa by 1EO
2. Tb&Sb by 1EO
3. Ta&Sb by 1EO
4. Tx&Sx by 1EO
1. ∀x(Bx→Dx)
2. Ba&Ca
1. Ba→Da by 1UO
2. Bb→Db by 1UO
3. Bb→Dc by 1UO
4. Bx→Dx by 1UO
1. ∀x(Rx→(Tx&Wx))
2. Rb&Sb
1. Rc→(Tc&Wc) by 1UO
2. Ra→(Tb&Wc) by 1UO
3. Rc→(Td&We) by 1UO
4. Rb→(Tb&Wb) by 1UO
1. Mc
2. ∀x((MxvNx)→Rx)
1. (MavNa)→Ra by 2UO
2. (MdvNd)→Rc by 2UO
3. (McvNd)→Re by 2UO
4. (McvNc)→Rc by 2UO
1. ∀x(Bx→Dx)
2. ∃x(Dx&Ex)
3. ~∀x(Fx→Gx)
1. Ba→Da by 1UO
2. Da&Ea by 2EO
3. ∃x~(Fx→Gx) by 3QE
4. ∃x(Fx&~Gx) by 3QE
1. ~∀x(Mx→Nx)
2. ∃x(Rx&Sx)
3. ~~∀x(Rx→Wx)
1. ∃x~(Mx→Nx) by 1QE
2. Ra&Sa by 2EO
3. ~∃x~(Rx→Wx) by 3QE
4. ∀x(Rx→Wx) by 3DN
1. ~~∃x(Hx&Gx)
2. ∃x(Fx&Gx)
3. Fa→~Ha
1. ∃x(Hx&Gx) by 1DN
2. Fa&Ga by 2EO
3. Fb&Gb by 2EO
4. Fa&Gb by 2EO
1. ∃x(Mx&Nx)
2. ∀x(Rx→Sx)
3. ~∃x(RxvSx)
1. Ma&Na by 1EO
2. Ra→Sa by 2UO
3. ∀x~(RxvSx) by 3QE
4. ~(RavSa) by 3EO
1. ∀x(Dx→Fx)
2. ~∀x(Gx→Hx)
3. ∃x(Hx&Dx)
1. Da→Fa by 1UO
2. ∃x~(Gx→Hx) by 2QE
3. Ha&Da by 3EO
4. Ha&Db by 3EO
1. ∀x(Bx→Cx)
2. ~∃x(Mx&Nx)
3. Ba&Da
1. Ba→Ca by 1UO
2. Bb→Cb by 1UO
3. ∀x~(Mx&Nx) by 2QE
4. ~(Mb&Nb) by 2EO
1. ∀x~~(Bx→Cx)
2. ~∃x(Cx&Dx)
3. ∀xBx
1. ∀x(Bx→Cx) by 1DN
2. ~~(Ba→Ca) by 1UO
3. ∀x~(Cx&Dx) by 2QE
4. Ba by 3UO
1. ∃x(HxvJx)
2. ~∃x(GxvHx)
3. ~(GavFa)
1. HavJa by 1EO
2. HbvJb by 1EO
3. ∀x~(GxvHx) by 2QE
4. ~Ga&~Fa by 3DM
1. ∀xHx
2. ∀x(Gxv~Hx)
3. ∃x~Gx
1. Ha by 1UO
2. Gav~Ha by 2UO
3. ~Ga by 3EO
4. ~∀xGx by 3QE

Predicate Logic Proof Method

Imagine that these are the first lines of a proof and that the conclusion is NOT quantified. According to the method, what would you put on the next line? Choose the best answer.