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