GR2

1. 1. ~ x^z r^~x

2. (~tvz) -> r

3. ~x ROK1

4. z ROK1

5. ~tvz RDA4

6. r RO2,5

7. r^~x RDK3,6

2.1. ~(~pv-q) (tvr)^q

2.((p^q)vs) ->r

3. ~~p^~~q deM1

4.p^q RPN3

5. q ROK4

6. (p^q)vs RDA 4

7.r RO2,6

8. tvr RDA7

9. (tvr)^q RDK 5,8

3.1. ~~(p <->r) (q^s)vr

2. p

3. (p<->r) RPN1

4. (p->r) ^ (r->p) RR3

5. p->r ROK4

6. r RO2,5

7. (s^q)vr RDA6

4.1. ~t ->q ~s->t

2. ~t ->(q->s)

3. ~s zdw

4. ~t zdn

5. q RO1,4

6. q->s RO 2,4

7. s RO 5,6

8. s^~s RDK 3,7

9. t RA 4-8

10. ~s -> t RDW 3-9

5.1 (p->q) ^ (r->s) (p^r)->(s^q)

2. (p->q) ROK1

3. (r->s) ROK1

4. (p^r) zdw

5. p ROK4

6. r ROK4

7. s RO 3,6

8. q RO 2,5

9. (s^q) RDK 7,8

10. (p^r)->(s^q) RDW 4-9

6.1. p-> ~(qvz) z->~p

2. z zdw

3. (qvz) RDA2

4. p zdn

5. ~(qvz) RO1,4

6. (qvz) ^ ~(qvz) RDK 3,5

7. ~p RA 4-6

8. z->~p RDW 2-7

7.1 ~(~r^q) rvt

2. ~r->p

3. (~r^p)->p

4. ~(rvt) zdn

5. ~r ^ ~t deM4

6.~r ROK5

7. p RO2,6

8. ~r^p RDK 6,7

9. q RO 3,8

10. ~r^q RDK 6,9

11. (~r^q) ^ ~(~r^q) RDK1,10

12. tvt RA 4-11

8.1 ((tvz)^q)->p ~rvp

2. r-> ((q^t)^z)

3.~(~rvp) zdn

4. r^~p deM3

5. r ROK4

6. ~p ROK4

7. ((q^t)^z) RO5,2

8. (q^(t^z)) RŁ7

9. ((t^z)^q) RP8

10.p RO1,9

11. ~p^p RDK6,10

12. ~rvp RA 3-11

9.1. p^q (sv~r)^q

2. q^t

3. (p^t)-> ~r

4. p ROK1

5. q ROK1

6. t ROK2

7. p^t RDK 4,6

8. ~r RO 3,7

9. sv~r RDA8

10. (sv~r)^q RDK5,9

GR1

1.1 p^q ~q^p

2. p->~q

3. p ROK1

4. q ROK1

5. ~q RO2,3

6. ~q^p RDK 3,5

2.1 (~p->q)->~(rvs) (~p->q)->(~rvq)

2. (~p>q) zdw

3. ~(rvs) RO1,2

4. ~r^~s deM3

5. ~r ROK4

6 ~rvq RDA 5

7. (~p->q)->(~rvq) RDW 2-6

3.1. (qvr)->s ~s->~q

2. ~s zdw

3. q zdn

4. qvr RDA3

5. s RO1,4

6. ~s^s RDK2,5

7. ~q RA 3-6

8. ~s->~q RDW2,7

4.1. (p^~q) r^~q

2. (pvz)->z

3. (zvt)->r

4. p ROK1

5. ~q ROK1

6. pvz RDA4

7. z RO 2,6

8. zvt RDA7

9. r RO3,8

10. r^ ~q RDK 5,9

5.1 ~p q

2. ~(q^p)->q

3. (~qv~p)->q deM2

4. ~qv~p RDA

5. q RO 3,4

6.1. (pv(qvr))->(s->r) (x^s)->r

2. x ->(qv(rvp))

3. x^s zdw

4. x ROK3

5. s ROK3

6. (qv(rvp)) RO2,4

7. ((qvr)vp) RŁ6

8. pv(qvr) RP7

9. s->r RO 1,8

10. r RO 5,9

11. (x^s)->r RDW3-10

7.1 ~(zvr) ~(~pvz)

2. ~r->p

3. ~(~pvz) zdw

4. ~~p^~z deM3

5. p^~z RPN4

6. ~z ROK7

7. ~z^~r deM1

8. ~r ROK7

9. p RO 2,8

10. p^~z RDK 6,9

11. ~(~pvz) RDW 3-10

9.1 p->q ~pvx

2. ~(p^q)

3.~(~pvx) zdn

4. ~~p^~x deM3

5. p^~x RPN4

6. p ROK5

7. q RO 1,6

8. p^q RDK 6,7

9. (p^q) ^ ~(p^q) RDK2,8

10. ~pvx RA3-9

1

---