При каких условиях аксиоматическая система доказательства имеет эквивалент естественного вывода?

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

Под «системой естественной дедукции» я подразумеваю систему доказательств, основанную на правилах введения и исключения, обеспечивающую относительно большой набор выводов. Например, исчисление секвенций в стиле Генцена с некоторыми доказательствами, обязательно содержащими строки с непустым набором посылок слева от турникета.

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

  1. (Классическая) логика высказываний: чтобы обеспечить эквивалентность естественной системе вывода с → -вводное правило, теорема дедукции должна выполняться в аксиоматической системе.
  2. (Классическая) логика первого порядка: чтобы обеспечить эквивалентность естественной системе вывода с ∀ -вводное правило, универсальное обобщение должно иметь место в аксиоматической системе.

Но можно ли сказать что-нибудь интересное и более общее об условиях эквивалентности, особенно распространяющихся на другие логики (например, модальные логики и логики высших порядков) и аксиоматические теории в математике? (Особенно те логики и математические теории, которые являются неполными?) Какие условия необходимы для обеспечения естественного дедуктивного эквивалента аксиоматической системы доказательства (и наоборот )? Существуют ли свойства аксиоматической или естественной системы вывода, которые окончательно блокируют эквивалентность?

Ответы (1)

Под «системой естественной дедукции» я подразумеваю систему доказательств, основанную на правилах введения и исключения, обеспечивающую относительно большой набор выводов. Например, исчисление секвенций в стиле Генцена с некоторыми доказательствами, обязательно содержащими строки с непустым набором посылок слева от турникета.

Во-первых, причина того, что системы естественного вывода имеют больше правил, заключается в том, что они используют больше логических связок ... вы могли бы создать аксиоматическую систему и для большего количества связок, и она также будет иметь больше аксиом. На самом деле, самый естественный способ создать аксиоматическую систему с правилами для всех обычных связок — это сделать эти правила условностями типичных правил Elim и Intro, например, у вас может быть аксиома ( п → Вопрос ) → ( ( Вопрос → п ) → ( п ↔ Вопрос ) ) как аксиоматическая обусловленность типичного ↔ Вступительное правило, в то время как что-то вроде ( п ↔ Вопрос ) → ( п → Вопрос ) был бы хорошим кандидатом для аксиоматизации ↔ Правило вывода Элима.

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

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

Конечно, если нет такой систематической связи между аксиомами и правилами вывода, то все ставки сняты, и вам придется доказывать эквивалентность между различными системами на более ad hoc основе,... другими словами, я не могу сказать вам какие-либо «общие требования к эквивалентности» ... кроме возможности доказать, что обе системы, конечно, завершены сами по себе.

Извините, я не хотел сказать, что «больше правил» было определяющей характеристикой систем ND — просто типичная особенность. Я предполагаю, что «более общие требования», которые я имел в виду, были чем-то вроде того, что вы получаете из соответствия Карри-Ховарда (-Ламбека), где теорема дедукции соответствует устранению абстракции в типизированной комбинаторной логике и → -intro соответствует абстракции функции в лямбда-исчислении....
... Таким образом, кажется, что одно требование для эквивалентности Гильберта <-> ND <-> Sequent состоит в том, что теорема дедукции верна для системы Гильберта, каждый вывод ND должен быть приведен к нормальной форме, а исчисление секвенций должно допускать устранение разрезов. Это кажется правильным? Если это правильно, то является ли «общее требование» (по крайней мере, необходимым условием), которое я преследую (хотя, по общему признанию, только в лучшем случае неуклюже), соответствует ли такое структурное правило/свойства нормализации?
@ Деннис Хм, многое из того, что вы здесь говорите, на самом деле выше моего понимания, извините! Надеюсь, вам помогут более опытные логики...
хорошо спасибо! Я должен добавить этот материал в вопрос. Только пытаясь прояснить, что я имел в виду для вас, я подумал спросить об этих связях. Так что ваш ответ очень помог!
@ Деннис О, хорошо! Думаю, иногда вам просто нужна дека. Рад быть полезным, ха-ха! :) Но да, отредактируйте свой пост, и, надеюсь, вы заставите других людей ответить!
При каких условиях аксиоматическая система доказательства имеет эквивалент естественного вывода?
СпросиСетьПолитика конфиденциальности1y, 0v