Równość rozstrzygalnych dowodów?

Chcę wiedzieć, czy rozstrzygalność o równości dwóch rozstrzygalnych dowodów tej samej twierdzenia można udowodnić bez żadnych dodatkowych aksjomatów w rachunku konstrukcji indukcyjnych.

W szczególności chcę wiedzieć, czy to prawda bez żadnych dodatkowych aksjomatów w Coq.

\forall P : Prop, P \lor \neg P \Rightarrow (\forall p_{1} : P, \forall p_{2} : P, {p_{1} = p_{2}} \lor {p_{1} \neq p_{2}})

$\forall P: \texttt{Prop}, P \vee \neg P \Rightarrow (\forall p_1 : P, \forall p_2: P, \{p_1 = p_2\} \vee \{p_1 \neq p_2\})$

Dzięki!

Edytowane w celu skorygowania błędu: Edytuj 2, aby Propbardziej precyzyjnie

coq constructive-mathematics calculus-of-constructions

— Adam Barak
źródło

To, co napisałeś, nie ma sensu. Jeśli jest twierdzeniem, to jest dowodem i nie można utworzyć . Czy miałeś na myśli, że twoja hipoteza to zamiast , tj. „ jest rozstrzygalne”?

P

$P$

p : P

$p : P$

p \lor \neg p

$p \lor \lnot p$

P \lor \neg P

$P \lor \lnot P$

p \lor \neg p

$p \lor \lnot p$

P

$P$

— Andrej Bauer,

Przepraszam, miałem na myśli hipotezę „ jest rozstrzygalne”, tj.

P

$P$

P \lor \neg P

$P \vee \neg P$

— Adam Barak

Weź aby być , a instrukcja jest fałszywa, ponieważ możesz łatwo zamieszkać z , a równoważność funkcji jest oczywiście nierozstrzygalna. Czy masz na myśli jakieś inne warunki dotyczące ?

P

$P$

N \to N

$\mathbb{N} \to \mathbb{N}$

(N \to N) \lor \neg (N \to N)

$(\mathbb{N} \to \mathbb{N}) \vee \lnot(\mathbb{N} \to \mathbb{N})$

i n l (λ x . x)

$\mathsf{inl}(\lambda x.\;x)$

P

$P$

— Neel Krishnaswami,

P powinno być propozycją. (Właściwie, w moim rozwoju używam już ekstensywności funkcjonalnej, więc stwierdzenie to nadal może być dla mnie ważne, ale na razie zignorujmy funkcjonalną / propozycyjną ekstensywność).

— Adam Barak,

Rozległość funkcji nie oznacza, że równoważność funkcji jest rozstrzygalna ... A odpowiedź Neela rozwiązuje ogólny przypadek: jeśli P jest (zamieszkałym) nieskończonym typem (który obejmuje niektóre typy Zdań, jeśli nie są uwzględnione żadne dodatkowe aksjomaty), to implikacja się nie udaje utrzymywać przez .

P \to P

$P\rightarrow P$

— cody

Jak wskazuje Neel, jeśli pracujesz pod „propozycjami są typy”, możesz łatwo wymyślić typ, którego równości nie da się rozstrzygać (ale oczywiście jest spójne założenie, że wszystkie typy mają równość rozstrzygalną), taki jak . $\mathbb{N} \to \mathbb{N}$

Jeśli rozumiemy „propozycję” jako bardziej ograniczony rodzaj, odpowiedź zależy od tego, co dokładnie mamy na myśli. Jeśli pracujesz nad rachunkiem konstrukcji z Proprodzajem, nadal nie możesz pokazać, że zdania rozstrzygalne mają rozstrzygającą równość. Dzieje się tak, ponieważ w rachunku konstrukcji jest spójne z Propwszechświatem typu dowodu, więc wiadomo, że Propmoże zawierać coś takiego jak . Oznacza to również, że nie możesz udowodnić swojego twierdzenia na temat pojęcia Coq . $\mathbb{N} \to \mathbb{N}$ Prop

Ale w każdym razie najlepsza odpowiedź pochodzi z teorii typów homotopii. Istnieje propozycja typu która spełnia Oznacza to, że zdanie ma co najwyżej jeden element (tak jak powinien, jeśli ma być rozumiany jako wartość prawdy nieistotna dla dowodu). W tym przypadku odpowiedź jest oczywiście pozytywna, ponieważ definicja zdania natychmiast sugeruje, że jego równość jest rozstrzygalna. $P$

\forall x, y : P . x = y .

$\forall x, y : P \,.\, x = y.$

Jestem ciekawy, co rozumiesz przez „propozycję”.

— Andrej Bauer
źródło

Jak miałbyś w środku ? Dzięki!

N \to N

$\mathbb{N} \rightarrow \mathbb{N}$ Prop

— Adam Barak,

W rachunku konstrukcji nic nie stoi na przeszkodzie, aby , prawda?

P r o p = T y p e

$\mathtt{Prop} = \mathtt{Type}$

— Andrej Bauer,

Zamieszanie dotyczy tego, co należy rozumieć przez „system coq”. Jeśli jest to „rachunek konstrukcji”, to . Jeśli dokładniejszy „Rachunek konstrukcji indukcyjnych z 1 wszechświatem impredykatywnym”, to nie ma znaczenia bez adnotacji na poziomie wszechświata. O ile mi wiadomo, jest spójnym aksjomatem (choć niespójnym z EM z subtelnych powodów).

P r o p = S e t = T y p e

$\mathtt{Prop=Set=Type}$

T y p e

$\mathtt{Type}$

T y p e_{1} = P r o p

$\mathtt{Type_1=Prop}$

— cody

Jasne, musimy przyczepić indeks do . Punkt, który @AdamBarak powinien zrozumieć, jest następujący: ponieważ nie prowadzi do żadnej sprzeczności w Coq, możemy pokazać, że czegoś nie można zrobić w Coq, pokazując, że doprowadziłoby to do sprzeczność, gdybyśmy mieli także .

T y p e

$\mathtt{Type}$

P r o p = {T y p e}_{1}

$\mathtt{Prop} = \mathtt{Type}_1$

P r o p = {T y p e}_{1}

$\mathtt{Prop} = \mathtt{Type}_1$

— Andrej Bauer,

Nadal nie do końca dobrze, ponieważ w Coq nie możemy pokazać, że równoważność funkcjonalna jest nierozstrzygalna. Orzeczenie „równość na jest rozstrzygalne” jest tym, co Martin Escardo nazywa konstruktywnym tabu: nie można tego ani udowodnić, ani obalić w Coq. Zatem poprawny argument to: jeśli to jest propozycją, a wyrażenie „równość w jest rozstrzygalny ”nie można udowodnić. (Podczas gdy powiedziałeś: a wyrażenie „równość na jest rozstrzygalne” jest fałszywe).

N \to N

$\mathbb{N} \to \mathbb{N}$

P r o p = {T y p e}_{1}

$\mathtt{Prop} = \mathtt{Type}_1$

N \to N

$\mathbb{N} \to \mathbb{N}$

N \to N

$\mathbb{N} \to \mathbb{N}$

N \to N

$\mathbb{N} \to \mathbb{N}$

— Andrej Bauer,