Дедуктивный аргумент, в котором четко указаны каждый шаг и посылка?

Есть ли в философии слово/термин, описывающий аргумент, в котором все посылки и правила вывода из этих посылок сформулированы явно, так что это может проверить даже компьютер? Я знаю, что, например, в логике высказываний можно легко доказать логическое следствие, проверив, верна ли формула во всех случаях, когда формулы теории Тистинны (например, по таблице истинности). Есть даже второй вариант доказательства, формально использующий аксиоматическую систему Гильберта. Первое доказательство неформальное, второе доказательство формальное, но оба одинаково «строгие». Существует ли слово/термин, которым философы или математики называют аргумент или доказательство, которое является «максимально строгим» (что означает, что все указано явно и может быть проверено компьютером, если его переписать на языке программирования)? Существует ли также слово/термин для «более слабой» формы аргумента или доказательства (имеется в виду, что не все шаги рассуждения явны — даже в исчислении Гильберта, если мы не указываем явно все используемые нами правила, я бы назвать его в этом смысле «более слабым» доказательством)?

Я обнаружил, что такие типы аргументов называются априорными аргументами или дедуктивными аргументами. Однако эти термины не описывают аргумент, в котором каждый шаг необходимо явно указать или записать на бумаге - поэтому может быть место для двусмысленности, если человек ничего не знает о логике высказываний или любой другой системе.

В следующих предметных областях есть раздел, который они преподают в соответствии с тем, что считается логикой: философия, психология, риторика (например, в современном праве или политике), математика и информатика. Я упоминаю об этом, потому что термин «логика» часто понимается неправильно и может означать разные вещи в этих контекстах. Некоторые термины НЕ используются повсеместно. Одни и те же слова могут иметь разное значение в зависимости от того, какая из перечисленных тем преподает так называемую логику. Дедуктивное рассуждение — это более широкий набор того, что подпадает под логику. Дедуктивное рассуждение касается уверенности, а не других видов рассуждений.
@Logikal, использование терминологии вопрошающим вполне уместно. Пожалуйста, прекратите это с навязчивой настойчивостью, что все в этой области ошибаются.
@ Пол Росс, я не настаивал на том, что все в поле ошибаются. Я ясно и часто указываю, что вся логика не является математической. У некоторых людей сложилось впечатление, что логика есть логика, и это все математика, которую мне постоянно приходится исправлять. Многие области логики не идентичны, что, кажется, продвигают математики. Я не математик, и меня не учили так, как я часто здесь вижу. Философия и математика не идентичны. Логика — слишком расплывчатый термин, чтобы использовать его отдельно. Если кто-то имеет в виду математическую логику, он должен выразить, что это именно математическая логика, а не логика.
@Logikal Довольно иронично, что, пытаясь исправить других в вопросах логики, вы пишете «вся логика не является математикой», когда вы намереваетесь сказать, что логика - это не только математика.
@Eliran, я вижу, что ты там сделал. К сожалению, я написал в определенном порядке, ПОТОМУ ЧТО многие люди уже ДУМАЮТ: «Вся логика математическая». Я часто прибегаю к аристотелевской логике, чтобы показать, что контекст терминов может различаться, и привести контрпримеры. Однако здесь я не помню, чтобы я говорил, что все в какой-то области неправы, и я не поправлял людей в вопросах логики. Я прокомментировал идею дедуктивного рассуждения в целом ОП, который, кажется, думает только математически. Все рассуждения - это не математика, это моя точка зрения. Здесь ни слова о коррекции. Информация, которая может отличаться, показывается оператору для ознакомления.

Ответы (2)

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

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

Не все формальные аргументы или даже все правильно построенные формальные доказательства естественного вывода находятся в нормальной форме. Однако многие формальные системы стремятся продемонстрировать что-то вроде теоремы о нормализации в том смысле, что когда вызывается любое неминимальное использование наших логических правил, мы можем без потери общности переписать аргумент, чтобы исключить его. Одним из главных сторонников такого рода работ был Даг Правиц, чей тезис о теоретико-доказательном анализе естественной дедукции помог во многих философских работах о доказательствах, выводах и вычислениях, которые последовали за этим.

Ценная концепция, которую Правиц вводит в свою работу, - это понятие «каркаса аргументов». (см. его «Об идее общей теории доказательств» для более доступного обзора). Это обобщение древовидных структур, используемых в аргументах или доказательствах формальной естественной дедукции, поскольку мы допускаем не только то, что мы работаем от логических аксиом как предпосылок к выводам (что мы называем закрытым аргументом), но также и то, что мы можем допустить недоказанные доказательства. антецеденты, которые ведут к следствиям посредством тех же логических правил вывода — эти структуры «открытого аргумента» также являются скелетами аргументов.

(Естественная дедукция часто пытается вообще обойтись без аксиом в своих структурах, скорее откладывая все «чисто логическое» до применения правил структурного вывода.)

