Egalité des preuves décidables?

Je veux savoir si la décidabilité de l'égalité de deux preuves décidables de la même proposition peut être prouvée sans aucun axiome supplémentaire dans le Calcul des constructions inductives.

Plus précisément, je veux savoir si cela est vrai sans aucun axiome supplémentaire dans 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\})$

Merci!

Modifié pour corriger l'erreur: Modifier 2 pour rendre Propplus explicite

coq constructive-mathematics calculus-of-constructions Adam Barak
la source

Ce que vous avez écrit n'a pas de sens. Si

est une proposition, alors

est une preuve et vous ne pouvez pas former

. Vouliez-vous dire que votre hypothèse était

au lieu de

, c'est-à-dire "

est décidable"?

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

Désolé, je voulais dire l'hypothèse "

est décidable", c'est-à-dire

P

$P$

P \lor \neg P

$P \vee \neg P$

Adam Barak

Prenez

pour être

, et l'énoncé est faux, car vous pouvez facilement habiter

avec

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})$

, et l'équivalence de fonction est évidemment indécidable. Y a-t-il d'autres conditions sur

vous avez en tête?

i n l (λ x . x)

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

P

$P$

Neel Krishnaswami

P devrait être une proposition. (En fait, dans mon développement, j'utilise déjà l'extensionnalité fonctionnelle, donc la déclaration peut toujours être valable pour moi, mais ignorons l'extensionnalité fonctionnelle / propositionnelle pour l'instant).

Adam Barak

L'extensionnalité des fonctions n'implique pas que l'équivalence des fonctions est décidable ... Et la réponse de Neel règle le cas général: si P est un type infini (habité) (qui inclut certains types de propositions si aucun axiome supplémentaire n'est inclus), alors l'implication échoue à tenir pour

P \to P

$P\rightarrow P$

cody

Réponses:

Comme le souligne Neel si vous travaillez sous les "propositions sont des types", vous pouvez facilement trouver un type dont l'égalité ne peut pas être montrée décidable (mais il est bien sûr cohérent de supposer que tous les types ont une égalité décidable), comme . $\mathbb{N} \to \mathbb{N}$

Si nous comprenons la «proposition» comme un type de type plus restreint, alors la réponse dépend de ce que nous voulons dire précisément. Si vous travaillez dans le calcul des constructions avec une Propsorte, vous ne pouvez toujours pas montrer que les propositions décidables ont une égalité décidable. Il en est ainsi parce qu'il est cohérent dans le calcul des constructions à assimiler Propavec un univers de type preuve pertinente, donc pour tout ce que vous savez Proppourrait contient quelque chose comme . Cela implique également que vous ne pouvez pas prouver votre théorème pour la notion de Coq de . $\mathbb{N} \to \mathbb{N}$ Prop

Mais dans tous les cas, la meilleure réponse vient de la théorie des types d'homotopie. Là, une proposition est un type qui satisfait $P$ C'est-à-dire qu'une proposition a au plus un élément (comme il se doit si elle doit être comprise comme une valeur de vérité non pertinente pour la preuve). Dans ce cas, la réponse est bien sûr positive car la définition de la proposition implique immédiatement que son égalité est décidable.

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

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

Je suis curieux de savoir ce que vous entendez par "proposition".

Andrej Bauer
la source

Comment auriez-vous

intérieur ? Merci!

N \to N

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

Adam Barak

P r o p = T y p e

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

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}$

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$

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}$