Обсуждение:Теорема дедукции

разница?

Мне трудно понять, чем теорема дедукции отличается от правила вывода условного доказательства в исчислении высказываний. У нас есть:

«если ф |-- ф, то |-- ф -> ф» ( Теорема_дедукции )

против

«Если ψ может быть выведено при принятии гипотезы φ, мы можем вывести ( φ → ψ )». Пропозициональное исчисление

Я не могу не думать, что это синонимы. Может быть, проблема в том, что первое дано в гораздо более формальной нотации, чем второе. Поможет ли мне, как полагают люди, если кто-то переведет последнее в более символическую форму? (Это вообще возможно?)

В любом случае, здесь должно быть что-то тонкое (по крайней мере, учитывая мой бэкграунд). Помогите? --Ryguasu 19:31, 17 мая 2005 (UTC) [ ответить ]

Теорема дедукции применяется к аксиоматическим системам, а правило условного доказательства — к естественным системам дедукции. Они аналогичны, но различны. Теорема дедукции — это не правило формальной системы; это свойство отношения выводимости системы, абстрактно истолкованное. Nortexoid 05:33, 2 апреля 2007 (UTC) [ ответить ]
На самом деле теорема о дедукции глубоко релевантна для аксиоматических систем, поскольку она обосновывает правило modus ponens: теорема о дедукции «говорит», что стрелка глубоко связана с понятием вывода из предположений (которое отсутствует в аксиоматических системах). Таким образом, говоря, что у вас есть теорема о дедукции в аксиоматической системе, вы обосновываете modus ponens как правило, поскольку вы показали, что стрелка сохраняет след вывода. И затем, посредством композиции выводов, вы знаете, что если у вас есть доказательство, скажем, A, у вас есть доказательство B (предполагая, что у вас есть доказательство A -> B). Вот почему это релевантно в аксиоматических системах. Но если вы рассматриваете, например, системы естественной дедукции, это больше не релевантно, поскольку у вас уже есть понятие вывода из предположений. Затем теорема о дедукции «интернализуется» в правилах для стрелки. Ianshil (обсуждение) 14:49, 13 февраля 2017 (UTC) [ ответить ]
В чем разница между «глубоко релевантным» и просто «релевантным»? — Предыдущий неподписанный комментарий добавлен 184.179.86.135 (обсуждение) 14:21, 3 июля 2018 (UTC)[ отвечать ]

Доказательство

В средней части доказательства:

  • Q→((Q→R)→R) 8. вычет из 5 в 7 QED

Разве не достаточно было бы использовать 5 и 7 вместо 5, 6 и 7, потому что 6 не появляется в этой строке, чтобы добраться до этой последней строки? Кроме того, 6 уже используется строкой выше. Разве этого недостаточно? Действительно, очень ясная ваша статья, и я понимаю здесь больше, чем в Deduktionstheorem Cheers.--de:Benutzer:Roomsixhu —Предыдущий неподписанный комментарий был добавлен 87.187.55.111 ( talk ) 02:20, 2 апреля 2007 (UTC). [ ответить ]

Я только что посмотрел на это во второй раз: строка 6 вытекает из гипотезы, строка 5, и аксиомы 1, строка 4, таким образом, вам нужно запомнить только гипотезу, а не аксиому, и вы можете ее опустить. Но строка 7 необходима, потому что она объединена, а не аксиоматична. Cheers de:Benutzer:Roomsixhu

Я сказал «вывод от 5 до 7», а не «вывод 5 и 7», потому что все шаги от 5 до 7, т. е. шаги 5, 6 и 7, зависят от гипотезы 5. И они используются при выводе заключения 7. Шаг 7 зависит от шага 6, который зависит от шага 5. В любом случае, форма этого виртуального правила вывода фиксирована и не может изменяться в зависимости от особенностей частного случая. JRSpriggs 09:43, 2 апреля 2007 (UTC) [ ответить ]
Спасибо еще раз: я только это заметил, потому что 6 зависит от 5 и аксиомы 1 (строка 4), а 8 зависит от 5, 6 и 7, но 6 зависит от 5 и 4, а 4 — это аксиома. В моем исчислении у вас есть основные формулы и основные правила, и вы можете опустить основные формулы, это, кажется, отличается от вашего исчисления, в котором есть аксиомы. Но я не нашел в нашей немецкой википадии четкого описания этого. Я все еще буду практиковаться, чтобы стать более уверенным. Пункт 3.2 — простой пример того, как получить дополнительные «мета»-формулы из основной решетки. --de:Benutzer:Roomsixhu —Предыдущий комментарий без знака был добавлен 87.187.55.111 ( talk ) 13:24, 2 апреля 2007 (UTC).[ отвечать ]

