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.

Véase también

• en:Begriffsschrift
• Cálculo proposicional
• Forma lógica
• Fórmulas bien formadas

Referencias

• Rosado Haddock, Guillermo (1996). A critical introduction to the philosophy of Gottlob Frege. Rowe.

• Buss, Samuel (1998). «An introduction to proof theory». Handbook of proof theory. Elsevier. pp. 1-78. ISBN 0-444-89840-9.

Enlaces externos

• Introducción a la lógica proposicional

• Datos: Q714691