Методы показа не выводимости в логиках и других системах формального доказательства

В доказательство систем для классической логики , если один хочет , чтобы показать , что определенная формула не выводима один просто показывает , что может быть получена (хотя возможны и другие методы , безусловно , возможны). Не выводимость по существу следует из обоснованности и полноты системы доказательств. $\psi$ $\neg\psi$

К сожалению, для неклассических логик и более экзотических систем доказательства (таких как правила, лежащие в основе операционной семантики) такой прямой техники не существует. Это может быть потому , что не-выводимость не означает , что выводима, как в случае с интуиционистской логикой, или не просто , что ни понятие отрицания существует. $\psi$ $\neg\psi$

На мой вопрос дана система доказательств , где $(\mathcal{L},\vdash)$ , (и, вероятно, его семантика), какие существуют методы, чтобы показать не выводимость? $\vdash\;\subseteq\mathcal{L}^*\times\mathcal{L}$

Интересующие системы доказательств могут включать операционную семантику языков программирования, логику Хоара, системы типов, неклассическую логику или правила вывода для того, что у вас есть.

lo.logic Дэйв Кларк
источник

Дэйв, я думаю , что есть опечатка в вопросе, чтобы показать , что

не выводим мы не показываем , что

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

φ

$\varphi$

\neg φ

$\lnot \varphi$

Каве

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

Дэйв Кларк

Спасибо за разъяснения, мой разум переходит к логике первого порядка по умолчанию, когда я читаю классическую логику. :)

Каве

Ответы:

IME, следующий список проще всего (конечно, он также наименее мощный):

Если ваша система звука, и вы можете доказать , то у вас есть результат nonderivability, конечно. $\lnot \phi$
Если у вас есть теоретико-решеточная семантика для вашей логики, относительно которой все ваши правила доказательства верны, то, если смысл предложения не является верхним элементом решетки, то это не выводимое предложение.
Если вы знаете, что ваша логика полна по отношению к классу моделей, проверьте, есть ли в этом классе конкретная модель, которая делает недействительным . $\phi$
Иногда вы можете сойти с перевода в другую логику и показать, что выводимость здесь подразумевает известный результат недопустимости.
Если у вас есть естественное вычитание или последовательное исчисление, проверьте, известен ли результат исключения среза или вы можете доказать его. Если да, то вы часто можете использовать свойство subformula, чтобы дать простые индуктивные аргументы о недопустимости. (Например, непротиворечивость посредством исключения-вырезки - это просто утверждение о том, что не существует доказательств ложного вырезания без вырезов, и поэтому, если все сокращения могут быть устранены, несоответствий не будет.)
Если больше ничего не работает, то вы часто можете показать результаты согласованности / недостижимости через аргумент логических отношений. Это большая пушка, которая работает тогда, когда больше ничего не происходит - в терминах теории множеств она сводится к использованию аксиомы замены, которая позволяет показать, что огромные множества хорошо упорядочены. (Вот почему вы можете использовать его для доказательства таких вещей, как нормализация системы F.)

Нил Кришнасвами
источник

F

$F$

P A^{2}

$PA^2$

F^{2}

$F^2$

Спасибо, теперь я понимаю, что вы имели в виду под «такими вещами, как нормализация системы F». :)

Каве

@Kaveh, @Neel: Сильная нормализация системы F не является теоремой PA2, а эквивалентна по PA согласованности PA2. Скорее, строгая нормализация для всех членов ранга n (ранг является мерой максимальной глубины квантификаторов типа nsted) может быть доказана с использованием ACA- n . Мне нравится говорить о тайном создании моделей снопов

Чарльз Стюарт,

@Charles: я узнал об этой идее из некоторых работ Жана Галье, которые на удивление недо цитируются. Несколько странно, что эта причудливая точка зрения помогла мне понять более простую историю Митчелла и Щедрова.

Нил Кришнасвами,