Исчисление высказываний Фрегеса - Википедия - Freges propositional calculus

В математическая логика, Исчисление высказываний Фреге был первым аксиоматизация из пропозициональное исчисление. Это было изобретено Готтлоб Фреге, который также изобрел исчисление предикатов, в 1879 г. в рамках его исчисление предикатов второго порядка (несмотря на то что Чарльз Пирс был первым, кто использовал термин «второй порядок» и разработал свою версию исчисления предикатов независимо от Фреге).

Он использует всего два логических оператора: импликацию и отрицание, и состоит из шести аксиомы и один правило вывода: modus ponens.

АксиомыПравило вывода
ТО-1
А → (В → А)
ТО-2
(A → (B → C)) → ((A → B) → (A → C))
ТО-3
(A → (B → C)) → (B → (A → C))
ФРГ-1
(A → B) → (¬B → ¬A)
ФРГ-2
¬¬A → А
ФРГ-3
А → ¬¬A
Депутат
P, P → Q ⊢ Q

Исчисление высказываний Фреге эквивалентно любому другому классическому исчислению высказываний, например, «стандартному ПК» с 11 аксиомами. ПК Фреге и стандартный ПК разделяют две общие аксиомы: THEN-1 и THEN-2. Обратите внимание, что аксиомы с THEN-1 по THEN-3 используют (и определяют) только оператор импликации, тогда как аксиомы FRG-1 по FRG-3 определяют оператор отрицания.

Следующие теоремы будут стремиться найти оставшиеся девять аксиом стандартного ПК в «пространстве теорем» ПК Фреге, показывая, что теория стандартного ПК содержится в теории ПК Фреге.

(Теория, также называемая здесь в переносных целях «пространством теорем», представляет собой набор теорем, которые являются подмножеством универсального набора правильные формулы. Теоремы связаны между собой направленным образом: правила вывода, образуя своего рода дендритную сеть. В основе пространства теорем находятся аксиомы, которые «порождают» пространство теорем во многом как генераторная установка генерирует группу.)

Правила

Правило (ТО-1) — А ⊢ В → А

#wffпричина
1.Апредпосылка
2.А → (В → А)ТО-1
3.Б → АМП 1,2.

Правило (ТО-2) —  A → (B → C) ⊢ (A → B) → (A → C)

#wffпричина
1.А → (В → С)предпосылка
2.(A → (B → C)) → ((A → B) → (A → C))ТО-2
3.(А → В) → (А → С)МП 1,2.

Правило (ТО-3) — A → (B → C) ⊢ B → (A → C)

#wffпричина
1.А → (В → С)предпосылка
2.(A → (B → C)) → (B → (A → C))ТО-3
3.В → (А → С)МП 1,2.

Правило (ФРГ-1) — А → В ⊢ ¬B → ¬A

#wffпричина
1.(A → B) → (¬B → ¬A)ФРГ-1
2.А → Бпредпосылка
3.¬B → ¬AМП 2,1.

Правило (TH1) —  А → В, В → С ⊢ А → С

#wffпричина
1.B → Cпредпосылка
2.(B → C) → (A → (B → C))ТО-1
3.А → (В → С)МП 1,2
4.(A → (B → C)) → ((A → B) → (A → C))ТО-2
5.(А → В) → (А → С)MP 3,4
6.А → Бпредпосылка
7.А → СМП 6,5.

Теоремы

Теорема (TH1) — (A → B) → ((B → C) → (A → C))

#wffпричина
1.(B → C) → (A → (B → C))ТО-1
2.(A → (B → C)) → ((A → B) → (A → C))ТО-2
3.(B → C) → ((A → B) → (A → C))TH1 * 1,2
4.((B → C) → ((A → B) → (A → C))) → ((A → B) → ((B → C) → (A → C)))ТО-3
5.(A → B) → ((B → C) → (A → C))МП 3,4.

Теорема (TH2) — А → (¬A → ¬B)

