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

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

Суждения используются при формальных системах дедукции:

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

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

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

Благодаря данному базовому разнообразию, между различными исчислениями, допускается следующее различие:

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

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

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

Примечания

Martin-Löf, Per (1996). (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11—60. ISSN .
Dybjer, Peter. "Intuitionistic Type Theory". In Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy.
Pfenning, Frank (August 2001). "A judgmental reconstruction of modal logic". Mathematical Structures in Computer Science (англ.) . 11 (4): 511—540. CiteSeerX . doi : .