Диссертация (1148869), страница 23
Текст из файла (страница 23)
(!A →!A) ∧ (A → B) → (!A →!B)AX.1(361)2. (!A →!A) → ((A → B) → (!A →!B))экспорт, 1(362)3. (!A →!A)тождество(363)4. (A → B) → (!A →!B)MP, 2,3(364)1. (B → A) → (!B →!A)T.1(365)2. A → (B → A)a fortiori(366)3. A → (!B →!A)транзитивность, 1, 2(367)4. !B → (A →!A)замена, 3(368)(T.2):Факт 4.2 Схема «частичный коллапс»(pColl) A →!A(369)124выводима в М, в действительности, она выводима уже в Mint, используя толькоAX.1 + AX.4 или, альтернативные, AX.1 + AX.3.Доказательство:Вывод (pColl) из AX.1 + AX.4:1. !U → (A →!A)T.2(370)2. !UAX.4(371)3.
A →!AMP, 1, 2(372)1. (!A →!A) →!(!A → A)AX.3[→](373)2. (!A →!A)тождество(374)3. !(!A → A)MP, 1, 2(375)4. !(!A → A) → (A →!A)T.2(376)5. A →!AMP, 3, 4(377)Вывод (pColl) из AX.1 + AX.3:Сентроне отмечает здесь следующее простое следствие из Факта 4.2. ПустьAX.5’ будет «¬!¬U», то есть ослабленный вариант оригинальной AX.5 Малли.Тогда сильная AX.5 оказывается выводимой из {AX.1, AX.4, AX.5’ } или из{AX.1,AX.4,AX.5’},используятолькоинтуиционистскуюлогику.Действительно, из этих аксиом можно вывести ¬ U →! ¬ U по Факту 4.2, и, такимобразом, также ¬! ¬ U → ¬ ¬ U, используя (интуиционистскую) контрапозицию.Затем, по МП с AX.5 можно получить ¬¬U, которая вместе с ¬! ¬ U, дает AX.5 спомощью интуиционистского тезиса ¬ ¬ A ∧ ¬ B → ¬ (A → B).Факт 4.3 Схема фактичности(T) !A → A(378)выводима в М, на самом деле она выводима уже только из AX.1 + AX.5.Доказательство:1.
!A → (U →!A)a fortiori(379)2. ￢A → (A→￢U)исключение лжи(380)3. !A ∧ ￢A → ((U →!A) ∧ (A →￢U))(интуиционистская)(381)125логика, 1, 24. (U →!A) ∧ (A→￢U) → (U →!￢U)AX.1(382)5. !A ∧ ￢A → (U →!￢U)транзитивность, 3, 4(383)6. ￢(U →!￢U)→￢(!A ∧ ￢A)(интуиционистская)(384)контрапозиция, 57. ￢(U →!￢U)AX.5(385)8. ￢(!A ∧ ￢A)MP, 6, 7(386)9. ￢(!A ∧ ￢A) → (!A → A)классическая(387)тавтология10. (!A → A)MP, 8, 9(388)Выводом, который был сделан из приведенных выше Фактов 4.2 и 4.3является то, что модальный коллапс Coll выводим уже в подсистеме M 0,определяемой тремя принципами AX.1, AX.4, AX.5 (или, альтернативно, AX.1,AX.3, AX.5).
Сами по себе,AX.4 и AX.5 (по крайней мере, формально)нормальны; это возлагает ответственность за модальный коллапс на AX.1.Поскольку AX.1 и AX.4 достаточно для вывода половины Coll, pColl (Факт4.2), то Сентроне задается вопросом, являются ли они также достаточными, чтобывывести оставшуюся половину Т. А поскольку AX.1 и AX.5 достаточно длявывода одной половины модального коллапса, а именно T (Факт 4.3), оназадается вопросом, также ли их достаточно для вывода оставшейся половиныpColl. Последовавшие результаты показывают, что ответ отрицательный в обоихслучаях.Факт 4.4 Схема «фактичности»(T): !A → A(389)не выводима из {AX.1, AX.2, AX.3, AX.4}, даже при использовании полнойклассической логики.126Доказательство: Определим переводA → A*(390)из FORMM в FORM индуктивно следующим образом:– p*: = p, для каждой пропозициональной переменной p(391)– U*: = Т и Т*: = Т(392)– (￢B) *: =￢(B*)(393)– (B ◦ C)*: = B* ◦ C*, для ◦ ∈ {∧ , ∨ , →, ↔}(394)– (!B) *: = Т(395)То есть, дана формула A ∈ FORMM, A* ∈ FORM получается из A путем замены Uна Т и каждой !-подформулы на Т, при этом все остальное не меняется.Доказуемость *-перевода каждой из первых четырех аксиом системы M вклассической пропозициональной логике C проверяется простым способом:AX.1*: (A* →Т) ∧ (B* →C*) → (A* →Т)(396)AX.2*: (A* →Т) ∧ (A* →Т) → (A* →Т)(397)AX.3*: (A* →Т)↔ Т(398)AX.4*: Т(399)Поскольку МР тривиально сохраняется при *-переводе (из A*и (A →B)* ≡ A*→B* ,Сентроне выводит B* по МР), из этого следует, что(♠) для всех A ∈ FORMM: ├М’A ⇒ ├C A*,(400)где M’ является M минус AX.5.Теперь можно легко сделать вывод, что T не выводимо в M.
Действительно,если бы├М’Т(401)имело место, тогда, в частности,├М’ !p → p(402)сохранялось бы, а из (♠) следовало бы, что├C (!p → p)*то есть(403)127├C (Т→ p)(404)что, конечно, не имеет места.Факт 4.5 Схема «частичного коллапса»(pColl): A →!A(405)не выводима из {AX.1, AX.2, AX.5}, даже при использовании полнойклассической логики.Доказательство: Определим переводA →A-(406)из FORMM в FORM по индукции следующим образом:– p−: = p, для каждой пропозициональной переменной p(407)– U−: = Т и Т−: = Т(408)– (￢B)−: =￢(B−)(409)– (B ◦ C)−: = B− ◦ C−, для ◦ ∈ {∧ , ∨ , →, ↔};(410)– (!B)−: = ⊥(411)То есть, учитывая формулу А ∈ FORMM, A− ∈ FORM получена путем замены Uна Т и каждой !-подформулы на ⊥, при сохранении всего остального неизменным.Легко проверить, что −-перевод каждой из аксиом AX.1, AX.2, AX.5 Mстановится доказуемым в классической логике высказываний C:AX.1−: (A− →⊥ ) ∧ (B− →C−) → (A− →⊥ )(412)AX.2−: (A− →⊥ ) ∧ (A− →⊥ ) → (A− →⊥ )(413)AX.5−: ￢(Т→⊥ )(414)Так как правило MP тривиально сохраняется при −-переводе, из этогоследует, что(♣) для всех A ∈ FORMМ: ├М’’A ⇒├C A−(415)где M’’ является M минус AX.3 и AX.4.Теперь можно легко вывести, что (pColl) не выводимо в M.
Действительно,если бы├М’’ A →!A(416)128имело место, тогда, в частности├М’’ p →!p(417)сохранялось бы, и, таким образом, из (♣)├С (p →!p)-(418)то есть├С p →⊥(419)Однако последнее, конечно, неверно.Далее Сентроне предлагает интуиционистскую реконструкцию «Деонтики»Малли.Сентроне замечает, что стоит обратить внимание на то, что при выводе какpColl, так и T (см. Факт 4.2 и 4.3 и дополнительно Факт 4.1) использовались двазакона, истинные в классических системах и отбрасываемые в релевантныхлогиках, а именно законы a fortiori (тем более) и ex falso (исключение лжи);действительно, создается впечатление, что их использования никак нельзяизбежать. Сентроне ссылается на реконструкцию системы Малли, основанную нарелевантной логике, RD, предложенную Локхорстом, говоря о том, что в RD ниодна из двух схем T и pColl не выводима, в то время как значительное числотеорем Малли остаются выводимыми.
В связи с этим она предлагает другуюмодификацию базовой логики для системы Малли, состоящую в заменеклассической логики интуиционистской, в которой не выводим«полныймодальный коллапс», но pColl остается выводимой.Факт 5.1 В полной системе Малли M, основанной на интуиционистскойлогике, то есть в Mint, схема «фактичности»(T): !A → A(420)не выводима.Доказательство. Определим перевод μ из множества FORM M всех LMформул в множество FORM всех L-формул.
Интуитивно, перевод Aμ формулы А∈ FORMM получается посредством замены везде U на Т и ! на двойное отрицани嬬, оставляя все остальное неизменным. Официальное индуктивное определениеAμ, таким образом, следующее:129– pμ: = p, для каждой пропозициональной переменной p(421)– Uμ: = Т и Тμ: = Т(422)– (￢B)μ: =￢(Bμ)(423)– (B ◦ C)μ: = Bμ ◦ Cμ, для ◦ ∈ {∧ , ∨ , →, ↔}(424)– (!B)μ:=￢￢Bμ(425)Теперь просто доказать:(*) для всех A ∈ FORMM: ├Mint A ├Int Aμ(426)Действительно, так как правило модус попенс, очевидно, сохраняется при μпереводе, чтобы проверить (∗) достаточно проверить, что μ-перевод каждой изпяти аксиом Малли является теоремой Int.
Теперь:(AX.1)μ: (Aμ →￢￢Bμ) ∧ (Bμ →Cμ) → (Aμ →￢￢Cμ)(427)(AX.2)μ: (Aμ →￢￢Bμ) ∧ (Aμ →￢￢Cμ) → (Aμ →￢￢(Bμ ∧ Cμ))(428)(AX.3)μ: (Aμ →￢￢Bμ)↔￢￢(Aμ → Bμ)(429)(AX.4)μ: ￢￢Т(430)(AX.5)μ: ￢(Т → ￢￢￢Т)(431)С другой стороны, легко проверить:(i) ├Int (D → E) → (￢￢D →￢￢E)(432)(ii) ├Int ￢￢D ∧ ￢￢E →￢￢(D ∧ E)(433)(iii) ├Int (D →￢￢E)↔￢￢(D → E)(434)(iv) ├Int ￢(Т → ￢￢￢Т) ↔ ￢￢Т и ├Int ￢￢Т ↔ Т.(435)Таким образом, Сентроне приходит к выводу, что:- ├Int (AX.1)μ: действительно, предположим Aμ → ¬¬Bμ и Bμ → Cμ; по (i)последнее дает ¬¬Bμ → ¬¬Cμ, которое, в свою очередь, вместе с первымпредположением, дает Aμ →¬¬Cμ по транзитивности.130- ├Int (AX.2)μ: аналогично, при помощи (ii).- ├Int (AX.3)μ: непосредственно по (iii).- ├Int (AX.4)μ и ├Int (AX.5)μ: непосредственно по (iv).Как только (∗) доказано, доказательство нашего требования под рукой.Предположим, что схема T !А → A выводима в Mint. Тогда подробно├Mint !p → p(436)и, таким образом, по (∗)├Int (!p → p)μ(437)то есть по определению перевода μ:├Int ￢￢p → p.(438)Последнее, однако, неверно.Так выглядит интуиционистская реконструкция Сентроне системы Малли.Далее Сентроне предлагает реконструкцию «Деонтики» путем модификацииаксиом без изменения основы в качестве классической пропозициональнойлогики.По мнению Сентроне, решения в направлении прогонки системы Малличерез модификацию деонтических постулатов при сохранении классической недеонтической логической базы возможны.
Как показывает анализ Сентроне,описанный выше, первый постулат, являющийся виновником модальногоколлапса, в тривиализированной системе Малли – это AX.1. Конечно, AX.3интуитивно также некорректен, по крайней мере, при материальном прочтенииимпликации. В то время как AX.1, по мнению Сентроне, нужноисправить,кажется, что AX.3 невозможно исправить приемлемым образом, поскольку онасмешивает двапонятия(можно сказать: необходимости антецедентаинеобходимости консеквента), которые должны быть разделены.Далее Сентроне представляет в исправленную версию системы Малли,эквивалентную стандартной деонтической модальной системе D.Определение 6.1 Пусть Мм получена из системы Малли M путеммодифицикации следующим образом:131- язык Мм совпадает с языком M, то есть с LM- AX.1 заменена соответствующим правилом вывода R.1:A →!B B→CA →!C(439)- AX.3 отбрасывается.Вспомним стандартную деонтическую нормальную модальную систему D(запись «!» вместо «», чтобы проще сформулировать сравнение).
Язык LDсистемы D является LM минус пропозициональная константа U. Таким образом,каждая формула LD - это формула LM, но не наоборот. Чтобы сделать эти дваязыка сопоставимыми, Сентроне сопоставляет каждой формулеу A из LMформулу A’ из LD, полученную из А путем замены везде U на Т.Аксиомы D те же, что и в C (классическая логика) плюс схемы(K) !(A → B) → (!A →!B)(440)(D) !A→￢!￢A(441)иПравилами вывода D являются модус поненс MP и правило необходимостиRN:А!А(442)Теорема6.2МодифицированнаясистемаМаллиМмэквивалентнастандартной деонтической нормальной модальной системе D в следующемсмысле:1.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