Ссылки на доказательства Эрбрана и Тарского и т. д.

Я уже слышал это раньше, но я с подозрением отношусь к этому, потому что никто никогда не дает доказательств. Где доказательство Эрбрана и для какой системы? Где доказательство Тарского и для какой системы? И откуда известно, что ни один из них не получил его от другого, напрямую или косвенно. И откуда известно, что никто не сделал этого раньше? Tyro13 ( talk ) 18:46, 2 ноября 2014 (UTC) [ ответить ]

Для справки, отрывок, на который сделана ссылка во введении к статье, следующий:

Хотя математикам на протяжении столетий казалось «очевидным», что доказательство B из A в сочетании с набором теорем равносильно доказательству импликации A  →  B , основанной только на этих теоремах, Эрбрану и Тарскому пришлось (независимо) показать, что это логически верно в общем случае.

Действительно, я бы счёл это утверждение не только необоснованным, но и откровенно сомнительным, поскольку первые аксиомы (P1–P3) системы дедукции в стиле Гильберта — это именно то, что нужно для теоремы дедукции — зачем выбирать именно эти аксиомы, если не предполагается устанавливать гипотетические рассуждения посредством теоремы дедукции? Тарский и Эрбран оба родились в первом десятилетии 1900-х годов, поэтому крайне маловероятно, что какая-либо их работа могла бы иметь достаточно времени, чтобы повлиять на Гильберта в чём-то столь фундаментальном, как аксиомы пропозициональной логики.

С другой стороны, история, рассказанная в системе вывода в стиле Гильберта, кажется, не проверяется, когда я заглядываю в книгу ван Хейеноорта « От Фреге до Гёделя» . Аксиомы Гильберта для импликации излагаются в этой книге несколько раз (один текст Колмогорова, один текст самого Гильберта), но центральная аксиома P3 не присутствует ни в одной из презентаций. Вместо этого список аксиом импликации Гильберта выглядит так: ( C → ( B → A ) ) → ( ( C → B ) → ( C → A ) ) {\displaystyle (C\to (B\to A))\to ((C\to B)\to (C\to A))}

  1. A → ( B → A ) {\displaystyle A\to (B\to A)}
  2. ( A → ( A → B ) ) → ( A → B ) {\displaystyle (A\to (A\to B))\to (A\to B)}
  3. ( A → ( B → C ) ) → ( B → ( A → C ) ) {\displaystyle (A\to (B\to C))\to (B\to (A\to C))}
  4. ( B → C ) → ( ( A → B ) → ( A → C ) ) {\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}

Место, где появляется , находится в Begriffsschrift Фреге , и Фреге перечисляет его (van Heijenoort, стр. 29) вместе с теми тремя предложениями из девяти, «составляющих ядро ​​представления», которые могут быть записаны с использованием только импликации; легко интерпретировать это описание как придание этим формулам статуса аксиом. ( Hilbert, D.; Ackermann, W. (1950). Mathematical Logic (Second ed.). New York: Chelsea. стр. 29. ( C → ( B → A ) ) → ( ( C → B ) → ( C → A ) ) {\displaystyle (C\to (B\to A))\to ((C\to B)\to (C\to A))} A → ( B → A ) {\displaystyle A\to (B\to A)} ( D → ( B → A ) ) → ( B → ( D → A ) ) {\displaystyle (D\to (B\to A))\to (B\to (D\to A))} ), по сути, с 1928 года, действительно дает систему из шести аксиом для пропозициональной логики и приписывает ее Фреге. Но не является аксиомой ни в одном из них, и Фреге фактически дает ее доказательство в Begriffsschrift! A → A {\displaystyle A\to A}

Так что да, история этого кажется довольно неинтуитивной. Нужен правильный источник! 130.243.68.163 (обсуждение) 17:07, 18 декабря 2019 (UTC) [ ответить ]

