Возможно, извинения за то, что я задал еще один вопрос о предпосылках, но я был озадачен начальными моментами. Я встречал различные термины, такие как «модальная логика», «временная логика», «логика первого порядка», «логика второго порядка» и «логика высшего порядка».

Что именно означает «логика» в этом контексте? Как мы строго определяем слово «логика»?

Пройдя начальные страницы нескольких книг, я могу примерно прийти к выводу, что «Логика - это способ решить, что следует из того, что важно для разработки языков программирования, и который диктует и облегчает разработку программ для автоматического мышления и понимания программ. чтобы понять о втором пункте в немного разработанной манере.

Теперь перейдем к этой логике.

Являются ли все эти логики, «временная логика», «модальная логика», «логика первого порядка», «логика высшего порядка» независимыми друг от друга, или нам нужно понять несколько из этих логик, чтобы понять несколько других в этой группе? В двух словах, что будет для них необходимым условием? (Было бы здорово, если бы я мог также получить предложения по некоторым материалам.)

PS: большое спасибо за вашу доброту

По сути, логика состоит из двух вещей.

• Синтаксис - это набор правил, которые определяют, что является формулой, а что нет.
• Семантика - это набор правил, которые определяют, какие формулы являются «истинными», а какие «ложными». Для теоретика модели это выражается в соотнесении формул с математическими структурами, в которых они истинны; для теоретика доказательств истина соответствует доказуемости из выбранного набора аксиом с выбранным набором правил (методов) доказательства.

Разница между разными логиками заключается, в основном, в выборе синтаксиса и семантики. Большинство логик являются расширениями логики высказываний или логики первого порядка . В некотором смысле эти расширения можно рассматривать как «добавление дополнительных функций» в логику. Например, временная логика имеет дело с истинами, которые могут меняться со временем.

В целом, эти функции могут быть выражены в более простой логике за счет необходимости писать более длинные формулы. Например, временное понятие «  истинно с этой точки зрения на вечность» можно выразить в порядке первого порядка, добавив параметр времени ко всем вашим предложениям и сказав «Для всех времен  t , если t  больше или равно текущее время, то φ  истинно в момент времени  t . " В некотором смысле вы можете думать об этих логиках как о добавлении библиотек к базовому языку программирования, чтобы вам было проще говорить.$\varphi$$t$$t$$\varphi$$t$

Поскольку в значительной степени все логики основаны на пропозициональной логике и логике первого порядка, я бы рекомендовал узнать о них в первую очередь.

Хотя такие области, как информатика, математика и физика, относительно хорошо организованы, логика имеет хаотическую историю. Его организация действительно сбивает с толку, поэтому я думаю, что важно прочитать историю, чтобы понять плотную структуру поля.

Путь, который вы должны выбрать, будет зависеть от вашего фона и целей .

Что такое логика?

1. Традиционная точка зрения гласит, что логика - это формальная система с формальным языком (синтаксис), семантическим (внешний смысл, восприятие интерпретаторов программ) и набором правил для вывода утверждений из других (подумайте о правилах сокращения программ). Логика рассматривается просто как математический объект.

2. Современная точка зрения гласит, благодаря известному изоморфизму Карри-Говарда, что логика - это система когерентного типа (доказательства - программы, а типы - формулы). Точнее: система правил вывода, использующая теорему об исключении разреза и теорему Черча-Россера / теорему слияния, подразумевающую, что базовая система программирования будет вести себя хорошо.

3. $p, q$

   • $P, Q$$P(x_1, ..., x_n)$$Q(x_1, ..., x_n)$
   • Во логике второго порядка переменная для предикатов становится своего рода функциями, принимающими функции первого порядка. Они ведут себя как функции, принимающие функции первого порядка в качестве аргумента. Например, мы можем иметь предикаты и количественную оценку предикатов.
   • Те же рассуждения для третьего порядка и т. Д. Логики более высокого порядка принимают любой заказ. Подумайте о Haskell и OCaml, которые имеют функции, принимающие функции функций функций и т. Д. В качестве аргумента.

4. В общем, нет единого мнения о том, что такое логика. Некоторые философы используют системы, которые не имеют согласованной системы программирования. На самом деле, я бы сказал, что каждое поле, использующее логику, имеет свою концепцию логики. И большинство математиков, вероятно, не заботятся о том, что такое логика.

Структура поля

История логики слишком велика, поэтому я просто приведу структуру поля. Область формальной логики разделена на: философское, математическое и вычислительное использование. Формальная логика начинается в 19-20 веке.

• Вы должны изучить пропозициональную логику и логику первого порядка первой. Они самые стандартные. Они были созданы, чтобы дать формальное / математическое объяснение старой логике времени Древней Греции.

  • Теория моделей (семантика), изучение математических структур с точки зрения логики
  • Теория доказательств (синтаксис) самостоятельно изучает доказательства как математический объект.

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

