17 Reglas derivadas en el sistema de Gentzen

Teorema 17.1 (Modus tollens, MT).

{A→B,¬⁢B}⊢¬⁢A\displaystyle\{A\rightarrow B,\neg B\}\vdash\neg A

Demostración.

A,B\displaystyle A,B formulas cualesquiera.

Cons: ¬⁢A\displaystyle\neg A

  1. 1.
    ​

    A→B\displaystyle A\rightarrow B Pr

  2. 2.
    ​

    ¬⁢B\displaystyle\neg B Pr

3.​A\displaystyle A Pr aux 4.​BE→3,1\displaystyle B\quad E\rightarrow 3,1 5.​B∧¬I∧4,2\displaystyle B\wedge\neg\quad I\wedge 4,2

  1. 6.
    ​

    A→B∧¬⁢BI→(3−5)\displaystyle A\rightarrow B\wedge\neg B\quad I\rightarrow(3-5)

  2. 7.
    ​

    ¬⁢AI⁢¬⁢,6\displaystyle\neg A\quad I\neg,6

∎

Teorema 17.2 (Teorema de la identidad, TI).
{A}⊢A\displaystyle\{A\}\vdash A

Usando el Teorema de deduccion puede reformularse como

⊢A→A\displaystyle\vdash A\rightarrow A
Demostración.
  1. 1.
    ​

    A\displaystyle A Pr

2.​¬⁢A\displaystyle\neg A Pr aux 3.​A∧¬⁢AI∧,2,1\displaystyle A\wedge\neg A\quad I\wedge,2,1

  1. 4.
    ​

    ¬⁢A→A∧¬⁢AI→(2−3)\displaystyle\neg A\rightarrow A\wedge\neg A\quad I\rightarrow(2-3)

  2. 5.
    ​

    ¬⁢¬⁢AI⁢¬⁢,4\displaystyle\neg\neg A\quad I\neg,4

  3. 6.
    ​

    AE⁢¬⁢,5\displaystyle A\quad E\neg,5

∎

Teorema 17.3 (Excontradictione quodlibet, EQ).
{A∧¬⁢A}⊢B\displaystyle\{A\wedge\neg A\}\vdash B
Demostración.

  1. 1.
    ​

    A∧¬⁢A\displaystyle A\wedge\neg A Pr

2.​¬⁢B\displaystyle\neg B Pr aux 3.​A∧¬⁢A\displaystyle A\wedge\neg A

  1. 4.
    ​

    ¬⁢B→A∧¬⁢AI→(2,−3)\displaystyle\neg B\to A\wedge\neg A\quad I\to(2,-3)

  2. 5.
    ​

    ¬⁢¬⁢BI⁢¬⁢,4\displaystyle\neg\neg B\quad I\neg,4

  3. 6.
    ​

    B\displaystyle B\quad

∎

Teorema 17.4 (Tollendo ponens, TP).
{A∨B,¬⁢A}⊢B\displaystyle\{A\vee B,\neg A\}\vdash B
Demostración.
  1. 1.
    ​

    A∨B\displaystyle A\vee B Pr

  2. 2.
    ​

    ¬⁢A\displaystyle\neg A Pr

3.​A\displaystyle A Pr aux 4.​A∧¬⁢AI∧,1,2\displaystyle A\wedge\neg A\quad I\wedge,1,2 5.​BE⁢Q⁢,4\displaystyle B\quad EQ,4

  1. 6.
    ​

    A→BI→(3−6)\displaystyle A\to B\quad I\to(3-6)

7.​B\displaystyle B Pr aux

  1. 8.
    ​

    B→BI→(7)\displaystyle B\to B\quad I\to(7)

  2. 9.
    ​

    BE∨,1,6,8\displaystyle B\quad E\vee,1,6,8

∎

Ejemplo.

Uso de reglas derivadas en una demostracion:

{p→t∨r,p∨q,q→t,¬⁢t∧s}⊢r∧s\displaystyle\{p\to t\vee r,p\vee q,q\to t,\neg t\wedge s\}\vdash r\wedge s

Cons: r∧s\displaystyle r\wedge s

  1. 1.
    ​

    p→t∨r\displaystyle p\to t\vee r Pr

  2. 2.
    ​

    p∨q\displaystyle p\vee q Pr

  3. 3.
    ​

    q→t\displaystyle q\to t Pr

  4. 4.
    ​

    ¬⁢t∧s\displaystyle\neg t\wedge s Pr

  5. 5.
    ​

    ¬⁢tE∧,4\displaystyle\neg t\quad E\wedge,4

  6. 6.
    ​

    ¬⁢qM⁢T⁢,5,3\displaystyle\neg q\quad MT,5,3

  7. 7.
    ​

    pT⁢P⁢,6,2\displaystyle p\quad TP,6,2

  8. 8.
    ​

    t∨rE→,7,1\displaystyle t\vee r\quad E\to,7,1

  9. 9.
    ​

    rT⁢P⁢,8,5\displaystyle r\quad TP,8,5

  10. 10.
    ​

    sE∧,4\displaystyle s\quad E\wedge,4

  11. 11.
    ​

    r∧sI∧,9,10\displaystyle r\wedge s\quad I\wedge,9,10

Teorema 17.5 (Doble negacion, DN).
{A}⊢¬⁢¬⁢A\displaystyle\{A\}\vdash\neg\neg A
Teorema 17.6 (Contraposicion, CP).

Son dos reglas que establecen la “equivalencia” entre dos formulas en este sistema formal.

