Concept

Frege's propositional calculus

In mathematical logic, Frege's propositional calculus was the first axiomatization of propositional calculus. It was invented by Gottlob Frege, who also invented predicate calculus, in 1879 as part of his second-order predicate calculus (although Charles Peirce was the first to use the term "second-order" and developed his own version of the predicate calculus independently of Frege). It makes use of just two logical operators: implication and negation, and it is constituted by six axioms and one inference rule: modus ponens. Frege's propositional calculus is equivalent to any other classical propositional calculus, such as the "standard PC" with 11 axioms. Frege's PC and standard PC share two common axioms: THEN-1 and THEN-2. Notice that axioms THEN-1 through THEN-3 only make use of (and define) the implication operator, whereas axioms FRG-1 through FRG-3 define the negation operator. The following theorems will aim to find the remaining nine axioms of standard PC within the "theorem-space" of Frege's PC, showing that the theory of standard PC is contained within the theory of Frege's PC. (A theory, also called here, for figurative purposes, a "theorem-space", is a set of theorems that are a subset of a universal set of well-formed formulas. The theorems are linked to each other in a directed manner by inference rules, forming a sort of dendritic network. At the roots of the theorem-space are found the axioms, which "generate" the theorem-space much like a generating set generates a group.) A ⊢ B→A A→(B→C) ⊢ (A→B)→(A→C) A→(B→C) ⊢ B→(A→C) A→B ⊢ ¬B→¬A A→B, B→C ⊢ A→C (A→B)→((B→C)→(A→C)) A→(¬A→¬B) ¬A→(A→¬B) ¬(A→¬B)→A (A→¬B)→(B→¬A) ¬(A→¬B)→B A→A A→((A→B)→B) B→((A→B)→B) A→(B→¬(A→¬B)) Note: ¬(A→¬B)→A (TH4), ¬(A→¬B)→B (TH6), and A→(B→¬(A→¬B)) (TH10), so ¬(A→¬B) behaves just like A∧B (compare with axioms AND-1, AND-2, and AND-3). (A→B)→((A→¬B)→¬A) TH11 is axiom NOT-1 of standard PC, called "reductio ad absurdum". ((A→B)→C)→(A→(B→C)) (B→(B→C))→(B→C) A→(B→P), P→Q ⊢ A→(B→Q) ((A→B)→(A→C))→(A→(B→C)) Theorem TH15 is the converse of axiom THEN-2.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.