Введение
В математической логике исчисление высказываний Фреге было первой аксиоматизацией исчисления высказываний. Оно было изобретено Готлобом Фреге, который также изобрел исчисление предикатов, в 1879 году в рамках своего исчисления предикатов второго порядка (хотя Чарльз Пирс был первым, кто использовал термин "второго порядка" и разработал свою собственную версию исчисления предикатов независимо от Фреге). Оно использует только два логических оператора: импликацию и отрицание и состоит из шести аксиом и одного правила вывода: 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 → ¬¬AMP P, P→Q ⊢ Q
Исчисление высказываний Фреге эквивалентно любому другому классическому исчислению высказываний, такому как "стандартный ПК" с 11 аксиомами. ПК Фреге и стандартный ПК имеют две общие аксиомы: THEN 1 и THEN 2. Обратите внимание, что аксиомы THEN 1 – THEN 3 используют (и определяют) только оператор импликации, в то время как аксиомы FRG 1 – FRG 3 определяют оператор отрицания. Следующие теоремы направлены на поиск оставшихся девяти аксиом стандартного ПК в "пространстве теорем" ПК Фреге, показывая, что теория стандартного ПК содержится в теории ПК Фреге. (Теория, также называемая здесь, в переносном смысле, "пространством теорем", представляет собой набор теорем, являющихся подмножеством универсального множества корректных формул. Теоремы связаны друг с другом направленным образом посредством правил вывода, образуя своего рода дендритную сеть. В корнях пространства теорем находятся аксиомы, которые "генерируют" пространство теорем, подобно тому, как образующее множество генерирует группу.)
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 → ¬¬AMP P, P→Q ⊢ Q
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.)
Правила
#wffreason1. Посылка2. А→(Б→А) ТОГДА 13. B→A МП 1,2. #wffreason1. A→(B→C) посылка2. (A → (B → C)) → ((A → B) → (A → C)) ТОГДА 23. (A→B)→(A→C) МП 1,2. #wffreason1. A→(B→C) посылка2. (A → (B → C)) → (B → (A → C)) ТОГДА 33. B→(A→C) МП 1,2. #wffreason1. (A→B)→(¬B→¬A) ФРГ 12. A→B посылка3. ¬B→¬A МП 2,1. #wffreason1. B→C посылка2. (B→C)→(A→(B→C)) ТОГДА 13. A→(B→C) МП 1,24. (A→(B→C))→((A→B)→(A→C)) ТОГДА 25. (A→B)→(A→C) МП 3,46. A→B посылка7. A→C МП 6,5.