Càlcul proposicional de Frege

Càlcul proposicional de Frege, en la Llògica matemàtica, el càlcul proposicional de Frege va ser la primera axiomatisació del càlcul proposicional. Va ser inventat per Gottlob Frege, qui també va inventar el càlcul de predicats, en 1879, com a part de la seua càlcul de predicats de segon orde (a pesar de que Charles Peirce va ser el primer en utilisar el terme "segon orde" i va desenrollar la seua pròpia versió de forma independent del càlcul de predicats de Frege).

Fa us de només dos operadors llògics: Implicació i la negació, i està constituïda per sis axioma i una regla d'inferència: modus ponens.

Axioma

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 d'Inferència

MP: P, P→Q ⊢ Q

El Càlcul proposicional de Frege és equivalent a qualsevol atre càlcul proposicional clàssic, com el "Càlcul proposicional" (CP) normal en 11 axioma. El CP de Frege i CP estàndart compartixen dos axioma en comú: THEN-1 i THEN-2. Tenint en conte que els axioma THEN-1 a el THEN-3 només fan us (i ho definixen) de l'operador d'implicació, mentres que els axioma FRG-1 a el FRG-3 definixen a l'operador de negació.

Les teoremes següents tindran com a objectiu trobar els atres nou axioma de el CP estàndart en la teorema de el CP de Frege, mostrant que la teoria-espai de el CP estàndart està contingut dins de la teoria de el CP de Frege.

(Una teoria, també nomenada ací, en fins de figuració, un "teorema-espai, és un conjunt de teoremes que són un subconjunt d'un conjunt univers de Fòrmules ben formades. Les teoremes estan vinculades entre sí en una forma indicada per les Regles d'inferència, formant una espècie de ret ramificada. En les raïls de la teorema-espai es troben els axioma, que "generen" la teorema-espai molt similar a un generador generant un grup.)

Vore també

• en:Begriffsschrift
• Càlcul proposicional
• Forma llògica
• Fòrmules ben formades