Дополнительные данные по этому вопросу:

  1. Мендельсон (ISBN 0-534-06624-0) дает ссылку на Эрбрана на ( Herbrand, J. (1930). «Recherches sur la theorie de laдемонстрировать». Travaux de la Soc. des Sci. et des Lettres Varsovie, III 33 : 33–160 .​), по-видимому, переведено как ( Herbrand, J. (1971). Logical Writings . Harvard & Reidel.). Мендельсон делает это приписывание только в контексте теоремы о выводе исчисления высказываний; для теоремы о выводе исчисления предикатов он вообще не дает никакого приписывания.
  2. Традиция Фреге на самом деле могла быть использована для установления нижних границ открытия теоремы дедукции. Поскольку у Фреге были все аксиомы, необходимые для теоремы дедукции (исчисления высказываний), но также включенные в качестве «аксиомы» [1], даже несмотря на то, что доказательство этого было бы простым применением теоремы дедукции, мы можем сделать вывод, что на самом деле у него не было теоремы дедукции. Гильберт и Аккерман (издание 1928 года или только издание 1938 года?) приписывают упрощенную систему аксиом в стиле Фреге Лукасевичу (не Лукасевичу и Тарскому совместно), так что где-то в течение этого полувека было обнаружено доказательство (хотя это не обязательно должно было быть посредством теоремы дедукции). ( D → ( B → A ) ) → ( B → ( D → A ) ) {\displaystyle (D\to (B\to A))\to (B\to (D\to A))} ( D → ( B → A ) ) → ( B → ( D → A ) ) {\displaystyle (D\to (B\to A))\to (B\to (D\to A))}

Ссылке на Herbrand, вероятно, понадобится номер страницы, прежде чем ее вернут в статью. И даже тогда ее, вероятно, следует поместить не в начало статьи, а в раздел об истории теоремы. 130.243.68.37 (обсуждение) 14:15, 19 декабря 2019 (UTC) [ ответить ]

Ссылки

  1. ^ Понятие аксиомы не определено ясно в Begriffsschrift, но в 1928 году Гильберт и Аккерман явно представляют формулы Фреге как систему аксиом для исчисления высказываний.

Турникеты?

В большей части этой статьи используется обычный турникет (символ) . Но затем, в разделе (довольно запутанно) под названием Теорема дедукции в логике предикатов , мы читаем, что ⊢ {\displaystyle \vdash }

Теорема дедукции верна также в логике первого порядка ... символ ├ означает «является синтаксическим следствием».

ну, хм. Но теперь я запутался на нескольких уровнях: мы говорим о логике первого порядка или о логике предикатов ? Мы не можем иметь и то, и другое, не так ли?

Теперь я всегда думал, что turnstyle всегда означает "является синтаксическим следствием .", так почему же в этом разделе используется другой вид turnstyle ├? Означает ли это, что более ранние turnstyle не были синтаксическими следствиями? Какой-то другой вид вывода ? Или это все просто плохое форматирование и плохое редактирование в этой статье? Или это на самом деле разные turnstyle с разными, эммм... значениями? ⊢ {\displaystyle \vdash }

Я имею в виду, если я посмотрю на Логическое следствие#Модальные счета , то получу описание фреймов Крипке. Обсуждается ли в этой статье смысл вывода — может ли это быть одним из видов выводов? Я почти уверен, что как только мы погрузимся в глубь модальной логики, мы найдем некоторые промежуточные логики , которые не имеют ослабления в качестве аксиомы, поскольку не способны доказать теорему дедукции. Так что даже сама концепция вывода для этих логик ведет в трясину — некоторая ясность в этой статье действительно очень помогла бы.

В любом случае, было бы неплохо, если бы в статье была ссылка на турникет (символ) и объяснялось, что это на самом деле означает вывод , а конкретно синтаксический вывод, а не что-то еще (?) (и, возможно, объяснялось, что «синтаксический вывод» означает «вы можете получить доказательство этого»), иначе мы останемся в озоне... 67.198.37.16 ( обсуждение ) 05:50, 31 августа 2016 (UTC) [ ответить ]

Два символа турникета должны быть одинаковыми. К сожалению, они по-разному отображаются в TeX и HTML.
Пропозициональная логика является подмножеством предикатной логики. Поэтому большинство вещей, сказанного о пропозициональной логике, также применимы к предикатной логике (также называемой логикой первого порядка). JRSpriggs ( talk ) 19:46, 31 августа 2016 (UTC) [ ответить ]
Вы уклоняетесь от основных вопросов. Статья — уродливый беспорядок, мешанина, которая непонятна, даже если вы уже знаете изрядную долю логики. Она остро нуждается в ремонте и внимании того, кто действительно разбирается в теме. 67.198.37.16 ( обсуждение ) 04:28, 1 сентября 2016 (UTC) [ ответить ]

