Равенство разрешимых доказательств?

9

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

В частности, я хочу знать, правда ли это, без каких-либо дополнительных аксиом в Coq.

P:Prop,P¬P(p1:P,p2:P,{p1=p2}{p1p2})

Спасибо!

Отредактировано, чтобы исправить ошибку: Изменить 2, чтобы сделать Propболее явным

Адам Барак
источник
1
То, что вы написали, не имеет смысла. ЕслиP это предложение тогда p:P является доказательством, и вы не можете сформировать p¬p, Вы имели в виду свою гипотезуP¬P вместо p¬pто естьPрешаемо "?
Андрей Бауэр
Извините, я имел в виду гипотезуP разрешима ", то есть P¬P
Адам Барак
2
принимать P быть NNи утверждение ложно, так как вы можете легко обитать (NN)¬(NN) с inl(λx.x)и эквивалентность функций, очевидно, неразрешима. Есть ли другие условия наPты имеешь в виду?
Нил Кришнасвами
P должен быть предложением. (На самом деле, в своей разработке я уже использовал функциональную экстенсиональность, поэтому утверждение все еще может быть для меня верным, но давайте пока проигнорируем функциональную / пропозициональную экстенсиональность).
Адам Барак
Расширение функций не подразумевает, что эквивалентность функций разрешима ... И ответ Нила решает общий случай: если P - (обитаемый) бесконечный тип (который включает в себя некоторые типы предложений, если не включены дополнительные аксиомы), то импликация не выполняется держать для PP,
Коди

Ответы:

5

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

Если мы понимаем «предложение» как более ограниченный тип, то ответ зависит от того, что именно мы имеем в виду. Если вы работаете в исчислении конструкций с Propвидом, вы все равно не сможете показать, что разрешимые предложения имеют разрешимое равенство. Это так, потому что в исчислении конструкций непротиворечиво отождествлять Propвселенную с релевантным для доказательства типом, поэтому все, что вы знаете, Propможет содержать что-то вродеNN, Это также означает, что вы не можете доказать свою теорему для понятия Кока о Prop.

Но в любом случае лучший ответ приходит из теории гомотопического типа. Там предложение является типомP который удовлетворяет

x,y:P.x=y.
То есть предложение имеет не более одного элемента (как и должно быть, если его следует понимать как значение истины, не относящееся к доказательству). В этом случае ответ, конечно, положительный, поскольку определение суждения сразу подразумевает, что его равенство разрешимо.

Мне любопытно узнать, что вы подразумеваете под «предложением».

Андрей Бауэр
источник
Как бы вы NNвнутри Prop? Спасибо!
Адам Барак
В исчислении конструкции нет ничего, что мешало бы Prop=Typе, есть?
Андрей Бауэр
Путаница здесь связана с тем, что подразумевается под «системой coq». Если это «исчисление конструкций», тоProp=Set=Type, Если более точное «Исчисление индуктивных конструкций с 1 импредикативной вселенной», тоTypeбессмысленно без аннотаций уровня вселенной. Насколько я знаю,Type1=Propявляется последовательной аксиомой (хотя несовместимой с EM по тонким причинам).
Коди
Конечно, мы должны прикрепить индекс на Type, Смысл для @AdamBarak понять это: потому чтоProp=Type1 не приводит к противоречию в Coq, мы можем показать, что что-то не может быть сделано в Coq, показав, что это приведет к противоречию, если бы мы также имели Prопзнак равноTYпе1,
Андрей Бауэр
1
Все еще не совсем верно, потому что в Coq мы не можем показать, что функциональная эквивалентность неразрешима. Утверждение "равенство наNN является решаемым ", это то, что Мартин Эскардо называет конструктивным табу: это нельзя ни доказать, ни опровергнуть в Coq. Поэтому правильный аргумент таков: если Prop=Type1 тогда NN это предложение, а утверждение "равенство на NN является разрешимым "не доказуемо. (В то время как вы сказали: и утверждение" равенство на NNявляется разрешимым "является ложным).
Андрей Бауэр