{A→B}⊢¬⁢B→¬⁢A\displaystyle\{A\to B\}\vdash\neg B\to\neg A
{¬⁢B→¬⁢A}⊢A→B\displaystyle\{\neg B\to\neg A\}\vdash A\to B
Demostración.
  1. 1.
    ​

    A→B\displaystyle A\to B Pr

2.​¬⁢B\displaystyle\neg B Pr aux 3.​¬⁢AM⁢T⁢,1,2\displaystyle\neg A\quad MT,1,2

  1. 4.
    ​

    ¬⁢B→¬⁢AI→(2−3)\displaystyle\neg B\to\neg A\quad I\to(2-3)

  1. 1.
    ​

    ¬⁢B→¬⁢A\displaystyle\neg B\to\neg A

2. ∎

Teorema 17.7 (Leyes de De Morgan, DM).

Cuatro reglas:

{¬⁡(A∨B)}⊢¬⁢A∧¬⁢B\displaystyle\{\neg(A\vee B)\}\vdash\neg A\wedge\neg B
{¬⁢A∧¬⁢B}⊢¬⁡(A∨B)\displaystyle\{\neg A\wedge\neg B\}\vdash\neg(A\vee B)
{¬⁡(A∧B)}⊢¬⁢A∨¬⁢B\displaystyle\{\neg(A\wedge B)\}\vdash\neg A\vee\neg B
{¬⁢A∨¬⁢B}⊢¬⁡(A∧B)\displaystyle\{\neg A\vee\neg B\}\vdash\neg(A\wedge B)
Demostración.

DM1:

  1. 1.
    ​

    ¬⁡(A∨B)\displaystyle\neg(A\vee B) Pr

2.​A\displaystyle A Pr aux 3.​A∨BI∨,2\displaystyle A\vee B\quad I\vee,2 4.​(A∨B)∧¬⁡(A∨B)I∧,1,3\displaystyle(A\vee B)\wedge\neg(A\vee B)\quad I\wedge,1,3

  1. 5.
    ​

    A→(A∨B)∧¬⁡(A∨B)I→(2−4)\displaystyle A\to(A\vee B)\wedge\neg(A\vee B)\quad I\to(2-4)

  2. 6.
    ​

    ¬⁢AI⁢¬⁢,5\displaystyle\neg A\quad I\neg,5

6.​B\displaystyle B Pr aux 7.​A∨BI∨,6\displaystyle A\vee B\quad I\vee,6 8.​(A∨B)∧¬⁡(A∨B)I∧,1,7\displaystyle(A\vee B)\wedge\neg(A\vee B)\quad I\wedge,1,7

  1. 9.
    ​

    ¬BI→,I¬(6−8)\displaystyle\neg BI\to,I\neg(6-8)

  2. 10.
    ​

    ¬⁢A∧¬⁢BI∧,5,9\displaystyle\neg A\wedge\neg B\quad I\wedge,5,9

DM2:

  1. 1.
    ​

    ¬⁢A∧¬⁢B\displaystyle\neg A\wedge\neg B Pr

2.​A∨B\displaystyle A\vee B Pr aux 3.​¬⁢AE∧,1\displaystyle\neg A\quad E\wedge,1 4.​BT⁢P⁢,2,3\displaystyle B\quad TP,2,3 5.​¬⁢BE∧,1\displaystyle\neg B\quad E\wedge,1 6.​B∧¬⁢BI∧,4,5\displaystyle B\wedge\neg B\quad I\wedge,4,5

  1. 7.
    ​

    ¬(A∨B)I→,I¬(2−6)\displaystyle\neg(A\vee B)\quad I\to,I\neg(2-6)

DM3:

  1. 1.
    ​

    ¬⁡(A∧B)\displaystyle\neg(A\wedge B) Pr

2.​¬⁡(¬⁢A∨¬⁢B)\displaystyle\neg(\neg A\vee\neg B) Pr aux 3.​¬⁢¬⁢A∧¬⁢¬⁢BD⁢M⁢,1,2\displaystyle\neg\neg A\wedge\neg\neg B\quad DM,1,2 4. 4.​¬⁢¬⁢AE∧,3\displaystyle\neg\neg A\quad E\wedge,3 5.​AE⁢¬⁢,4\displaystyle A\quad E\neg,4 6.​¬⁢¬⁢BE∧,3\displaystyle\neg\neg B\quad E\wedge,3 7.​BE⁢¬⁢,6\displaystyle B\quad E\neg,6 8.​A∧BI∧,5,7\displaystyle A\wedge B\quad I\wedge,5,7 9.​(A∧B)∧¬⁡(A∧B)I∧,1,8\displaystyle(A\wedge B)\wedge\neg(A\wedge B)\quad I\wedge,1,8

  1. 10.
    ​

    ¬A∨¬BI→,I¬,E¬(2−9)\displaystyle\neg A\vee\neg B\quad I\to,I\neg,E\neg(2-9)

DM4:

  1. 1.
    ​

    ¬⁢A∨¬⁢B\displaystyle\neg A\vee\neg B Pr

2.​A∧B\displaystyle A\wedge B Pr aux 3.​AE∧,2\displaystyle A\quad E\wedge,2 4.​¬⁢BT⁢P⁢,3,1\displaystyle\neg B\quad TP,3,1 5.​BE∧,2\displaystyle B\quad E\wedge,2 6.​B∧¬⁢BI∧,5,4\displaystyle B\wedge\neg B\quad I\wedge,5,4

  1. 7.
    ​

    ¬(A∧B)I→,I¬(2−6)\displaystyle\neg(A\wedge B)\quad I\to,I\neg(2-6)

∎

Teorema 17.8 (Interdefinicion).

Cuatro reglas:

{A→B}⊢¬⁢A∨B\displaystyle\{A\to B\}\vdash\neg A\vee B