• Затем появился Лей Брауэр, который разделил логику на две части:

  • $A$$A \lor \lnot A$
  • Интуиционистская логика - это своего рода логика, отвергающая исключенное среднее и все эквивалентные законы (по техническим и философским причинам я не буду здесь объяснять).

• В другом контексте философы заинтересовались формальной логикой и думали, что она может ответить на философские вопросы (аналитическая философия). Они создали свои собственные независимые логические системы (паранепротиворечивые логики, логики релевантности и модальные логики, такие как деонтические логики, временные логики, эпистемические логики, ...). Модальная логика работает не с истиной, а с такими модальностями, как возможность, необходимость, время, знание. Все они не зависят от вышеуказанной логики.

• $\lambda$

• Компьютерные ученые хотели проверить и доказать громкость систем формально, и кажется, что модальные логики актуальны. Сегодня они используют временную логику и модальную логику для рассуждения о системах (см .: формальные методы, проверка моделей). Системы моделируются с помощью теории автоматов (например) и проверяются с помощью логических инструментов. Это привело к линейной темпоральной логике (LTL) и вычислительной логике дерева (CTL) .

• По той же причине, ученые-компьютерщики хотели проверить правильность и доказать свойства программ. Таким образом, мы изобрели логику Хоара для императивных программ и, в более общем смысле, логику разделения .

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

• Линейная логика также происходит от того, что мы называем субструктурной логикой, отвергающей структурные правила логики. Соответствующая логика и аффинная логика являются примерами для таких систем.

Резюме и выбор пути

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

• Мы можем добавлять или удалять правила для создания вариантов существующих систем:

  • Удалить исключенный-средний: интуиционистская логика
  • Добавить модальности: модальная логика
  • Ограничить противоречие и ослабление: линейная логика
  • Удалить сокращение: аффинная логика
  • Убрать ослабление: соответствующая логика
  • Обращайтесь с отрицанием иначе: паранепротиворечивая логика

• Сначала изучите логику высказываний и логику первого порядка:

  • теория моделей, второго порядка, высшего порядка, если вы заинтересованы в математике
  • теория доказательств, интуиционистская логика, второй порядок, линейная логика, если вы заинтересованы в основах информатики
  • модальная логика, логика Hoare, логика разделения, если вы заинтересованы в проверке систем и программ
  • модальная логика, неклассическая логика в целом, если вы интересуетесь философией

Ссылки (Книги)

Я лично рекомендую смешивать ссылки, если это возможно.

• Математическая логика (Chiswell & Hodges) : очень краткая и простая книга для начала.
• Первый курс по логике (Хедман) : немного похож на предыдущий, но дает больше деталей и учитывает вычислимость.
• Справочник по практической логике и автоматическому рассуждению (Харрисон) : Если вы хотите понять, как некоторые логические концепции реализуются на практике. Больше ориентирован на автоматическое рассуждение.
• Логика в области компьютерных наук (Хут и Райан) : очень понятная и ориентированная на компьютерных специалистов (проверка программ и систем, логика Хоара, практическое использование модальной логики, временная логика, проверка моделей).
• Введение в теорию доказательств (Buss) : введение в теорию доказательств. Это должно быть лучше читать после некоторой общей логики.

Рекомендации (Википедия)

• https://en.wikipedia.org/wiki/Philosophical_logic
• https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
• https://en.wikipedia.org/wiki/Non-classical_logic
• https://en.wikipedia.org/wiki/Intuitionistic_logic
• https://en.wikipedia.org/wiki/Modal_logic
• https://en.wikipedia.org/wiki/Model_theory
• https://en.wikipedia.org/wiki/Proof_theory
• https://en.wikipedia.org/wiki/Linear_temporal_logic
• https://en.wikipedia.org/wiki/Computation_tree_logic
• https://en.wikipedia.org/wiki/Separation_logic
• https://en.wikipedia.org/wiki/Hoare_logic
• https://en.wikipedia.org/wiki/Linear_logic
• https://en.wikipedia.org/wiki/Substructural_logic

Все эти логики находятся под математической логикой .

Математическая логика часто делится на области теории множеств, теории моделей, теории рекурсии и теории доказательств. Эти области имеют общие результаты по логике, особенно по логике первого порядка и определимости. В компьютерных науках (особенно в классификации ACM) математическая логика включает в себя дополнительные темы, не описанные в этой статье; см. Логика в информатике для тех.

Более того, если вы хотите узнать о логике в общих чертах, эта статья может быть полезна.

Логика, изначально означающая «слово» или «что говорят», но обозначающая «мысль» или «разум», является предметом, связанным с наиболее общими законами истины, и в настоящее время, как правило, состоит из систематического изучения. формы действительного вывода. Действительный вывод - это тот, где существует определенная логическая поддержка между допущениями вывода и его заключением.