#wffпричина
1.А → (В → А)ТО-1
2.(B → A) → (¬A → ¬B)ФРГ-1
3.А → (¬A → ¬B)TH1 * 1,2.

Теорема (TH3) — ¬A → (A → ¬B)

#wffпричина
1.А → (¬A → ¬B)TH 2
2.(A → (¬A → ¬B)) → (¬A → (A → ¬B))ТО-3
3.¬A → (A → ¬B)МП 1,2.

Теорема (TH4) — ¬ (А → ¬B) → А

#wffпричина
1.¬A → (A → ¬B)TH3
2.(¬A → (A → ¬B)) → (¬ (A → ¬B) → ¬¬A)ФРГ-1
3.¬ (А → ¬B) → ¬¬AМП 1,2
4.¬¬A → АФРГ-2
5.¬ (А → ¬B) → АTH1 * 3,4.

Теорема (TH5) — (A → ¬B) → (B → ¬A)

#wffпричина
1.(A → ¬B) → (¬¬B → ¬A)ФРГ-1
2.((A → ¬B) → (¬¬B → ¬A)) → (¬¬B → ((A → ¬B) → ¬A))ТО-3
3.¬¬B → ((A → ¬B) → ¬A)МП 1,2
4.B → ¬¬BФРГ-3, с A: = B
5.B → ((A → ¬B) → ¬A)TH1 * 4,3
6.(B → ((A → ¬B) → ¬A)) → ((A → ¬B) → (B → ¬A))ТО-3
7.(A → ¬B) → (B → ¬A)МП 5,6.

Теорема (TH6) — ¬ (A → ¬B) → B

#wffпричина
1.¬ (B → ¬A) → BTH4, где A: = B, B: = A
2.(B → ¬A) → (A → ¬B)TH5, где A: = B, B: = A
3.((B → ¬A) → (A → ¬B)) → (¬ (A → ¬B) → ¬ (B → ¬A))ФРГ-1
4.¬ (A → ¬B) → ¬ (B → ¬A)MP 2,3
5.¬ (A → ¬B) → BTH1 * 4,1.

Теорема (TH7) — А → А

#wffпричина
1.А → ¬¬AФРГ-3
2.¬¬A → АФРГ-2
3.А → АTH1 * 1,2.

Теорема (TH8) — А → ((А → В) → Б)

#wffпричина
1.(А → В) → (А → В)TH7, где A: = A → B
2.((A → B) → (A → B)) → (A → ((A → B) → B))ТО-3
3.А → ((А → В) → Б)МП 1,2.

Теорема (TH9) — Б → ((А → В) → Б)

#wffпричина
1.Б → ((А → В) → Б)ТО-1, где A: = B, B: = A → B.

Теорема (TH10) — A → (B → ¬ (A → ¬B))

