В математической логике , суждение (или суждение ) или утверждение является утверждение или дикция в метаязыке . Например, типичными суждениями в логике первого порядка будет то, что строка является правильно сформированной формулой или что предложение истинно . Точно так же суждение может утверждать наличие свободной переменной в выражении объектного языка или доказуемость предложения . В общем, суждение может быть любым индуктивно определяемым утверждением в метатеории .
Суждения используются при формализации систем дедукции : логическая аксиома выражает суждение, предпосылки правила вывода формируются как последовательность суждений, и их вывод также является суждением (таким образом, гипотезы и выводы доказательств являются суждениями). Характерной особенностью вариантов систем дедукции в стиле Гильберта является то, что контекст не изменяется ни в одном из их правил вывода, в то время как как естественный вывод, так и исчисление последовательностей содержат некоторые правила, изменяющие контекст. Таким образом, если мы заинтересованы только в выводимости из тавтологийа не гипотетические суждения, то мы можем формализовать систему дедукции в стиле Гильберта таким образом, чтобы ее правила вывода содержали только суждения довольно простой формы. То же самое нельзя сделать с двумя другими системами дедукции: поскольку контекст изменяется в некоторых из их правил умозаключений, они не могут быть формализованы так, чтобы можно было избежать гипотетических суждений - даже если мы хотим использовать их только для доказательства выводимости тавтологий. .
Это базовое разнообразие между различными исчислениями допускает такое различие, что одна и та же основная мысль (например, теорема дедукции ) должна быть доказана как метатеорема в системе дедукции гильбертова, в то время как ее можно явно объявить как правило вывода в естественной дедукции .
В теории типов используются некоторые аналогичные понятия, как и в математической логике (вызывающие связи между двумя областями, например, соответствие Карри – Ховарда ). Абстракция в понятии суждения в математической логике также может быть использована в качестве основы теории типов.
См. Также [ править ]
Ссылки [ править ]
- Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Северный журнал философской логики . 1 (1): 11–60. ISSN 0806-6205 .
- Дибьер, Питер. «Интуиционистская теория типов» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
- Пфеннинг, Франк ; Дэвис, Роуэн (август 2001 г.). «Оценочная реконструкция модальной логики». Математические структуры в информатике . 11 (4): 511–540. CiteSeerX 10.1.1.43.1611 . DOI : 10.1017 / S0960129501003322 . CS1 maint: обескураженный параметр ( ссылка )
Внешние ссылки [ править ]
- «Суждения в формальных системах» . Все 2 .
- Пфеннинг, Франк (весна 2004 г.). «Естественная дедукция» (PDF) . 15-815 Автоматическое доказательство теорем .
- Мартин-Лёф, Пер (1983). «О значении логических констант и обоснованиях логических законов» . Сиенские лекции .
