Есть ли большая разница в наличии недостаточного количества аксиом и правил вывода/процедуры доказательства для создания полной теории?
Кажется, что во многих случаях добавление нового правила вывода или новой аксиомы дает тот же эффект. Например, рассмотрим язык с двуместными связками. . В языке также есть правило вывода .
Теперь мы можем добавить новые схемы аксиом: и для любой формулы . Альтернативой является добавление новых правил вывода: и . В этом случае я утверждаю, что теории эквивалентны независимо от аксиоматизации.
В частности, я думаю, что в логике второго порядка что-то мешает нам заменить правила вывода аксиомами, сколько бы правил вывода ни было определено, поскольку утверждается, что исчисление доказательств второго порядка всегда недостаточно (для некоторых теорий). В противном случае мы всегда могли бы использовать одно и то же исчисление доказательств и просто добавлять аксиомы, и, таким образом, иметь универсальную процедуру проверки доказательств. Почему добавление аксиом вместо правил вывода терпит неудачу?
Аксиомы, схемы аксиом и правила вывода — это три разные вещи.
Аксиома — это часть данных. Это предложение, которое вводится в логику без доказательства.
Правило вывода (RoI) — это программа. Его можно рассматривать как программу для создания нового предложения из существующих предложений (перечисление); его можно рассматривать как процедуру принятия решения, чтобы проверить, следует ли новое предложение из существующих предложений (проверка).
Схема аксиом — это область интереса, которая вводит исчисляемое бесконечное число утверждений. Таким образом, описание схемы аксиом как представляет , и т.д., все в теорию.
Некоторые логики явно имеют RoI с именем «Пропозициональная замена». Это правило состоит в том, что если у вас есть доказанное пропозициональное выражение, любая пропозициональная переменная может быть полностью заменена произвольным пропозициональным выражением. Так, например, если вы доказали , то можно сделать вывод . Яськовский сделал это правило явным в своей логике.
В логике с пропозициональной подстановкой аксиомы и схема аксиом одного и того же описания порождают одну и ту же теорию. На самом деле, такая логика, как правило, даже не беспокоится о схеме аксиом. В логике без пропозициональной подстановки аксиомы и схема аксиом одного и того же описания могут порождать разные теории. Например, из аксиомы ты не мог сделать вывод без пропозициональной замены.
Исключение всех RoI (даже тех, которые не являются схемой аксиом) сделало бы невозможным введение в теорию новых теорем, поэтому вы никогда не сможете доказать ничего, кроме того, что явно предполагается.
В современной логике насущный вопрос, как правило, прямо противоположный: как сделать так, чтобы пользователь логики мог вводить новые действительные области интереса? Существует множество процедур принятия решений, которые могут оценивать предложения и определять их правильность гораздо быстрее, чем если бы они были ограничены композициями из нескольких жестко запрограммированных RoI, и по мере увеличения формальных библиотек это становится основным узким местом.
Дуг Спунвуд
Эрик Вофси
хмахольм ушел за Монику