https://ru.wikipedia.org/wiki/Теорема_о_дедукции

Теорему о дедукции никто не называет теоремой Эрбрана. В частности в книге Клини [1973], на которую идет ссылка как на АИ, теоремой Эрбрана (параграф 55) названа совершенно другая теорема, та, на которую, собственно, и стоит кросс-ссылка в английскую википедию.

A ⇒ B означает, логическую операцию импликации.
   (просто такая стрелка - https://en.wikipedia.org/wiki/Mathematical_operators_and_symbols_in_Unicode)

A ⊢ B означает, что формула B выводится из формулы A (в теории L)
   (https://en.wikipedia.org/wiki/Turnstile_(symbol), turnstile ~= "турникет",
   механические ворота, состоящие из вращающихся горизонтальных рычагов, прикрепленных к вертикальной стойке,
   позволяющих проходить одновременно только одному человеку)

⊢ A означает, что формула A доказуема (является теоремой теории L)
   (что такое "теория"?)

Формулировка теоремы для теории высказываний (в моём понимании/пересказе):
Если A ⊢ B и  ⊢ A, то A ⇒ B истинно (доказуемо?).
Если высказывание B выводимо из высказывания A, и высказывание A истинно (доказуемо), то B тоже истинно (доказуемо).
    (что значит "выводимо"? в чём разница между "истинностью" и "доказуемостью"?)

Формулировка теоремы для теории первого порядка:
она ещё более непонятна. Плохо, отвратительно изучать математику по википедии.

https://ru.wikipedia.org/wiki/Дедуктивное_умозаключение

Цепь умозаключений (рассуждений), где звенья (высказывания) связаны между собой логическими выводами.

    (Чем "умозаключение" отличается от "суждения"/"высказывания"?)

«Даже из простейших примеров видно, что задача построения доказательств формул
является сложной и зачастую весьма искусственной.
То же относится и к построению выводов. Попытайтесь, для примера построить вывод
AC ® D ├─ A ® (C ® D).
Для облегчения этой работы сначала доказывают ряд вспомогательных правил вывода,
которыми затем можно заменять целые куски выводов или доказательств.
Ряд наиболее распространенных вспомогательных правил вывода
можно получить из так называемой теоремы дедукции.
Однако и ее формулировка и доказательство в общем случае сложны.»
    (q) https://studopedia.su/14_161201_vivodimost-i-dokazuemost-formul.html

https://en.wikipedia.org/wiki/Herbrand%27s_theorem
https://ru.qwertyu.wiki/wiki/Herbrand's_theorem
https://ru.wikipedia.org/wiki/Теоремы_Эрбрана

«Теорема связывает логику первого порядка с пропозициональной логикой»
    (простите, что? что такое "пропозициональная логика"?)
«Используется для установления существования выводов и доказательств, не используя их построения»
    (простите, что? что такое "построение"? для чего, с какой целью "не используя"?)

https://ru.wikipedia.org/wiki/Теория_моделей
https://ru.wikipedia.org/wiki/Теория_доказательств
https://ru.wikipedia.org/wiki/Теория_алгоритмов (википедия перенаправляет с "Теория вычислений" на "Теория алгоритмов")

1995, Samuel R. Buss, On Herbrand’s Theorem

По сообщению Тарского, он знал и применял этот принцип еще в 1921 году (Alfred Tarski, он же Альфред Тайтельбаум - поляко-американец)
Без доказательств использовалась Эрбраном в 1928 году (Жак Эрбран - француз, разбился в возрасте 23 лет упав со скалы во время скалолазания)
Впервые была явно сформулирована и доказана в 1930 году Эрбраном.
Независимо этот принцип был сформулирован Тарским в 1930 году. (Тарский и Тарьян - это два разных человека)

Отредактировано Лис (2019-11-24 18:28:16)