17 Reglas derivadas en el sistema de Gentzen

Theorem 17.1 (Modus tollens, MT).

{A→B,¬B}⊢¬A\left\{A\rightarrow B,\neg B\right\}\vdash\neg A

Proof 17.2.

A,BA,B formulas cualesquiera.

Cons: ¬A\neg A

  1. 1.
    ​

    A→BA\rightarrow B Pr

  2. 2.
    ​

    ¬B\neg B Pr

[resume] 1.​AA Pr aux 2.​BE→3,1B\quad E\rightarrow 3,1 3.​B∧¬I∧4,2B\wedge\neg\quad I\wedge 4,2

  1. [resume]

  2. 6.
    ​

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

  3. 7.
    ​

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

Theorem 17.3 (Teorema de la identidad, TI).
{A}⊢A\left\{A\right\}\vdash A

Usando el Teorema de deduccion puede reformularse como

⊢A→A\vdash A\rightarrow A
Proof 17.4.
  1. 1.
    ​

    AA Pr

[resume] 1.​¬A\neg A Pr aux 2.​A∧¬AI∧,2,1A\wedge\neg A\quad I\wedge,2,1

  1. 4.
    ​

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

  2. 5.
    ​

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

  3. 6.
    ​

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

Theorem 17.5 (Excontradictione quodlibet, EQ).
{A∧¬A}⊢B\left\{A\wedge\neg A\right\}\vdash B
Proof 17.6.
  1. 1.
    ​

    A∧¬AA\wedge\neg A Pr

[resume] 1.​¬B\neg B Pr aux 2.​A∧¬AA\wedge\neg A

  1. 4.
    ​

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

  2. 5.
    ​

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

  3. 6.
    ​

    BB\quad

Theorem 17.7 (Tollendo ponens, TP).
{A∨B,¬A}⊢B\left\{A\vee B,\neg A\right\}\vdash B
Proof 17.8.
  1. 1.
    ​

    A∨BA\vee B Pr

  2. 2.
    ​

    ¬A\neg A Pr

[resume] 1.​AA Pr aux 2.​A∧¬AI∧,1,2A\wedge\neg A\quad I\wedge,1,2 3.​BE⁢Q,4B\quad EQ,4

  1. 6.
    ​

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

7.​BB Pr aux

  1. 8.
    ​

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

  2. 9.
    ​

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

Example 17.9.

Uso de reglas derivadas en una demostracion:

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

Cons: r∧sr\wedge s

  1. 1.
    ​

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

  2. 2.
    ​

    p∨qp\vee q Pr

  3. 3.
    ​

    q→tq\to t Pr

  4. 4.
    ​

    ¬t∧s\neg t\wedge s Pr

  5. 5.
    ​

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

  6. 6.
    ​

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

  7. 7.
    ​

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

  8. 8.
    ​

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

  9. 9.
    ​

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

  10. 10.
    ​

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

  11. 11.
    ​

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

Theorem 17.10 (Doble negacion, DN).
{A}⊢¬¬A\left\{A\right\}\vdash\neg\neg A
Theorem 17.11 (Contraposicion, CP).

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

{A→B}⊢¬B→¬A\left\{A\to B\right\}\vdash\neg B\to\neg A
{¬B→¬A}⊢A→B\left\{\neg B\to\neg A\right\}\vdash A\to B
Proof 17.12.
  1. 1.
    ​

    A→BA\to B Pr

[resume] 1.​¬B\neg B Pr aux 2.​¬AM⁢T,1,2\neg A\quad MT,1,2

  1. 4.
    ​

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

  1. 1.
    ​

    ¬B→¬A\neg B\to\neg A

[resume] 1.

Theorem 17.13 (Leyes de De Morgan, DM).

Cuatro reglas:

{¬(A∨B)}⊢¬A∧¬B\left\{\neg(A\vee B)\right\}\vdash\neg A\wedge\neg B
{¬A∧¬B}⊢¬(A∨B)\left\{\neg A\wedge\neg B\right\}\vdash\neg(A\vee B)
{¬(A∧B)}⊢¬A∨¬B\left\{\neg(A\wedge B)\right\}\vdash\neg A\vee\neg B
{¬A∨¬B}⊢¬(A∧B)\left\{\neg A\vee\neg B\right\}\vdash\neg(A\wedge B)
Proof 17.14.

DM1:

  1. 1.
    ​

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

[resume] 1.​AA Pr aux 2.​A∨BI∨,2A\vee B\quad I\vee,2 3.​(A∨B)∧¬(A∨B)I∧,1,3(A\vee B)\wedge\neg(A\vee B)\quad I\wedge,1,3

  1. 5.
    ​

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

  2. 6.
    ​

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

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

  1. 9.
    ​

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

  2. 10.
    ​

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

DM2:

  1. 1.
    ​

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

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

  1. 7.
    ​

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

DM3:

  1. 1.
    ​

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

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

  1. 10.
    ​

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

DM4:

  1. 1.
    ​

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

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

  1. 7.
    ​

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

Theorem 17.15 (Interdefinicion).

Cuatro reglas:

{A→B}⊢¬A∨B\left\{A\to B\right\}\vdash\neg A\vee B