#wffпричина
1.(A → ¬B) → (A → ¬B)TH7
2.((A → ¬B) → (A → ¬B)) → (A → ((A → ¬B) → ¬B)ТО-3
3.А → ((А → ¬B) → ¬B)МП 1,2
4.((A → ¬B) → ¬B) → (B → ¬ (A → ¬B))TH5
5.A → (B → ¬ (A → ¬B))TH1 * 3,4.

Примечание: ¬ (A → ¬B) → A (TH4), ¬ (A → ¬B) → B (TH6) и A → (B → ¬ (A → ¬B)) (TH10), поэтому ¬ (A → ¬B) ведет себя так же, как A∧B (сравните с аксиомами AND-1, AND-2 и AND-3).

Теорема (TH11) — (A → B) → ((A → ¬B) → ¬A)

#wffпричина
1.A → (B → ¬ (A → ¬B))TH10
2.(A → (B → ¬ (A → ¬B))) → ((A → B) → (A → ¬ (A → ¬B)))ТО-2
3.(A → B) → (A → ¬ (A → ¬B))МП 1,2
4.(A → ¬ (A → ¬B)) → ((A → ¬B) → ¬A)TH5
5.(A → B) → ((A → ¬B) → ¬A)TH1 * 3,4.

TH11 - это аксиома НЕ-1 стандартного ПК, называемая "сокращение до абсурда ".

Теорема (TH12) — ((A → B) → C) → (A → (B → C))

#wffпричина
1.В → (А → В)ТО-1
2.(B → (A → B)) → (((A → B) → C) → (B → C))TH1
3.((A → B) → C) → (B → C)МП 1,2
4.(B → C) → (A → (B → C))ТО-1
5.((A → B) → C) → (A → (B → C))TH1 * 3,4.

Теорема (TH13) — (B → (B → C)) → (B → C)

#wffпричина
1.(B → (B → C)) → ((B → B) → (B → C))ТО-2
2.(B → B) → ((B → (B → C)) → (B → C))ТО-3 * 1
3.B → BTH7
4.(B → (B → C)) → (B → C)МП 3,2.

Правило (TH14) —  A → (B → P), P → Q ⊢ A → (B → Q)

#wffпричина
1.P → Qпредпосылка
2.(P → Q) → (B → (P → Q))ТО-1
3.B → (P → Q)МП 1,2
4.(B → (P → Q)) → ((B → P) → (B → Q))ТО-2
5.(B → P) → (B → Q)MP 3,4
6.((B → P) → (B → Q)) → (A → ((B → P) → (B → Q)))ТО-1
7.A → ((B → P) → (B → Q))MP 5,6
8.(A → (B → P)) → (A → (B → Q))ТО-2 * 7
9.А → (В → П)предпосылка
10.А → (В → Q)МП 9,8.

Теорема (TH15) — ((A → B) → (A → C)) → (A → (B → C))

#wffпричина
1.((A → B) → (A → C)) → (((A → B) → A) → ((A → B) → C))ТО-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)))ТО-3 * 3
5.А → ((А → В) → А)ТО-1
6.A → (((A → B) → (A → C)) → (A → (B → C)))TH1 * 5,4
7.((A → B) → (A → C)) → (A → (A → (B → C)))ТО-3 * 6
8.(A → (A → (B → C))) → (A → (B → C))TH13
9.((A → B) → (A → C)) → (A → (B → C))TH1 * 7,8.

Теорема TH15 - это разговаривать аксиомы ТО-2.

Теорема (TH16) — (¬A → ¬B) → (B → A)

#wffпричина
1.(¬A → ¬B) → (¬¬B → ¬¬A)ФРГ-1
2.¬¬B → ((¬A → ¬B) → ¬¬A)ТО-3 * 1
3.B → ¬¬BФРГ-3
4.В → ((¬A → ¬B) → ¬¬A)TH1 * 3,2
5.(¬A → ¬B) → (B → ¬¬A)ТО-3 * 4
6.¬¬A → АФРГ-2
7.(¬¬A → A) → (B → (¬¬A → A))ТО-1
8.Б → (¬¬A → А)МП 6,7
9.(B → (¬¬A → A)) → ((B → ¬¬A) → (B → A))ТО-2
10.(B → ¬¬A) → (B → A)MP 8,9
11.(¬A → ¬B) → (B → A)TH1 * 5,10.

Теорема (TH17) — (¬A → B) → (¬B → A)

#wffпричина
1.(¬A → ¬¬B) → (¬B → A)TH16, с B: = ¬B
2.B → ¬¬BФРГ-3
3.(B → ¬¬B) → (¬A → (B → ¬¬B))ТО-1
4.¬A → (B → ¬¬B)MP 2,3
5.(¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B))ТО-2
6.(¬A → B) → (¬A → ¬¬B)MP 4,5
7.(¬A → B) → (¬B → A)TH1 * 6,1.

Сравните TH17 с теоремой TH5.

Теорема (TH18) — ((A → B) → B) → (¬A → B)

#wffпричина
1.(A → B) → (¬B → (A → B))ТО-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))ТО-2
9.(¬B → ¬ (A → B)) → (¬B → A)MP 7,8
10.((A → B) → B) → (¬B → ¬ (A → B))ФРГ-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.

