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