# Cálculo proposicional de Frege

Cálculo proposicional de Frege, en la Lógica matemática, el cálculo proposicional de Frege fue la primera axiomatización del cálculo proposicional. Fue inventado por Gottlob Frege, quien también inventó el cálculo de predicados, en 1879, como parte de su cálculo de predicados de segundo orden (a pesar de que Charles Peirce fue el primero en utilizar el término "segundo orden" y desarrolló su propia versión de forma independiente del cálculo de predicados de Frege).
Hace uso de sólo dos operadores lógicos: Implicación y la negación, y está constituida por seis axiomas y una regla de inferencia: modus ponens.

## Axiomas

THEN-1: A → (B → A) THEN-2: (A → (B → C)) → ((A → B) → (A → C)) THEN-3: (A → (B → C)) → (B → (A → C)) FRG-1: (A → B) → (¬B → ¬A) FRG-2: ¬¬A → A FRG-3: A → ¬¬A

## Regla de Inferencia

MP: P, P→Q ⊢ Q
El Cálculo proposicional de Frege es equivalente a cualquier otro cálculo proposicional clásico, como el "Cálculo proposicional" (CP) normal con 11 axiomas. El CP de Frege y CP estándar comparten dos axiomas en común: THEN-1 y THEN-2. Teniendo en cuenta que los axiomas THEN-1 al THEN-3 sólo hacen uso (y lo definen) del operador de implicación, mientras que los axiomas FRG-1 al FRG-3 definen al operador de negación.
Los teoremas siguientes tendrán como objetivo encontrar los otros nueve axiomas del CP estándar en el teorema del CP de Frege, mostrando que la teoría-espacio del CP estándar está contenido dentro de la teoría del CP de Frege.
(Una teoría, también nombrada aquí, con fines de figuración, un "teorema-espacio, es un conjunto de teoremas que son un subconjunto de un conjunto universo de Fórmulas bien formadas. Los teoremas están vinculados entre sí en una forma indicada por las Reglas de inferencia, formando una especie de red ramificada. En las raíces del teorema-espacio se encuentran los axiomas, que "generan" el teorema-espacio muy similar a un generador generando un grupo.)

## Reglas y Teoremas

FBF → Fórmula bien formada

### Reglas THEN

Regla THEN-1
* A ⊢ B→A
| # | FBF | Razón |
| 1. | A | premisa |
| 2. | A→(B→A) | THEN-1 |
| 3. | B→A | MP 1,2. |
Regla THEN-2
* A→(B→C) ⊢ (A→B)→(A→C)
| # | FBF | Razón |
| 1. | A→(B→C) | premisa |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | THEN-2 |
| 3. | (A→B)→(A→C) | MP 1,2. |
Regla THEN-3
* A→(B→C) ⊢ B→(A→C)
| # | FBF | Razón |
| 1. | A→(B→C) | premisa |
| 2. | (A → (B → C)) → (B → (A → C)) | THEN-3 |
| 3. | B→(A→C) | MP 1,2. |
Regla FRG-1
* A→B ⊢ ¬B→¬A
| # | FBF | Razón |
| 1. | (A→B)→(¬B→¬A) | FRG-1 |
| 2. | A→B | premisa |
| 3. | ¬B→¬A | MP 2,1. |
Regla TH1
* A→B, B→C ⊢ A→C
| # | FBF | Razón |
| 1. | B→C | premisa |
| 2. | (B→C)→(A→(B→C)) | THEN-1 |
| 3. | A→(B→C) | MP 1,2 |
| 4. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 5. | (A→B)→(A→C) | MP 3,4 |
| 6. | A→B | premisa |
| 7. | A→C | MP 6,5. |

### Teoremas TH

Teorema TH1
* (A→B)→((B→C)→(A→C))
| # | FBF | Razón |
| 1. | (B→C)→(A→(B→C)) | THEN-1 |
| 2. | (A→(B→C))→((A→B)→(A→C)) | THEN-2 |
| 3. | (B→C)→((A→B)→(A→C)) | TH1* 1,2 |
| 4. | ((B→C)→((A→B)→(A→C)))→((A→B)→((B→C)→(A→C))) | THEN-3 |
| 5. | (A→B)→((B→C)→(A→C)) | MP 3,4. |
Teorema TH2
* A→(¬A→¬B)
| # | FBF | Razón |
| 1. | A→(B→A) | THEN-1 |
| 2. | (B→A)→(¬A→¬B) | FRG-1 |
| 3. | A→(¬A→¬B) | TH1* 1,2. |
Teorema TH3
* ¬A→(A→¬B)
| # | FBF | Razón |
| 1. | A→(¬A→¬B) | TH 2 |
| 2. | (A→(¬A→¬B))→(¬A→(A→¬B)) | THEN-3 |
| 3. | ¬A→(A→¬B) | MP 1,2. |
Teorema TH4
* ¬(A→¬B)→A
| # | FBF | Razón |
| 1. | ¬A→(A→¬B) | TH3 |
| 2. | (¬A→(A→¬B))→(¬(A→¬B)→¬¬A) | FRG-1 |
| 3. | ¬(A→¬B)→¬¬A | MP 1,2 |
| 4. | ¬¬A→A | FRG-2 |
| 5. | ¬(A→¬B)→A | TH1* 3,4. |
Teorema TH5
* (A→¬B)→(B→¬A)
| # | FBF | Razón |
| 1. | (A→¬B)→(¬¬B→¬A) | FRG-1 |
| 2. | ((A→¬B)→(¬¬B→¬A))→(¬¬B→((A→¬B)→¬A)) | THEN-3 |
| 3. | ¬¬B→((A→¬B)→¬A) | MP 1,2 |
| 4. | B→¬¬B | FRG-3, with A := B |
| 5. | B→((A→¬B)→¬A) | TH1* 4,3 |
| 6. | (B→((A→¬B)→¬A))→((A→¬B)→(B→¬A)) | FRG-1 |
| 7. | (A→¬B)→(B→¬A) | MP 5,6. |
Teorema TH6
* ¬(A→¬B)→B
| # | FBF | Razón |
| 1. | ¬(B→¬A)→B | TH4, with A := B, B := A |
| 2. | (B→¬A)→(A→¬B) | TH5, with A := B, B := A |
| 3. | ((B→¬A)→(A→¬B))→(¬(A→¬B)→¬(B→¬A)) | FRG-1 |
| 4. | ¬(A→¬B)→¬(B→¬A) | MP 2,3 |
| 5. | ¬(A→¬B)→B | TH1* 4,1. |
Teorema TH7
* A→A
| # | FBF | Razón |
| 1. | A→¬¬A | FRG-3 |
| 2. | ¬¬A→A | FRG-2 |
| 3. | A→A | TH1* 1,2. |
Teorema TH8
* A→((A→B)→B)
| # | FBF | Razón |
| 1. | (A→B)→(A→B) | TH7, with A := A→B |
| 2. | ((A→B)→(A→B))→(A→((A→B)→B)) | THEN-3 |
| 3. | A→((A→B)→B) | MP 1,2. |
Teorema TH9
* B→((A→B)→B)
| # | FBF | Razón |
| 1. | B→((A→B)→B) | THEN-1, with A := B, B := A→B. |
Teorema TH10
* A→(B→¬(A→¬B))
| # | FBF | Razón |
| 1. | (A→¬B)→(A→¬B) | TH7 |
| 2. | ((A→¬B)→(A→¬B))→(A→((A→¬B)→¬B) | THEN-3 |
| 3. | A→((A→¬B)→¬B) | MP 1,2 |
| 4. | ((A→¬B)→¬B)→(B→¬(A→¬B)) | TH5 |
| 5. | A→(B→¬(A→¬B)) | TH1* 3,4. |
Nota: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), y A→(B→¬(A→¬B)) (TH10), entonces ¬(A→¬B) se comporta como A∧B. (Compara con los axiomas AND-1, AND-2, y AND-3).
Teorema TH11
* (A→B)→((A→¬B)→¬A)
| # | FBF | Razón |
| 1. | A→(B→¬(A→¬B)) | TH10 |
| 2. | (A→(B→¬(A→¬B)))→((A→B)→(A→¬(A→¬B))) | THEN-2 |
| 3. | (A→B)→(A→¬(A→¬B)) | MP 1,2 |
| 4. | (A→¬(A→¬B))→((A→¬B)→¬A) | TH5 |
| 5. | (A→B)→((A→¬B)→¬A) | TH1* 3,4. |
TH11 es un axioma NOT-1 de cálculo proposicional estándar, llamado "reductio ad absurdum".
Teorema TH12
* ((A→B)→C)→(A→(B→C))
| # | FBF | Razón |
| 1. | B→(A→B) | THEN-1 |
| 2. | (B→(A→B))→(((A→B)→C)→(B→C)) | TH1 |
| 3. | ((A→B)→C)→(B→C) | MP 1,2 |
| 4. | (B→C)→(A→(B→C)) | THEN-1 |
| 5. | ((A→B)→C)→(A→(B→C)) | TH1* 3,4. |
Teorema TH13
* (B→(B→C))→(B→C)
| # | FBF | Razón |
| 1. | (B→(B→C)) → ((B→B)→(B→C)) | THEN-2 |
| 2. | (B→B)→ ( (B→(B→C)) → (B→C)) | THEN-3* 1 |
| 3. | B→B | TH7 |
| 4. | (B→(B→C)) → (B→C) | MP 3,2. |
Teorema TH14
* A→(B→P), P→Q ⊢ A→(B→Q)
| # | FBF | Razón |
| 1. | P→Q | premisa |
| 2. | (P→Q)→(B→(P→Q)) | THEN-1 |
| 3. | B→(P→Q) | MP 1,2 |
| 4. | (B→(P→Q))→((B→P)→(B→Q)) | THEN-2 |
| 5. | (B→P)→(B→Q) | MP 3,4 |
| 6. | ((B→P)→(B→Q))→ (A→((B→P)→(B→Q))) | THEN-1 |
| 7. | A→((B→P)→(B→Q)) | MP 5,6 |
| 8. | (A→(B→P))→(A→(B→Q)) | THEN-2* 7 |
| 9. | A→(B→P) | premisa |
| 10. | A→(B→Q) | MP 9,8. |
Teorema TH15
* ((A→B)→(A→C))→(A→(B→C))
| # | FBF | Razón |
| 1. | ((A→B)→(A→C))→(((A→B)→A)→((A→B)→C)) | THEN-2 |
| 2. | ((A→B)→C)→(A→(B→C)) | TH12 |
| 3. | ((A→B)→(A→C))→(((A→B)→A)→(A→(B→C))) | TH14* 1,2 |
| 4. | ((A→B)→A)→ ( ((A→B) →(A→C))→(A→(B→C))) | THEN-3* 3 |
| 5. | A→((A→B)→A) | THEN-1 |
| 6. | A→ ( ((A→B) →(A→C))→(A→(B→C)) ) | TH1* 5,4 |
| 7. | ((A→B)→(A→C))→(A→(A→(B→C))) | THEN-3* 6 |
| 8. | (A→(A→(B→C)))→(A→(B→C)) | TH13 |
| 9. | ((A→B)→(A→C))→(A→(B→C)) | TH1* 7,8. |
El teorema TH15 es la Conversión lógica del axioma THEN-2.
Teorema TH16
* (¬A→¬B)→(B→A)
| # | FBF | Razón |
| 1. | (¬A→¬B)→(¬¬B→¬¬A) | FRG-1 |
| 2. | ¬¬B→((¬A→¬B)→¬¬A) | THEN-3* 1 |
| 3. | B→¬¬B | FRG-3 |
| 4. | B→((¬A→¬B)→¬¬A) | TH1* 3,2 |
| 5. | (¬A→¬B)→(B→¬¬A) | THEN-3* 4 |
| 6. | ¬¬A→A | FRG-2 |
| 7. | (¬¬A→A)→(B→(¬¬A→A)) | THEN-1 |
| 8. | B→(¬¬A→A) | MP 6,7 |
| 9. | (B→(¬¬A→A))→((B→¬¬A)→(B→A)) | THEN-2 |
| 10. | (B→¬¬A)→(B→A) | MP 8,9 |
| 11. | (¬A→¬B)→(B→A) | TH1* 5,10. |
Teorema TH17
* (¬A→B)→(¬B→A)
| # | FBF | Razón |
| 1. | (¬A→¬¬B)→(¬B→A) | TH16, con B := ¬B |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | (¬A→B)→(¬B→A) | TH1* 6,1. |
Compara TH17 con el teorema TH5.
Teorema TH18
* ((A→B)→B)→(¬A→B)
| # | FBF | Razón |
| 1. | (A→B)→(¬B→(A→B)) | THEN-1 |
| 2. | (¬B→¬A)→(A→B) | TH16 |
| 3. | (¬B→¬A)→(¬B→(A→B)) | TH1* 2,1 |
| 4. | ((¬B→¬A)→(¬B→(A→B)))→(¬B→(¬A→(A→B))) | TH15 |
| 5. | ¬B→(¬A→(A→B)) | MP 3,4 |
| 6. | (¬A→(A→B))→(¬(A→B)→A) | TH17 |
| 7. | ¬B→(¬(A→B)→A) | TH1* 5,6 |
| 8. | (¬B→(¬(A→B)→A))→ ((¬B→¬(A→B))→(¬B→A)) | THEN-2 |
| 9. | (¬B→¬(A→B))→(¬B→A) | MP 7,8 |
| 10. | ((A→B)→B) → (¬B→¬(A→B)) | FRG-1 |
| 11. | ((A→B)→B)→(¬B→A) | TH1* 10,9 |
| 12. | (¬B→A)→(¬A→B) | TH17 |
| 13. | ((A→B)→B)→(¬A→B) | TH1* 11,12. |
Teorema TH19
* (A→C)→ ((B→C)→(((A→B)→B)→C))
| # | FBF | Razón |
| 1. | ¬A→(¬B→¬(¬A→¬¬B)) | TH10 |
| 2. | B→¬¬B | FRG-3 |
| 3. | (B→¬¬B)→(¬A→(B→¬¬B)) | THEN-1 |
| 4. | ¬A→(B→¬¬B) | MP 2,3 |
| 5. | (¬A→(B→¬¬B))→((¬A→B)→(¬A→¬¬B)) | THEN-2 |
| 6. | (¬A→B)→(¬A→¬¬B) | MP 4,5 |
| 7. | ¬(¬A→¬¬B)→¬(¬A→B) | FRG-1* 6 |
| 8. | ¬A→(¬B→¬(¬A→B)) | TH14* 1,7 |
| 9. | ((A→B)→B)→(¬A→B) | TH18 |
| 10. | ¬(¬A→B)→¬((A→B)→B) | FRG-1* 9 |
| 11. | ¬A→(¬B→¬((A→B)→B)) | TH14* 8,10 |
| 12. | ¬C→(¬A→(¬B→¬((A→B)→B))) | THEN-1* 11 |
| 13. | (¬C→¬A)→(¬C→(¬B→¬((A→B)→B))) | THEN-2* 12 |
| 14. | (¬C→(¬B→¬((A→B)→B))) → ((¬C→¬B)→(¬C→¬((A→B)→B))) | THEN-2 |
| 15. | (¬C→¬A)→ ((¬C→¬B)→(¬C→¬((A→B)→B))) | TH1* 13,14 |
| 16. | (A→C)→(¬C→¬A) | FRG-1 |
| 17. | (A→C)→((→C→¬B)→(¬C→¬((A→B)→B))) | TH1* 16,15 |
| 18. | (¬C→¬((A→B)→B))→(((A→B)→B)→C) | TH16 |
| 19. | (A→C)→ ((¬C→¬B)→(((A→B)→B)→C)) | TH14* 17,18 |
| 20. | (B→C)→(¬C→¬B) | FRG-1 |
| 21. | ((B→C)→(¬C→¬B))→ (((¬C→¬B)→ (((A→B)→B)→C) ) → ( (B→C) → (((A→B)→B)→C))) | TH1 |
| 22. | ((¬C→¬B)→ (((A→B)→B)→C) ) → ( (B→C) → (((A→B)→B)→C)) | MP 20,21 |
| 23. | (A→C)→ ((B→C)→(((A→B)→B)→C)) | TH1* 19,22. |
Nota: A→((A→B)→B) (TH8), B→((A→B)→B) (TH9), y (A→C)→((B→C)→(((A→B)→B)→C)) (TH19), entonces((A→B)→B) se comporta como A∨B. (Compara con los axiomas OR-1, OR-2, y OR-3.)
Teorema TH20
* (A→¬A)→¬A
| # | FBF | Razón |
| 1. | (A→A)→((A→¬A)→¬A) | TH11 |
| 2. | A→A | TH7 |
| 3. | (A→¬A)→¬A | MP 2,1. |
TH20 corresponde al axioma NOT-3 del cálculo proposicional estándar, llamado "tertium non datur".
Teorema TH21
* A→(¬A→B)
| # | FBF | Razón |
| 1. | A→(¬A→¬¬B) | TH2, con B := ~B |
| 2. | ¬¬B→B | FRG-2 |
| 3. | A→(¬A→B) | TH14* 1,2. |
TH21 corresponde al axioma NOT-2 del cálculo proposicional estándar, llamado "ex contradictione quodlibet".
Todos los axiomas del cálculo proposicional estándar derivan del cálculo proposicional de Frege.
A∧B := ¬(A→¬B) yA∨B := (A→B)→B.
Estas expresiones no son únicas, por ejemplo, A∨B también podría haber sido definido como
(B→A)→A, ¬A→B, or ¬B→A.
Nótese, sin embargo, que la definición de A∨B := (A→B)→B no contiene negaciones. Por otra parte, A∧B no puede definirse en términos de solo implicación, sin el uso de la negación.
En cierto sentido, las expresiones A∧B y A∨B pueden ser consideradas como "cajas negras". En el interior, estas cajas negras contienen fórmulas compuestas solamente de implicación y negación. Las cajas negras pueden contener cualquier cosa, siempre y cuando estén conectado dentro de los axiomas AND-1 al AND-3 y OR-1 al OR-3 del cálculo proposicional estándar y siguen siendo válidos. Estos axiomas proporcionan definiciones sintácticas completas de los operadores de conjunción y disyunción.

### Teoremas ST

El siguiente conjunto de teoremas tratará de encontrar los otros cuatro axiomas del CP de Frege en el "teorema-espacio" del CP estándar, mostrando que la teoría del CP de Frege está contenido dentro de la teoría del CP estándar.
Teorema ST1
* A→A
| # | FBF | Razón |
| 1. | (A→((A→A)→A))→((A→(A→A))→(A→A)) | THEN-2 |
| 2. | A→((A→A)→A) | THEN-1 |
| 3. | (A→(A→A))→(A→A) | MP 2,1 |
| 4. | A→(A→A) | THEN-1 |
| 5. | A→A | MP 4,3. |
Teorema ST2
* A→¬¬A
| # | FBF | Razón |
| 1. | A | hipótesis |
| 3. | A→(¬A→A) | THEN-1 |
| 4. | ¬A→A | MP 1,3 |
| 6. | ¬A→¬A | ST1 |
| 7. | (¬A→A)→((¬A→¬A)→¬¬A) | NOT-1 |
| 8. | (¬A→¬A)→¬¬A | MP 4,7 |
| 9. | ¬¬A | MP 6,8 |
| 10. | A ⊢ ¬¬A | sumario 1-9 |
| 11. | A→¬¬A | DT 10. |
ST2 es el axioma FRG-3 del cálculo proposicional de Frege.
Teorema ST3
* B∨C→(¬C→B)
| # | FBF | Razón |
| 1. | C→(¬C→B) | NOT-2 |
| 2. | B→(¬C→B) | THEN-1 |
| 3. | (B→(¬C→B))→ ((C→(¬C→B))→((B ∨ C)→(¬C→B))) | OR-3 |
| 4. | (C→(¬C→B))→((B ∨ C)→(¬C→B)) | MP 2,3 |
| 5. | B∨C→(¬C→B) | MP 1,4. |
Teorema ST4
* ¬¬A→A
| # | FBF | Razón |
| 1. | A∨¬A | NOT-3 |
| 2. | (A∨¬A)→(¬¬A→A) | ST3 |
| 3. | ¬¬A→A | MP 1,2. |
ST4 es el axioma FRG-2 del cálculo proposicional de Frege.
Teorema ST5
* (A→(B→C))→(B→(A→C))
| # | FBF | Razón |
| 1. | A→(B→C) | hipótesis |
| 2. | B | hipótesis |
| 3. | A | hipótesis |
| 4. | B→C | MP 3,1 |
| 5. | C | MP 2,4 |
| 6. | A→(B→C), B, A ⊢ C | sumario 1-5 |
| 7. | A→(B→C), B ⊢ A→C | DT 6 |
| 8. | A→(B→C) ⊢ B→(A→C) | DT 7 |
| 9. | (A→(B→C)) → (B→(A→C)) | DT 8. |
ST5 es el axioma THEN-3 del cálculo proposicional de Frege.
Teorema ST6
* (A→B)→(¬B→¬A)
| # | FBF | Razón |
| 1. | A→B | hipótesis |
| 2. | ¬B | hipótesis |
| 3. | ¬B→(A→¬B) | THEN-1 |
| 4. | A→¬B | MP 2,3 |
| 5. | (A→B)→((A→¬B)→¬A) | NOT-1 |
| 6. | (A→¬B)→¬A | MP 1,5 |
| 7. | ¬A | MP 4,6 |
| 8. | A→B, ¬B ⊢ ¬A | sumario 1-7 |
| 9. | A→B ⊢ ¬B→¬A | DT 8 |
| 10. | (A→B)→(¬B→¬A) | DT 9. |
ST6 es el axioma FRG-1 del cálculo proposicional de Frege.

## Conclusión

Cada uno de los axiomas de Frege se pueden derivar de los axiomas estándar, y cada uno de los axiomas estándar se pueden derivar de los axiomas de Frege. Esto significa que los dos conjuntos de axiomas son interdependientes y no hay axioma en un conjunto que sea independiente del otro conjunto. Por lo tanto los dos conjuntos de axiomas generan la misma teoría: El calculo proposicional de Frege es equivalente a un calculo proposicional estándar.