Completeness, soundness и consistency.

[agonization]

Есть достаточно хороший способ проверить эти вещи для произвольной теории? Естественно, полнота понимается как полнота по Гёделю.

Есть вариант посмотреть доказательства и просто рассуждения в теореме Гёделя о полноте (1929), а также в теоремах Гёделя о неполноте (1930), но будут ли подходы, использованные там, адекватными для произвольной теории? Как минимум даже в мат.логике исчисления существуют далеко не только гильбертовского типа. Я не уверен в том, что это подходит для более широкого класса исчислений, чем для того, над которым работал сам Гёдель; т.е. это может быть таковым, но для меня пока что это не очевидно. Тем не менее понятие полноты (по Гёделю) и его значимость для проверки теорий никуда не исчезают. Точнее, полноты синтаксической и семантической.

Что же о soundness - я в принципе не знаю, в каких теоремах это разбиралось, но понятие существует и, по-моему, должно быть столь же важным.

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

Нет чего-либо проще и более строгого для нахождения того, что произвольная теория непротиворечива?

Более того, не существует ли ещё средств автоматической проверки хотя бы простейших синтаксических противоречий, нужно лишь задать для программы правила вывода, правила преобразования и набор исходных высказываний теории?

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

[agonization]

Естественно, речь про паттерны пошла по той причине, что в случае, когда теория неполна, есть большие проблемы с установлением её непротиворечивости. И тогда можно попытаться найти в ней конкретные противоречия, найденные по конкретным паттернам. Есть ли какой сравнительно простой и при этом достаточно точный, системный способ нахождения противоречий? Да и случай с полнотой теории не выглядит тривиальным.

[mihaild]

Если теория неполна, то она заведомо непротиворечива - в противоречивых теориях выводится всё.

Простого универсального способа нахождения противоречий не существует, иначе не существовало бы открытых проблем.

agonization в сообщении #1349989 писал(а):

Что же о soundness - я в принципе не знаю, в каких теоремах это разбиралось, но понятие существует и, по-моему, должно быть столь же важным.

Теоремы о корректности.

agonization в сообщении #1349989 писал(а):

Тем не менее понятие полноты (по Гёделю) и его значимость для проверки теорий никуда не исчезают

Уточните, что вы тут понимаете под полнотой. Потому что теорема Гёделя о полноте - про исчисление, а не про какую-то теорию

[agonization]

mihaild в сообщении #1350048 писал(а):

Если теория неполна, то она заведомо непротиворечива

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

mihaild в сообщении #1350048 писал(а):

Простого универсального

Естественно. Но способа проще, чем способа изучать то, как находились уже найденные противоречия, нет?

mihaild в сообщении #1350048 писал(а):

Уточните, что вы тут понимаете

Если я не ошибаюсь, формальная теория, если изъясняться через ТМ, может быть описана так: это множество высказываний (формул), замкнутое на коллекции операций, а именно принятых правил вывода (например, modus ponens) и преобразования (например, правило подстановки). В этом множестве можно выделить подмножество аксиом. Например, это будут те тавтологии (высказывания, истинные во всех формальных интерпретациях), которые будут выбраны для дальнейшего вывода теорем, и те постулаты, которые характеризуют остальное содержание теории, т.е. в конечном счёте формул, выражающихся при помощи тех или иных дескриптивных знаков модели. Таким образом строится система аксиом данной теории (может быть построена другая). Также можно в альтернативе построить систему схем аксиом, как это сделано в модальной логике - т.е. это будет система формул метаязыка теории. Но это в гильбертовских исчислениях, альтернативно можно использовать вместо обычных и привычных тавтологий, как пример, секвенции. Многие мат.теории, далёкие от мат.логики, вовсе не имеют чего-либо достаточно похожего на тавтологии (например, в геометрии); тем не менее вывод в них производится согласно некоторому исчислению. Исчисление же как таковое подразумевает, кроме системы аксиом (или схем их получения), правил вывода и правил преобразования - также алфавит (счётное множество знаков, и из него можно составить множество слов подразумеваемого языка) и формальную порождающую грамматику (правила построения допустимых формул из знаков алфавита - множество таких формул будет подмножеством слов языка). Полнота (по Гёделю) характеризует свойство некоторой системы аксиом. Естественно, я подразумевал под полнотой или неполнотой теории то её свойство, которое характеризует выделенную в ней систему аксиом. В принципе понятие полноты может говорить также о том, что любая система аксиом данной теории будет, как минимум предположительно, неполной.