Аксиома 1 ???

Раздел под названием Примеры дедукции — самый первый раздел после лида — мог бы использовать кучу слов, чтобы объяснить, что происходит. Итак, я узнаю так называемую «аксиому 1», потому что это первая аксиома в системе Гильберта — ну, за исключением того, что это на самом деле схема аксиом , а не аксиома, и на самом деле это схема аксиом 2, а не 1... похоже, что «аксиома 1» — это просто какая-то случайная фраза, придуманная только для этой статьи, а не реальная вещь. Путаница между аксиомами и схемой аксиом также не внушает доверия.

Я также запутался в отступах. Стиль явно НЕ секвенциального исчисления , поэтому я предполагаю, что это должен быть стиль Гильберта. Если так, можем ли мы так сказать и дать викиссылку на систему Гильберта ? Однако в статье о системе Гильберта не говорится об отступах... и затем следующий раздел противоречит всему:

Следующий раздел называется Виртуальные правила вывода , который объясняет отступы, а также призывает к необходимости трех правил вывода. Теперь, система Гильберта имеет только одно правило вывода, так что эта новая система вывода, очевидно, является какой-то другой системой. Если я перейду к правилу вывода , я на самом деле не вижу, чтобы эти три правила были там названы. Они также не появляются в Списке правил вывода , так что они кажутся какими-то исключительными или экстраординарными правилами, живущими в своем собственном маленьком особом облаке. Поэтому их называют «виртуальными»? «виртуальный» — это фактический термин, используемый в литературе? Если я гуглю фразу «виртуальное правило вывода», я не получаю ничего многообещающего, так что этот термин — какой-то оригинальный неологизм, придуманный специально для этой статьи??? Это немного сбивает с толку.

Тогда первое правило вывода называется "гипотеза", но, насколько я понимаю, это правило не допускается в (например) линейной логике . Похоже, это некая форма "ослабления", также известная как монотонность вывода , которая не допускается во множестве различных логик. Soo .. Является ли "гипотеза" на самом деле тем же самым, что и ослабление, или это что-то, что как-то отличается??? В любом случае, похоже, что теорема дедукции может быть верна только в некоторых логиках, а не во всех...

Все эти вопросы меня в значительной степени сбивают с толку. Я имею в виду, если я затуманиваю глаза, я чувствую, что смутно понимаю, но детали совершенно сбивают с толку; я не могу сказать, что действительно, когда это действительно, и при каких обстоятельствах что может быть вызвано, где или когда. 67.198.37.16 ( talk ) 06:18, 31 августа 2016 (UTC) [ ответить ]

Схема аксиом Гильберта P1 выводится из его схем аксиом P2 и P3. Многие системы ее опускают.
Я не вижу причин считать систему Гильберта единственно верной и окончательной, как это, судя по всему, делаете вы.
То, как HTML и Tex обрабатываются в Википедии, затрудняет выполнение определенных видов отступов. JRSpriggs ( обсуждение ) 19:57, 31 августа 2016 (UTC) [ ответ ]
Ну, я не думаю, что это как-то связано с системами Гильберта. Так что мы полностью согласны, в этом. Но я думаю, что вы уклоняетесь от основных вопросов. Статья — уродливый беспорядок, мешанина, которая непонятна, даже если вы уже знаете изрядную долю логики. Она остро нуждается в исправлении и внимании со стороны того, кто действительно разбирается в теме. Она читается как любительская попытка объяснить концепцию — полная неверных указаний и неверных утверждений и неопределенных терминов, выдуманной терминологии. Это ужасно. 67.198.37.16 ( обсуждение ) 04:31, 1 сентября 2016 (UTC) [ ответить ]


Я бы удалил большинство примеров, которые кажутся мне очень своеобразными, и немного упростил бы прозу. — Карл ( CBM  ·  talk ) 11:02, 1 сентября 2016 (UTC) [ ответить ]

Вывод полезных теорем

