Классические аксиомы подразумевают, что каждое предложение разрешимо? - PullRequest
Новая
       14

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

3 голосов
/ 20 апреля 2020

В руководстве по Lean «Теорема, доказывающая по Lean» я читал: «С помощью классических аксиом мы можем доказать, что каждое предложение разрешимо».

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

Читая «С классическими аксиомами», я понимаю, что у нас есть что-то эквивалентное закону исключенного среднего: 

Axiom LEM : forall (p:Prop), p \/ ~p.

Читая «каждое предложение разрешимо», я понимаю, что мы можем определить функцию (или, по крайней мере, мы можем доказать существование такой функции ): 

Definition decide (p:Prop) : Dec p.

, где Dec - это семейство индуктивных типов: 

Inductive Dec (p:Prop) : Type :=
| isFalse : ~p -> Dec p
| isTrue  :  p -> Dec p
.

Тем не менее, с помощью того, что я знаю о Coq, я не могу реализовать decide, поскольку не могу уничтожить (LEM p) (вроде Prop), чтобы вернуть что-то отличное от Prop.

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

1 Ответ

2 голосов
/ 21 апреля 2020

В исчислении конструкций без каких-либо аксиом есть мета-теоретическое свойство, заключающееся в том, что каждое доказательство A \/ B обязательно является доказательством того, что A выполнено (упаковано с использованием конструктора or_introl) или доказательство того, что B выполнено (используя другой конструктор). Таким образом, доказательство A \/ ~ A является либо доказательством того, что A выполнено, либо доказательством того, что ~ A выполнено.

Следуя этому мета-теоретическому свойству, в Coq без аксиом , все доказательства предложений вида forall x, P x \/ ~P x фактически являются доказательствами, что P разрешима. В этом параграфе значение decidable является общепринятым значением, используемым книгами по вычислимости.

Некоторые пользователи начали использовать слово decidable для любого предиката P так что существует доказательство forall x, P x \/ ~ P x. Но они на самом деле говорят о другом. Чтобы было понятнее, я назову это понятие злоупотребление терминологией-разрешимым .

Теперь, если вы добавите аксиому типа LEM в Coq, вы в основном заявите, что каждый предикат P становится допускающим злоупотребление терминологией . Конечно, вы не можете изменить значение условно-разрешимого , просто добавив аксиому в вашу разработку Coq, так что больше нет включения.

Я боролся с этим злоупотреблением терминологией в течение многих лет, но безуспешно.

Чтобы быть более точным, в терминологии Coq термин decidable используется не для предложений или предикатов, которые пользуются LEM, но для предложений или предикатов, которые пользуются более сильным следующим утверждением: 

forall x, {P x}+{~P x}

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

...