Суждение (математическая логика)
 | Эту статью предлагается удалить. |
В математической логике, суждение, умозаключение или утверждение — высказывание или формулировка на метаязыке. Например, типичными суждениями в логике первого порядка являются утверждение, о том, что строка является правильно сформированной формулой[англ.], или утверждение, о том, что предложение истинно. Аналогично, суждение может утверждать вхождение свободной переменной[англ.], в выражение объектного языка или доказательство пропозиции. В общем смысле, суждением, может быть любое индуктивно определяемое утверждение метатеории.
Формальная система
[править | править код]Суждения используются при формальных системах дедукции: логическая аксиома выражает суждение, посылки правила вывода формируются как последовательность суждений и заключение также является суждением, таким образом, гипотезы и выводы доказательств являются суждениями.
Характерной особенностью вариантов дедукции систем Гильберта[англ.], является отсутствие изменения контекста, в любом из правил вывода, в то время, как и натуральный вывод и исчисление секвенций содержит ряд правил, позволяющих изменять контекст.
Таким образом, если нас интересует только возможность умозаключения тавтологий, а не гипотетических суждений, то мы можем формализовать систему дедукции Гильберта, так, что правила вывода в ней будут содержать только суждения достаточно простой формы.
С двумя другими системами дедукции дело обстоит иначе: в силу того, что в ряде правил умозаключений, меняется контекст — невозможно формализовать системы, таким образом, чтобы избежать гипотетических суждений, даже если мы хотим использовать данные модели только для доказательства истинности тавтологий.
Благодаря данному базовому разнообразию, между различными исчислениями, допускается следующее различие:
Одна и та же основная мысль, например, теорема о дедукции, должна быть доказана, как метатеорама, в системе дедукции Гильберта, в то время, как в натуральном выводе, может быть сформулирована, в явном виде, как «правило вывода».
В теории типов, аналогично математической логике, используются схожие понятия, что приводит, к появлению связей, между этими двумя областями, например, соответствие Карри — Ховарда. Абстракция, в понятии суждения, в математической логике, может быть использована и в основах теории типов.
См. также
[править | править код]Литература
[править | править код]- Martin-Löf, Per (1996). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11—60. ISSN 0806-6205.
- 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 10.1.1.43.1611. doi:10.1017/S0960129501003322.
Внешние ссылки
[править | править код]- Judgments in formal systems. Everything2.
- Pfenning, Frank. Natural Deduction // 15-815 Automated Theorem Proving. — Spring 2004.
- Martin-Löf. On the meaning of the logical constants and the justifications of the logical laws. Siena Lectures (1983).