См. Теорема о дедукции#Полезные теоремы . В качестве примера того, насколько теорема о дедукции упрощает доказательства, я выведу полезные теоремы как с теоремой о дедукции, так и без нее. Чтобы показать:

А → А
( Б → В )→(( А → В )→( А → В ))
( А →( Б → В ))→( Б →( А → В ))
( А → Б )→(( Б → В )→( А → В ))
( А → ( А → С ))→ ( А → С )

С помощью теоремы о дедукции:

1. ___ Гипотеза
2. Вычет А → А
3. ___ B → C гипотеза
4. ______ Гипотеза А → Б
5. _________ Гипотеза
6. _________ B modus ponens 5,4
7. _________ C modus ponens 6,3
8. ______ A → C вычет
9. ___( A → B )→( A → C ) вычитание
10. ( B → C )→(( A → B )→( A → C )) вычитание
11. ___ A →( B → C ) гипотеза
12. ______ Б гипотеза
13. _________ Гипотеза
14. _________ B → C modus ponens 13,11
15. _________ C modus ponens 12,14
16. ______ A → C вычет
17. ___ B →( A → C ) вычет
18. ( А →( Б → В ))→( Б →( А → В )) вычитание
19. ___ Гипотеза А → Б
20. ______ B → C гипотеза
21. _________ Гипотеза
22. _________ B modus ponens 21,19
23. _________ C modus ponens 22,20
24. ______ A → C вычет
25. ___( B → C )→( A → C ) вычитание
26. ( А → Б )→(( Б → В )→( А → В )) вычитание
27. ___ A →( A → C ) гипотеза
28. ______ Гипотеза
29. ______ A → C modus ponens 28,27
30. ______ C modus ponens 28,29
31. ___ A → C вычет
32. ( А →( А → С ))→( А → С ) вычет

Без теоремы дедукции:

1. B →( A → B ) дано
2. ( А →( Б → В ))→(( А → В )→( Б → В )) дано
3. ( А →(( Б → А )→ А ))→(( А →( Б → А ))→( А → А )) 2
4. А →(( Б → А )→ А ) 1
5. ( А →( В → А ))→( А → А ) modus ponens 4,3
6. А →( Б → А ) 1
7. A → A modus ponens 6,5 ПЕРВЫЙ
8. [( А →( Б → В ))→(( А → В )→( А → В ))]→(( Б → В )→[( А →( Б → В ))→(( А → В )→( А → В ))]) 1
9. ( B → C )→[( A →( B → C ))→(( A → B )→( A → C ))] modus ponens 2,8
10. (( Б → В )→[( А →( Б → В ))→(( А → В )→( А → В ))])→([( Б → В )→( А →( Б → В ))]→[( Б → В )→(( А → В )→( А → В ))]) 2
11. [( B → C )→( A →( B → C ))]→[( B → C )→(( A → B )→( A → C ))] modus ponens 9,10
12. ( Б → С )→( А →( Б → С )) 1
13. ( B → C )→(( A → B )→( A → C )) modus ponens 12,11 СЕКУНД.
14. (( А → Б )→( А → В ))→(( Б →( А → В ))→( Б →( А → В ))) 13
15. [(( А → Б )→( А → В ))→(( Б →( А → В ))→( Б →( А → В )))]→([( А →( В → В ))→(( А → Б )→( А → В ))]→[( А →( В → В ))→(( Б →( А → В ))→( Б →( А → В )))]) 13
16. [( А →( B → C ))→(( A → B )→( A → C ))]→[( A →( B → C ))→(( B →( A → B ))→ ( B →( A → C )))] modus ponens 14,15
17. ( A →( B → C ))→(( B →( A → B ))→( B →( A → C ))) modus ponens 2,16
18. [( А →( Б → С ))→(( Б →( А → В ))→( Б →( А → С )))]→([( А →( Б → С ))→( Б →( А → В ))]→[( А →( Б → С ))→( Б →( А → С ))]) 2
19. [( A →( B → C ))→( B →( A → B ))]→[( A →( B → C ))→( B →( A → C ))] modus ponens 17,18
20. ( Б →( А → Б ))→[( А →( Б → С ))→( Б →( А → Б ))] 1
21. ( A →( B → C ))→( B →( A → B )) modus ponens 1,20
22. ( A →( B → C ))→( B →( A → C )) modus ponens 21,19 ТРЕТИЙ
23. [( Б → В )→(( А → В )→( А → В ))]→[( А → В )→(( Б → В )→( А → В ))] 22
24. ( A → B )→(( B → C )→( A → C )) modus ponens 13,23 ЧЕТВЕРТЫЙ
25. ( А →( А → С ))→(( А → А )→( А → С )) 2
26. [( А →( А → С ))→(( А → А )→( А → С ))]→[( А → А )→(( А →( А → С ))→( А → С ))] 22
27. ( A → A )→(( A →( A → C ))→( A → C )) modus ponens 25,26
28. ( А →( А → С ))→( А → С ) modus ponens 7,27 ПЯТЫЙ

