Русская Википедия:Суждение (математическая логика)
Шаблон:К удалению В математической логике, суждение, умозаключение или утверждение — высказывание или формулировка на метаязыке. Например, типичными суждениями в логике первого порядка являются утверждение, о том, что строка является правильно сформированной формулой (well-formed formula), или утверждение, о том, что предложение истинно. Аналогично, суждение может утверждать вхождение свободной переменной (free variable), в выражение объектного языка или доказательство пропозиции. В общем смысле, суждением, может быть любое индуктивно определяемое утверждение метатеории.
Суждения используются при формальных системах дедукции:
Логическая аксиома выражает суждение, посылки правила вывода формируются как последовательность суждений и заключение также является суждением (таким образом, гипотезы и выводы доказательств являются суждениями). Характерной особенностью вариантов дедукции систем Гильберта (Hilbert-style deduction systems), является отсутствие изменения контекста, в любом из правил вывода, в то время, как и естественная дедукция (natural deduction) и исчисление секвенций содержит ряд правил, позволяющих изменять контекст.
Таким образом, если нас интересует только возможность умозаключения тавтологий, а не гипотетических суждений, то мы можем формализовать систему дедукции Гильберта, так, что правила вывода в ней будут содержать только суждения достаточно простой формы.
С двумя другими системами дедукции дело обстоит иначе: в силу того, что в ряде правил умозаключений, меняется контекст — невозможно формализовать системы, таким образом, чтобы избежать гипотетических суждений, даже если мы хотим использовать данные модели только для доказательства истинности тавтологий.
Благодаря данному базовому разнообразию, между различными исчислениями, допускается следующее различие:
Одна и та же основная мысль, например, теорема о дедукции, должна быть доказана, как метатеорама, в системе дедукции Гильберта, в то время, как в естественной дедукции (natural deduction), может быть сформулирована, в явном виде, как «правило вывода».
В теории типов, аналогично математической логике, используются схожие понятия, что приводит, к появлению связей, между этими двумя областями, например, соответствие Карри — Ховарда. Абстракция, в понятии суждения, в математической логике, может быть использована и в основах теории типов.
Смотрите также
Примечания
- Шаблон:Cite journal
- Dybjer, Peter. "Intuitionistic Type Theory". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
- Шаблон:Cite journal
Внешние ссылки
