Symbolizations
1. Ca & (Wa -> ~Na)
2. (Wa -> Pa) & ~(Pa -> Wa)
3. (Pa -> ~Na) -> ~Wa
4. $x(Cx & Wx) -> ~Na
5. $x((Cx & ~Nx) & @y(Qy -> Axy))
6. @x(Cx -> (Wx -> Px)
7. @x(Cx & @y(Qy -> Axy) -> ~Nx)
8. @x(Cx -> (Wx <-> (@y(Qy -> Axy)))
Indirect Truth Tables
9. Invalid. P: T; Q: F; R: F; S: F
10. Valid
11. Valid
12. Invalid. P: T; Q: F; R: F; S: F
Expansions
13. ((Ha & Fa) & ~Ga) v ((Hb & Fb) & ~Gb) True
14. P <-> (Ha -> ~Ga) & (Hb -> ~Gb) False
15. Ha & Hb -> (Fa v Fb) & (Ga v Gb) True
16. (Ga & (Ha & Hb)) v (Gb & (Ha & Hb)) True
Countermodels
17. U: {a,b} F: {a} G: { }
18. U: {a,b} F: {a} G: {a,b} H: {a}
19. U: {a} B: { } C: { } D: {a}
20. U: {a,b,c} M: {b} N: {a} P:{a,c}
Proofs
#21.
~S -> T & U, ~R -> ~(T v
U), (T <-> U) -> S & R |- S & R
Normally, we
prove a conjunction one conjunct at a time by RAA.
If you do the proof this way, it is not hard but it is very long.
1 (1) ~S->T&U
.A
2 (2)
~R->~(TvU) .A
3 (3) (T<->U)->S&R
.A
4 (4) ~S
.A
1,4 (5) T&U
.1,4 ->E
4 (6) ~Sv~R
.4 VI
4 (7) ~(S&R) .6
DM
3,4 (8) ~(T<->U)
.3,7 MTT
3,4 (9) ~T<->U
.8 NEG<->
1,4 (10) U
.5 &E
1,4 (11) T
.5 &E
1,3,4 (12) ~T
.9,10 BP
1,3 (13) S
.11,12 RAA(4)
14 (14) ~R
.A
2,14 (15) ~(TvU)
.2,14 ->E
2,14 (16) ~T&~U
.15 DM
2,14 (17) ~T
.16
&E
2,14 (18) ~U
.16 &E
14 (19) ~Sv~R
.14 VI
14 (20) ~(S&R)
.19 DM
3,14 (21) ~(T<->U)
.3,20 MTT
3,14 (22) ~T<->U
.21 NEG<->
2,3,14 (23) U
.17,22 BP
2,3 (24) R
.18,23 RAA(14)
1,2,3 (25) S&R
.13,24 &I
Here’s
a much shorter way to do the same sequent.
1 (1) ~S->T&U
.A
2 (2) ~R->~(TvU)
.A
3 (3) (T<->U)->S&R
.A
4 (4) ~(S&R)
.A
3,4 (5) ~(T<->U)
.3,4 MTT
3,4 (6) ~T<->U
.5 NEG<->
3,4 (7) ~T->U
.6 <->E
3,4 (8) TvU
.7 V->
2,3,4 (9) R
.2,8 MTT
3,4 (10) T<->~U
.5
NEG<->
3,4 (11) T->~U
.10 <->E
3,4 (12) ~(T&U)
.11 NEG->
1,3,4 (13) S
.1,12 MTT
1,2,3,4 (14) S&R
.9,13 &I
1,2,3 (15) S&R
.4,14 RAA(4)
#22.
~(@xFx -> $xBx), $x~Cx ->
$xBx, @x(Fx & Cx -> Da) |- Da
1 (1) ~(@xFx->$xBx)
.A
2 (2) $x~Cx->$xBx
.A
3 (3) @x(Fx&Cx->Da)
.A
1 (4) @xFx&~$xBx
.1 NEG->
1 (5) @xFx
.4 &E
1 (6) Fb
.5 @E
1 (7) ~$xBx
.4 &E
1,2 (8) ~$x~Cx
.2,7 MTT
1,2 (9) @xCx
.8
QE
1,2 (10) Cb
.9 @E
1,2 (11) Fb&Cb
.6,10 &I
3 (12) Fb&Cb->Da
.3 @E
1,2,3 (13) Da
.11,12 ->E
#23.
@x(Px -> $yMxy), @x~Px ->
@xFx |- $x~Fx -> $y$xMyx
1 (1) @x(Px->$yMxy)
.A
2 (2) @x~Px->@xFx
.A
3 (3) $x~Fx
.A [for ->I]
3 (4) ~@xFx
.3 QE
2,3 (5) ~@x~Px
.2,4 MTT
2,3 (6) $xPx
.5 QE
1 (7) Pa->$yMay
.1 @E
8 (8) Pa
.A [for $E on 6, a]
1,8 (9) $yMay
.7,8 ->E
10 (10) Mab
.A [for $E on 9, b]
10
(11) $xMax
.10 $I
10 (12) $y$xMyx
.11 $I
1,8 (13) $y$xMyx
.9,12 $E(10)
1,2,3 (14) $y$xMyx
.6,13 $E(8)
1,2 (15) $x~Fx->$y$xMyx
.14 ->I(3)
#24
(@xHx -> $xGx) -> ~$y(Fy v
$zTz), ~@xFx -> $xGx, @xHx -> $x~Fx
|- $x~Tx
1 (1) (@xHx->$xGx)->~$y(Fyv$zTz)
.A
2 (2) ~@xFx->$xGx
.A
3 (3) @xHx->$x~Fx
.A
4 (4) @xHx .A [for ->I]
Note that
our old strategies from sentential logic suggest that we assume this to prove
the antecedent of the antecedent of premise 1
3,4 (5) $x~Fx
.3,4 ->E
3,4 (6) ~@xFx
.5 QE
2,3,4 (7) $xGx
.2,6 ->E
2,3 (8) @xHx->$xGx
.7 ->I(4)
1,2,3 (9) ~$y(Fyv$zTz)
.1,8 ->E
1,2,3 (10) @y~(Fyv$zTz)
.9 QE
1,2,3 (11) ~(Fav$zTz)
.10 @E
1,2,3 (12) ~Fa&~$zTz
.11 DM
1,2,3 (13) ~$zTz
.12 &E
1,2,3 (14) @z~Tz
.13
QE
1,2,3 (15) ~Ta
.14 @E
1,2,3 (16) $x~Tx
.15 $I
Another
strategy for doing the same proof.
1 (1) (@xHx->$xGx)->~$y(Fyv$zTz)
.A
2 (2) ~@xFx->$xGx
.A
3 (3) @xHx->$x~Fx
.A
4 (4) Ta
.A [for RAA]
4 (5) $zTz
.4 $I
4 (6) Fav$zTz
.5 VI
4 (7) $y(Fyv$zTz)
.6 $I
1,4 (8) ~(@xHx->$xGx)
.1,7 MTT
1,4 (9) @xHx&~$xGx
.8 NEG->
1,4 (10) @xHx
.9 &E
1,3,4 (11) $x~Fx
.3,10 ->E
1,3,4 (12) ~@xFx
.11 QE
1,2,3,4 (13) $xGx
.2,12 ->E
1,4 (14) ~$xGx
.9 &E
1,2,3 (15) ~Ta
.13,14 RAA(4)
1,2,3 (16) $x~Tx
.15 $I
#25
@x(Hx -> Bx v ~Fx), @x$y(~Bx
& Fy)|-$x~Hx
Yes, this
one is a looping problem.
1 (1) @x(Hx->Bxv~Fx)
.A
2 (2) @x$y(~Bx&Fy)
.A
1 (3) Ha->Bav~Fa
.1 @E
2 (4) $y(~Ba&Fy)
.2 @E
5 (5) ~Ba&Fb
.A [for $E on 4]
2 (6) $y(~Bc&Fy)
.2 @E
7 (7) ~Bc&Fa
.A [for $E on 6]
8 (8) Ha
.A [for RAA]
1,8 (9) Bav~Fa
.3,8 ->E
5 (10) ~Ba
.5 &E
1,5,8 (11) ~Fa
.9,10 VE
7 (12) Fa
.7 &E
1,5,7 (13) ~Ha
.11,12 RAA(8)
1,5,7 (14) $x~Hx
.13 $I
1,2,7 (15) $x~Hx
.4,14 $E(5)
1,2 (16) $x~Hx
.6,15 $E(7)
You must discharge 5 before 7 here.