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

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

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

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

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

Смотрите также

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

Рекомендации

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

внешняя ссылка

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