Так что, возможно, некоторые полезные обороты речи могут быть следующими: ваши «более слабые» формальные аргументы — это открытые аргументы, а их «доказательства» — это каркасы аргументов, поскольку они намекают на структуру доказательства, которая потенциально может быть усовершенствована. Ваши «более сильные» аргументы — это закрытые аргументы, в том смысле, что их скелеты не оставляют болтающихся экстра-логических предположений, и наиболее синтаксически минимальная версия такого аргумента (идеально подходящая для машинной обработки) будет его нормальной формой.

Существуют альтернативные интерпретации такого рода работы в других формах теории доказательств. В то время как Правиц использует скелеты аргументов для поддержки своей системы естественной дедукции, более распространенная технология последовательного исчисления , разработанная на основе системы Гильберта Герхардом Генценом, позволяет нам фиксировать правила преобразования для выводов, стирая различие между открытыми и закрытыми аргументами. Однако понимание этого различия может помочь понять, что исчисление секвенций делает по-другому, и как мы можем использовать принципы непротиворечивости и преобразования аргументов, сохраняющие правильность, для механического манипулирования строками доказательства.

Некоторые части этого превосходны и очень актуальны, например, ссылка на скелеты аргументов Правица; но я думаю, что предложение «нормальной формы» в качестве ответа на вопрос ОП действительно ошибочно. Нахождение в нормальной форме является гораздо более сильным свойством, чем то, что оно дается в качестве полностью формального аргумента, как описывает OP - доказательства, написанные для систем компьютерной проверки, таких как Mizar и Coq, почти никогда не находятся в нормальной форме (даже после того, как они полностью разработаны средством проверки типов), и было бы невозможно требовать, чтобы они были такими, поскольку нормализация обычно приводит к значительному увеличению размера.
Спасибо за ваш комментарий, Питер - это очень сильная степень формализации, и я полагаю, что мне интересно, есть ли больше смысла в том, что задающий вопрос подразумевает под «максимально строгим», если будет достаточно чего-то менее развернутого, чем нормальная форма чтобы удовлетворить их потребности. Возможно, сохранение этой терминологии для нормальной формы может помочь объяснить, что «что-то чуть менее максимально строгое» - это то, к чему стремится ОП?

См. этот пост о спектре формальности математического аргумента . То, что вы описали как «каждый шаг и предпосылки явно указаны», будет классифицировано как «абсолютно формальное» (и «формальное доказательство» без каких-либо оговорок часто означает это). Большинство математических аргументов не выражаются как абсолютно формальные доказательства, а скорее подпадают под категорию «достаточно формальных». Вы просили ввести термин для доказательств в дедуктивной системе, которые явно не устанавливают используемые правила, но такого термина нет, потому что формальные системы обычно устроены так, чтобы можно было механически проверить, соблюдаются ли правила или нет, и, следовательно, Нет необходимости указывать, какое правило используется на каждом шаге, кроме как для повышения эффективности процесса проверки.

Однако у вас, похоже, неправильное представление о природе доказательства пропозициональной тавтологии с помощью таблиц истинности. Хотя разумно считать его неформальным в том смысле, что вы рисуете таблицу и говорите: «посмотрите, это все случаи, и утверждение верно в каждом случае», на самом деле его можно выразить не менее формально, чем в стиле Гильберта или Фитча . -стиль или секвент-стильдоказательство. Все, что вам нужно сделать, это выписать таблицу по одной строке за раз в систематическом порядке (например, в лексикографическом порядке; для 3 переменных A, B, C у вас будут строки 000,001,010,011,100,101,110,111, обозначающие значения истинности A, B, C). ) и истинностное значение утверждения для каждой строки (которое можно вычислить механически). Это иногда называют семантическим доказательством, потому что оно осуществляется путем проверки истинностного значения утверждения (в соответствии с семантикой пропозициональной логики) в каждой ситуации (истинностное присвоение переменных). Напротив, доказательство в некоторой дедуктивной системе является синтаксическим доказательством, потому что это «просто» вопрос толкования символов без учета «значения». Тем не менее, семантические доказательства могут быть столь же формальными, как и синтаксические доказательства, поскольку вам по-прежнему нужен какой-то механический процесс проверки синтаксического доказательства.

Но, как всегда, стоит подчеркнуть, что, хотя мы можем иметь семантические доказательства для логики высказываний, невозможно иметь семантические доказательства для полной логики первого порядка (поскольку теоремы о неполноте, примененные к PA-, показывают, что не может быть программы, которая может решить за конечное число шагов, является ли входное предложение формы «X ⇒ Y» на языке PA тавтологией или нет, где «X» — это конъюнкция аксиом PA−). Таким образом, синтаксические доказательства остаются единственным полностью адекватным методом доказательства для логики первого порядка.

Дедуктивный аргумент, в котором четко указаны каждый шаг и посылка?
СпросиСетьПолитика конфиденциальности1y, 0v