Я хочу знать, может ли быть доказана разрешимость равенства двух разрешимых доказательств одного и того же предложения без каких-либо дополнительных аксиом в исчислении индуктивных построений.
В частности, я хочу знать, правда ли это, без каких-либо дополнительных аксиом в Coq.
Спасибо!
Отредактировано, чтобы исправить ошибку: Изменить 2, чтобы сделать Prop
более явным
Ответы:
Как указывает Нил, если вы работаете в «предложениях - это типы», вы можете легко придумать тип, равенство которого не может быть показано разрешимым (но, конечно, непротиворечиво полагать, что все типы имеют разрешимое равенство), напримерN → N ,
Если мы понимаем «предложение» как более ограниченный тип, то ответ зависит от того, что именно мы имеем в виду. Если вы работаете в исчислении конструкций сN → N , Это также означает, что вы не можете доказать свою теорему для понятия Кока о
Prop
видом, вы все равно не сможете показать, что разрешимые предложения имеют разрешимое равенство. Это так, потому что в исчислении конструкций непротиворечиво отождествлятьProp
вселенную с релевантным для доказательства типом, поэтому все, что вы знаете,Prop
может содержать что-то вродеProp
.Но в любом случае лучший ответ приходит из теории гомотопического типа. Там предложение является типомп который удовлетворяет
Мне любопытно узнать, что вы подразумеваете под «предложением».
источник
Prop
? Спасибо!