8.4.1

8.4.5 (b)

 PD+ : 845B                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     ¬(Ex)¬Gx v ¬Fa                            | |
| PREMISE               |  2|     ¬Gb -> Fa                                 | |
| PREMISE               |  3|     ¬Gb                                       | |
| ->E2,3                |  4|     Fa                                        | |
| DN4                   |  5|     ¬¬Fa                                      | |
| DS1,5                 |  6|     ¬(Ex)¬Gx                                  | |
| EIx/b3                |  7|     (Ex)¬Gx                                   | |
+-----------------------------------------------------------------------------+

No (more) errors


Since the test is inconsistent, ¬Gb is derivable from the given set. 

8.4.6 (j)

 PD+ : 846J                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     (Ex)Fx -> (Ax)(Gx v (Ey)Hyx)              | |
| PREMISE               |  2|     (Ax)Fx & (Ax)(¬Hxa v Gc)                  | |
| &EL2                  |  3|     (Ax)Fx                                    | |
| AEa/x3                |  4|     Fa                                        | |
| EIx/a4                |  5|     (Ex)Fx                                    | |
| ->E1,5                |  6|     (Ax)(Gx v (Ey)Hyx)                        | |
| AEa/x6                |  7|     Ga v (Ey)Hya                              | |
| ASSM                  |  8|+----Ga                                        | |
| EIx/a8                |  9|+----(Ex)Gx                                    | |
| ASSM                  | 10|+----(Ey)Hya                                   | |
| ASSM                  | 11||+---Hda                                       | |
| &ER2                  | 12|||   (Ax)(¬Hxa v Gc)                           | |
| AEd/x 12              | 13|||   ¬Hda v Gc                                 | |
| DN11                  | 14|||   ¬¬Hda                                     | |
| DS 13,14              | 15|||   Gc                                        | |
| EIx/c15               | 16||+---(Ex)Gx                                    | |
| EEd/y10,11-16         | 17|+----(Ex)Gx                                    | |
| vE7,8-9,10-17         | 18|     (Ex)Gx                                    | |
+-----------------------------------------------------------------------------+

No (more) errors

8.4.7(h)

 PD+ : 847H                                                                    
+-----------------------------------------------------------------------------+
| PRE                   |  1|     (Ax)(P -> Fx)                             | |
| Aea/x1                |  2|     P -> Fa                                   | |
| assm                  |  3|+----P                                         | |
| ->e2,3                |  4||    Fa                                        | |
| Aix/a4                |  5|+----(Ax)Fx                                    | |
| ->i3-5                |  6|     P -> (Ax)Fx                               | |
|                       |  7|                                               | |
| pre                   |  8|     P -> (Ax)Fx                               | |
| assm                  |  9|+----P                                         | |
| ->e 8, 9              | 10||    (Ax)Fx                                    | |
| Aeb/x10               | 11|+----Fb                                        | |
| ->i 9-11              | 12|     P -> Fb                                   | |
| Aix/b12               | 13|     (Ax)(P -> Fx)                             | |
+-----------------------------------------------------------------------------+

No (more) errors

8.4.5 (b)

 PD+ : 845B                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     ¬(Ex)¬Gx v ¬Fa                            | |
| PREMISE               |  2|     ¬Gb -> Fa                                 | |
| PREMISE               |  3|     ¬Gb                                       | |
| ->E2,3                |  4|     Fa                                        | |
| DN4                   |  5|     ¬¬Fa                                      | |
| DS1,5                 |  6|     ¬(Ex)¬Gx                                  | |
| EIx/b3                |  7|     (Ex)¬Gx                                   | |
+-----------------------------------------------------------------------------+

No (more) errors

8.5.4 (d)



 PD+ : 854D                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     Lm -> ¬(Ex)Rmx                            | |
| PREMISE               |  2|     (Aw)(Ax)(Rwx & Lw) & Sam                  | |
| &el2                  |  3|     (Aw)(Ax)(Rwx & Lw)                        | |
| Aem/w3                |  4|     (Ax)(Rmx & Lm)                            | |
| Aeb/x4                |  5|     Rmb & Lm                                  | |
| &el5                  |  6|     Rmb                                       | |
| &er5                  |  7|     Lm                                        | |
| ->e1,7                |  8|     ¬(Ex)Rmx                                  | |
| Eix/b6                |  9|     (Ex)Rmx                                   | |
+-----------------------------------------------------------------------------+

No (more) errors

8.5.6 (d)


 PD+ : 856B                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     (Ex)Rx                                    | |
| PREMISE               |  2|     (Ay)(Ry = Say)                            | |
| ASSME                 |  3|+----Rb                                        | |
| AEb/y2                |  4||    Rb = Sab                                  | |
| =E3,4                 |  5||    Sab                                       | |
| EIw/b5                |  6|+----(Ew)Saw                                   | |
| EEb/x1,3-6            |  7|     (Ew)Saw                                   | |
+-----------------------------------------------------------------------------+

No (more) errors

8.5.7 (b)




 PD+ : 857B                                                                    
+-----------------------------------------------------------------------------+
| PREMISE               |  1|     (Ax)Fx -> P                               | |
| ASSUME                |  2|+----(Ax)Fx                                    | |
| R2                    |  3|+----(Ax)Fx                                    | |
| ->I2-3                |  4|     (Ax)Fx -> (Ax)Fx                          | |
| IM4                   |  5|     ¬(Ax)Fx v (Ax)Fx                          | |
| ASSME                 |  6|+----¬(Ax)Fx                                   | |
| QN6                   |  7||    (Ex)¬Fx                                   | |
| ASSME                 |  8||+---¬Fa                                       | |
| vIR8                  |  9|||   ¬Fa v P                                   | |
| IM9                   | 10|||   Fa -> P                                   | |
| EIx/a10               | 11||+---(Ex)(Fx -> P)                             | |
| EEa/x7,8-11           | 12|+----(Ex)(Fx -> P)                             | |
| ASSME                 | 13|+----(Ax)Fx                                    | |
| ->E1,13               | 14||    P                                         | |
| vIL14                 | 15||    ¬Fa v P                                   | |
| IM15                  | 16||    Fa -> P                                   | |
| EIx/a16               | 17|+----(Ex)(Fx -> P)                             | |
| vE5,6-12,13-17        | 18|     (Ex)(Fx -> P)                             | |
|                       | 19|                                               | |
| PREMISE               | 20|     (Ex)(Fx -> P)                             | |
| ASSME                 | 21|+----(Ax)Fx                                    | |
| ASSME                 | 22||+---Fa -> P                                   | |
| AEa/x21               | 23|||   Fa                                        | |
| ->E22,23              | 24||+---P                                         | |
| EEa/x20,22-24         | 25|+----P                                         | |
| ->I21-25              | 26|     (Ax)Fx -> P                               | |
+-----------------------------------------------------------------------------+

No (more) errors


8.6.4
Solution: Theory(\emptyset) is the set of all tautologies. It is easy to see that the set {(Ax)Fx,¬Fa} is inconsistent. Therefore, Theory({(Ax)Fx, ¬Fa}) is the set of all PL sentences.