Теорема (TH19) — (A → C) → ((B → C) → (((A → B) → B) → C))

#wffпричина
1.¬A → (¬B → ¬ (¬A → ¬¬B))TH10
2.B → ¬¬BФРГ-3
3.(B → ¬¬B) → (¬A → (B → ¬¬B))ТО-1
4.¬A → (B → ¬¬B)MP 2,3
5.(¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B))ТО-2
6.(¬A → B) → (¬A → ¬¬B)MP 4,5
7.¬ (¬A → ¬¬B) → ¬ (¬A → B)ФРГ-1 * 6
8.¬A → (¬B → ¬ (¬A → B))TH14 * 1,7
9.((A → B) → B) → (¬A → B)TH18
10.¬ (¬A → B) → ¬ ((A → B) → B)ФРГ-1 * 9
11.¬A → (¬B → ¬ ((A → B) → B))TH14 * 8,10
12.¬C → (¬A → (¬B → ¬ ((A → B) → B)))ТО-1 * 11
13.(¬C → ¬A) → (¬C → (¬B → ¬ ((A → B) → B)))ТОГДА-2 * 12
14.(¬C → (¬B → ¬ ((A → B) → B))) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B)))ТО-2
15.(¬C → ¬A) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B)))TH1 * 13,14
16.(A → C) → (¬C → ¬A)ФРГ-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)ФРГ-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.

Примечание: A → ((A → B) → B) (TH8), B → ((A → B) → B) (TH9) и (A → C) → ((B → C) → (((A → B) → B) → C)) (TH19), поэтому ((A → B) → B) ведет себя так же, как A∨B. (Сравните с аксиомами OR-1, OR-2 и OR-3.)

Теорема (TH20) — (А → ¬A) → ¬A

#wffпричина
1.(A → A) → ((A → ¬A) → ¬A)TH11
2.А → АTH7
3.(А → ¬A) → ¬AМП 2,1.

TH20 соответствует аксиоме НЕ-3 стандартного ПК, называемой "tertium non datur ".

Теорема (TH21) — А → (¬A → В)

#wffпричина
1.А → (¬A → ¬¬B)TH2, где B: = ~ B
2.¬¬B → BФРГ-2
3.А → (¬A → В)TH14 * 1,2.

TH21 соответствует аксиоме НЕ-2 стандартного ПК, называемой "ex противоречие quodlibet ".

Все аксиомы стандартного ПК были заимствованы из ПК Фреге после того, как

Правило ($1) — $2

A∧B: = ¬ (A → ¬B) и A∨B: = (A → B) → B. Эти выражения не уникальны, например A∨B также можно было определить как (B → A) → A, ¬A → B или ¬B → A. Однако обратите внимание, что определение A∨B: = (A → B) → B не содержит отрицаний. С другой стороны, A∧B нельзя определить только в терминах импликации без использования отрицания.

В некотором смысле выражения A∧B и A∨B можно рассматривать как «черные ящики». Внутри эти черные ящики содержат формулы, состоящие только из импликации и отрицания. Черные ящики могут содержать что угодно, пока они подключены к аксиомам от AND-1 до AND-3 и OR-1 до OR-3 стандартного ПК, эти аксиомы остаются верными. Эти аксиомы предоставляют полные синтаксические определения соединение и дизъюнкция операторы.

Следующий набор теорем будет направлен на поиск оставшихся четырех аксиом ПК Фреге в «пространстве теорем» стандартного ПК, показывая, что теория ПК Фреге содержится в теории стандартного ПК.

Теорема (ST1) — А → А

#wffпричина
1.(A → ((A → A) → A)) → ((A → (A → A)) → (A → A))ТО-2
2.А → ((А → А) → А)ТО-1
3.(А → (А → А)) → (А → А)MP 2,1
4.А → (А → А)ТО-1
5.А → АМП 4,3.

Теорема (ST2) — А → ¬¬A

