Суждение (математическая логика)

Чтобы узнать о других значениях, см. Суждение (значения) .

В математической логике ( суждение или суждение ) или утверждение представляет собой утверждение или высказывание на метаязыке . Например, типичными суждениями в логике первого порядка будет то, что строка представляет собой правильно сформированную формулу или что предложение истинно . Аналогично, суждение может утверждать наличие свободной переменной в выражении объектного языка или доказуемость предложения . В общем, суждением может быть любое индуктивно определяемое утверждение метатеории .

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

Это базовое разнообразие между различными исчислениями допускает такие различия, что одна и та же основная мысль (например, теорема о дедукции ) должна быть доказана как метатеорема в системе дедукции в стиле Гильберта, в то время как она может быть явно объявлена ​​​​как правило вывода в естественной дедукции .

В теории типов используются некоторые аналогичные понятия, как и в математической логике (приводящие к связи между двумя областями, например соответствие Карри-Говарда ). Абстракция понятия суждения в математической логике также может быть использована в основе теории типов.

См. также

• Просто типизированное лямбда-исчисление
• Математическая логика

Ссылки

• Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Северный журнал философской логики . 1 (1): 11–60. ISSN   0806-6205 .
• Дюбьер, Питер. «Интуиционистская теория типов» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
• Пфеннинг, Фрэнк ; Дэвис, Роуэн (август 2001 г.). «Судебная реконструкция модальной логики». Математические структуры в информатике . 11 (4): 511–540. CiteSeerX   10.1.1.43.1611 . дои : 10.1017/S0960129501003322 . S2CID   263699107 .

Внешние ссылки

• «Суждения в формальных системах» . Всё ₂ .
• Пфеннинг, Фрэнк (весна 2004 г.). «Естественная дедукция» (PDF) . 15-815 Автоматическое доказательство теорем .
• Мартин-Лёф, Пер (1983). «О значении логических констант и обоснованиях логических законов» . Лекции в Сиене .