Хотя доказательство без теоремы о дедукции оказалось менее точным, во многих случаях эти шаги были гораздо сложнее (и менее очевидны). JRSpriggs ( talk ) 21:48, 23 октября 2018 (UTC) [ ответить ]

Показать, что вместо аксиомы 2 можно использовать две другие теоремы.

1. B →( A → B ) дано
2. ( А → Б )→(( Б → В )→( А → В )) дано
3. ( А →( А → С ))→( А → С ) дано
4. ( А →( Б → В ))→((( Б → В )→( А → В ))→( А →( А → В ))) 2
5. [( А → Б )→(( Б → В )→( А → В ))]→([(( Б → В )→( А → В ))→( А →( А → В ))]→[( А → Б )→( А →( А → В ))]) 2
6. [(( B → C )→( A → C ))→( A →( A → C ))]→[( A → B )→( A →( A → C ))] modus ponens 2,5
7. [( А →( Б → С ))→((( Б → С )→( А → С ))→( А →( А → С )))]→(([(( Б → С )→( А → С ))→( А →( А → С ))]→[( А → В )→( А →( А → С ))])→[( А → ( Б → С ))→(( А → В ) → ( А → С )))]) 2
8. ([(( B → C )→( A → C ))→( A →( A → C ))]→[( A → B )→( A →( A → C ))])→[( A →( B → C ))→(( A → B )→( A →( A → C )))] modus ponens 4,7
9. ( A →( B → C ))→(( A → B )→( A →( A → C ))) modus ponens 6,8
10. (( А → Б )→( А →( А → С )))→[(( А →( А → С ))→( А → С ))→(( А → Б )→( А → С ))] 2
11. [( А →( Б → В ))→(( А → В )→( А →( А → В ) ))]→([(( А → В )→ ( А → В )))→[(( А → ( А → В ) ) → ( А → В ) ) → (( А → В )→( А → В ))]]→[( А →( Б → В ))→[(( А → ( А → В ))→( А → В )) → (( А → В )→( А → В ))]]) 2
12. [(( A → B )→( A →( A → C )))→[(( A →( A → C ))→( A → C ))→(( A → B )→( A → C ))]]→[( A →( B → C ))→[(( A →( A → C ))→( A → C ))→(( A → B )→( A → C ))] ] модус поненс 9,11
13. ( A →( B → C ))→[(( A →( A → C ))→( A → C ))→(( A → B )→( A → C ))] modus ponens 10,12
14. (( А →( А → С ))→( А → С ))→(( А →( Б → С ))→(( А →( А → С ))→( А → С ))) 1
15. ( A →( B → C ))→(( A →( A → C ))→( A → C )) modus ponens 3,14
16. [( А →( Б → В ))→[(( А →( А → В ))→( А → В ))→(( А → В )→( А → В ))]]→([( А →( Б → В ))→(( А →( А → В ))→( А → В ))]→[( А →( Б → В ))→[( А →( Б → В ))→(( А → В )→( А → В ))]]) 9
17. [( А →( B → C ))→(( A →( A → C ))→( A → C ))]→[( A →( B → C ))→[( A →( B → C ))→(( A → B )→( A → C ))]] modus ponens 13,16
18. ( A →( B → C ))→[( A →( B → C ))→(( A → B )→( A → C ))] modus ponens 15,17
19. (( А →( Б → В ))→[( А →( Б → В ))→(( А → В )→( А → В ))])→[( А →( Б → В ))→(( А → В )→( А → В ))] 3
20. ( A →( B → C ))→(( A → B )→( A → C )) modus ponens 18,19 QED

-- JRSpriggs ( обсуждение ) 17:53, 29 октября 2018 (UTC) [ ответить ]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Talk:Deduction_theorem&oldid=1201418906"