-- 29.10.2018, 20:27 --

mihaild в сообщении #1350048 писал(а):

Теоремы о корректности.

Можете привести устоявшийся пример?

[mihaild]

agonization в сообщении #1350084 писал(а):

Но способа проще, чем способа изучать то, как находились уже найденные противоречия, нет?

Можно доказывать, что если какая-то теория непротиворечива, то наша тоже непротиворечива. Например, доказано, что если ZF непротиворечива, то ZFC и PA тоже непротиворечивы.

agonization в сообщении #1350084 писал(а):

Полнота (по Гёделю) характеризует свойство некоторой системы аксиом.

Определение "полноты по Гёделю" можете написать?

agonization в сообщении #1350084 писал(а):

Исчисление же как таковое подразумевает, кроме системы аксиом (или схем их получения), правил вывода и правил преобразования - также алфавит (счётное множество знаков, и из него можно составить множество слов подразумеваемого языка) и формальную порождающую грамматику (правила построения допустимых формул из знаков алфавита - множество таких формул будет подмножеством слов языка)

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

[agonization]

mihaild в сообщении #1350089 писал(а):

Определение "полноты по Гёделю" можете написать?

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

[mihaild]

agonization в сообщении #1350101 писал(а):

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

В смысле формула, истинная в каждой интерпретации, доказуема? Я не уверен, что понимаю, как стоят кванторы.

agonization в сообщении #1350101 писал(а):

вывод должен быть истинным во всех формальных интерпретациях

Что такое "истинность вывода"?

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

[agonization]

mihaild в сообщении #1350103 писал(а):

Что такое "истинность вывода"?

Выведенная формула принимает значение истины. По каким принципам она принимает именно это значение, зависит от рассматриваемой интерпретации (если это не тавтология) и от принятой T-теории в формальной семантике рассматриваемой предметной теории; это задаётся в метаязыке, чаще всего через реализации T-схем.

mihaild в сообщении #1350103 писал(а):

теория полна, если в ней для каждого утверждения выводимо либо оно, либо его отрицание

Это синтаксическая полнота (без учёта некоторых случаев).

mihaild в сообщении #1350103 писал(а):

В смысле формула, истинная в каждой интерпретации, доказуема?

Все тавтологии должны быть либо аксиомами, либо доказуемыми. То есть, это:

mihaild в сообщении #1350103 писал(а):

из общезначимости утверждения в этом классе моделей следует его выводимость

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

UPD: правда, если быть точнее, то терм (не понятие, используемое тут) "значимость", именно такой, должен переводиться как "definability", скорее всего.

[mihaild]

agonization в сообщении #1350084 писал(а):

Можете привести устоявшийся пример?

Ну собственно теорема о корректности исчисления предикатов, например: для любой теории все ее теоремы истинны в любой модели.

[agonization]

Так что насчёт программ, которые могли бы проверять хотя бы самые простые противоречия на их наличие в указанной теории под указанное исчисление? Такое существует? В тематике автопруверов я не образован.

И неужели нет каких-то иных подходов, кроме как апелляций к другим теориям (что выглядит, по-моему, не очень корректно)?

Да и все остальные вопросы, указанные в первом сообщении.

[mihaild]

Если бы вы задавали вопросы по одному, их обсуждать было бы сильно легче

Прувер теоретически можно попросить вывести отрицание аксиомы из остальных. Не знаю, насколько успешно.

Непротиворечивость теории мы в любом случае будем доказывать средствами какой-то еще теории. И если теория, средствами которой мы доказываем непротиворечивость, сама по себе противоречива, то смысла в нашем доказательстве нет.

[agonization]

agonization в сообщении #1350101 писал(а):

каждое доказательство должно быть произведено за конечное число шагов и при помощи конечного числа аксиом.

И каждая формула должна принимать на вход конечное число переменных.

[agonization]

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

Это я к тому, что в английской литературе терм "значимость" понимается явно иначе. Хотя и "soundness" тут перевели как "корректность", хотя есть ещё и "correctness", что тоже вполне может встречаться в матлогике (как минимум в смежных областях встречается).

Плюс я сам себя поправил.