#wffпричина
1.Агипотеза
2.А → (¬A → А)ТО-1
3.¬A → АМП 1,2
4.¬A → ¬AST1
5.(¬A → A) → ((¬A → ¬A) → ¬¬A)НЕ-1
6.(¬A → ¬A) → ¬¬AMP 3,5
7.¬¬AMP 4,6
8.А ⊢ ¬¬Aрезюме 1-7
9.А → ¬¬AДТ 8.

ST2 - аксиома FRG-3 ПК Фреге.

Теорема (ST3) — B∨C → (¬C → B)

#wffпричина
1.С → (¬C → В)НЕ-2
2.B → (¬C → B)ТО-1
3.(B → (¬C → B)) → ((C → (¬C → B)) → ((B ∨ C) → (¬C → B)))ИЛИ-3
4.(C → (¬C → B)) → ((B ∨ C) → (¬C → B))MP 2,3
5.B∨C → (¬C → B)МП 1,4.

Теорема (ST4) — ¬¬A → А

#wffпричина
1.A∨¬AНЕ-3
2.(A∨¬A) → (¬¬A → A)ST3
3.¬¬A → АМП 1,2.

ST4 - аксиома FRG-2 ПК Фреге.

Докажите ST5: (A → (B → C)) → (B → (A → C))

#wffпричина
1.А → (В → С)гипотеза
2.Bгипотеза
3.Агипотеза
4.B → CMP 3,1
5.CМП 2,4
6.А → (В → С), В, А ⊢ Срезюме 1-5
7.А → (В → С), В ⊢ А → СDT 6
8.A → (B → C) ⊢ B → (A → C)DT 7
9.(A → (B → C)) → (B → (A → C))ДТ 8.

ST5 - это аксиома THEN-3 ПК Фреге.

Теорема (ST6) — (A → B) → (¬B → ¬A)

#wffпричина
1.А → Бгипотеза
2.¬Bгипотеза
3.¬B → (A → ¬B)ТО-1
4.А → ¬BMP 2,3
5.(A → B) → ((A → ¬B) → ¬A)НЕ-1
6.(А → ¬B) → ¬AMP 1,5
7.¬AMP 4,6
8.А → В, ¬B ⊢ ¬Aрезюме 1-7
9.А → В ⊢ ¬B → ¬ADT 8
10.(A → B) → (¬B → ¬A)DT 9.

ST6 - аксиома FRG-1 ПК Фреге.

Каждую из аксиом Фреге можно вывести из стандартных аксиом, и каждую из стандартных аксиом можно вывести из аксиом Фреге. Это означает, что два набора аксиом взаимозависимы, и в одном наборе нет аксиомы, независимой от другого. Следовательно, эти два набора аксиом порождают одну и ту же теорию: ПК Фреге эквивалентен стандартному ПК.

(Поскольку, если теории должны быть разными, то одна из них должна содержать теоремы, не содержащиеся в другой теории. Эти теоремы могут быть выведены из набора аксиом их собственной теории: но, как было показано, весь этот набор аксиом может быть получен из другой теории. набор аксиом теории, что означает, что данные теоремы могут быть фактически получены исключительно из набора аксиом другой теории, так что данные теоремы также принадлежат другой теории. Противоречие: таким образом, два набора аксиом охватывают одно и то же пространство теорем. : Любая теорема, полученная из стандартных аксиом, может быть выведена из аксиом Фреге, и наоборот, сначала доказывая как теоремы аксиомы другой теории, как показано выше, а затем используя эти теоремы как леммы для вывода желаемой теоремы.)

Смотрите также

Рекомендации

  • Басс, Сэмюэл (1998). «Введение в теорию доказательств» (PDF). Справочник по теории доказательств. Эльзевир. С. 1–78. ISBN  0-444-89840-9.
  • Детловс, Вилнис; Подниекс, Карлис (24 мая 2017 г.). «Аксиомы логики: минимальная система, конструктивная система и классическая система». Введение в математическую логику (PDF). Латвийский университет. С. 29–30.