Advanced Symbolic Logic

Advanced Symbolic Logic Homework set # 8

Page 147, #1 {a, b, c}

Fa ® p .q. Fb® p .q. Fc ® p Fa.Fb.Fc. ® p

Fa ®p . Fb ® p . Fc ® p Fa q Fb q Fc. ® p

Page 154 # 4

"x$y(Fx®Gy.«Hy)

"x$y(Fx®Gy.Hy.q.-(Fx®Gy).-Hy) eliminate biconditional in favor of alternation

"x ($y (Fx®Gy.Hy).q. $y(-(Fx®Gy).-Hy)) distribute per passage rule 2

"x ($y (-FxqGy.Hy).q. $y(-(-FxqGy).-Hy)) eliminate the conditionals

"x ($y (-Fx.Hy.q.Gy.Hy).q. $y(Fx.-Gy.-Hy)) DeMorgan and distribute

"x (-Fx.$yHy.q.$y(Gy.Hy).q .Fx. $y (-Gy.-Hy)) distribute per passage rules 1 and 2

Now we have a partially purified formula in ANF, but since universal quantification does not distribute across alternation, we need to convert to CNF to finish the purification. The formula we have has the form qq r q ps. Dualize, distribute, simplify, dualize to get the CNF equivalent. qq . r . p q s ….. pqr q rs q qrs .…p q q q r . q r qs . q q r qs which is equivalent in our original to

"x(Fx q $yHy q $y(GyHy) : -Fx q $y(GyHy) q $y(-Gy-Hy) : $yHy q $y(GyHy) q $y (-Gy-Hy))

"x(Fx q $yHy q $y(GyHy)) : "x(-Fx q $y(GyHy) q $y(-Gy-Hy)) : $yHy q $y(GyHy) q $y (-Gy-Hy))

"xFx q $yHy q $y(GyHy) : "x-Fx q $y(GyHy) q $y(-Gy-Hy) : $yHy q $y(GyHy) q $y (-Gy-Hy))

Page 154 # 2, put '$xFx « $xGx. ® $xHx' into prenex form.

$xFx « $yGy. ® $zHz relettter to avoid collisions

$xFx ® $yGy.$yGy ® $xFx. ® $zHz eliminate the biconditional

$xFx ® $yGy.$sGs ® $tFt. ® $zHz relettter to avoid collisions

"x(Fx ® $yGy).$sGs ® $tFt. ® $zHz curios twist on $x

"x(Fx ® $yGy.$sGs ® $tFt. ® $zHz No curious twist expanding across conjunction

$x[Fx ® $yGy.$sGs ® $tFt. ® $zHz] Curious twist expanding the antecedent

$x[$y(Fx ® Gy).$sGs ® $tFt. ® $zHz]

$x[$y(Fx ® Gy.$sGs ® $tFt). ® $zHz]

$x"y[Fx ® Gy.$sGs ® $tFt. ® $zHz] Curious twist expanding the antecedent

$x"y[Fx ® Gy."s(Gs ® $tFt). ® $zHz] Curious twist

$x"y["s(Fx ® Gy.Gs ® $tFt). ® $zHz]

$x"y$s[Fx ® Gy.Gs ® $tFt. ® $zHz] Curious twist

$x"y$s[Fx ® Gy.$t(Gs ® Ft). ® $zHz]

$x"y$s[$t(Fx ® Gy.Gs ® Ft). ® $zHz]

$x"y$s"t[Fx ® Gy.Gs ® Ft. ® $zHz] Curious twist

$x"y$s"t$z[Fx ® Gy.Gs ® Ft. ® Hz] prenex form

Put 'Fx «."xGx q$xHx' into prenex form

Fx «."yGy q$zHz

Fx ®."yGy q$zHz: "yGy q $zHz. ®Fx

Fx ®."yGy q$zHz: "sGs q $tzHt. ®Fx

"y$z(Fx ®.Gy qHz): $s"t(Gs q Ht. ®Fx )

"y$z$s"t(Fx ®.Gy qHz: Gs q Ht. ®Fx) prenex form