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.

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

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.)

FBF → Fórmula bien formada

Regla THEN-1

Regla THEN-2

Regla THEN-3

Regla FRG-1

Regla TH1

Teorema TH1

Teorema TH2

Teorema TH3

Teorema TH4

Teorema TH5

Teorema TH6

Teorema TH7

Teorema TH8

Teorema TH9

Teorema TH10

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

TH11 es un axioma NOT-1 de cálculo proposicional estándar, llamado "reductio ad absurdum".

Teorema TH12

Teorema TH13

Teorema TH14

Teorema TH15

El teorema TH15 es la Conversión lógica del axioma THEN-2.

Teorema TH16

Teorema TH17

Compara TH17 con el teorema TH5.

Teorema TH18

Teorema TH19

(((¬C→¬B)→ (((A→B)→B)→C) ) → ( (B→C) → (((A→B)→B)→C)))

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

TH20 corresponde al axioma NOT-3 del cálculo proposicional estándar, llamado "tertium non datur".

Teorema TH21

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.

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

Teorema ST2

ST2 es el axioma FRG-3 del cálculo proposicional de Frege.

Teorema ST3

Teorema ST4

ST4 es el axioma FRG-2 del cálculo proposicional de Frege.

Teorema ST5

ST5 es el axioma THEN-3 del cálculo proposicional de Frege.

Teorema ST6

ST6 es el axioma FRG-1 del cálculo proposicional de Frege.

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.

---