私はCOQで証明外れを考えています。 一つの証明可能な文は言う：証明書とは無関係です。
タイプの平等が決定可能であるならば、平等文の唯一の証拠、すなわち、再帰性があることができます。
COQで複数の等価証明を持つ型を構築できるかどうかは疑問です。したがって、私は次の構成が一貫しているかどうか尋ねます。私はここにパズル何
(*it is known that f=g is undecidable in COQ *)
Definition f(n:nat) := n.
Definition g(n:nat) := n+0.
Axiom p1: f=g.
Axiom p2: f=g.
Axiom nonirrelevance:p1<>p2.
は、P1導入することによって、私は=グラム決定可能F平等に作られたので、それが唯一の証拠を持っているべきであるという事実です！私の推論における誤りは何ですか？
これはすべて純粋なCOQ動作か、それともHOTTと似ていますか？
私はいくつか混乱していると思います。
あなたが話している証明可能な文はhttps://coq.inria.fr/library/Coq.Logic.Eqdep_dec.htmlで見つけることができると
Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) :
forall (y:A) (p1 p2:x = y), p1 = p2.
は今非常に興味深いものが何であるかをeq_decのタイプです。まず第一に、平等が決定可能であることを本当に要求することさえありません。ただ真実であるか偽であるかを求めるだけです。 xとyは等価性を証明するために、すべての関数に対してこのプロパティを求めます。
あなたは矛盾を証明する必要がありますのでforall (f g : nat -> nat), f = g \/ f <> gできません。 p1はあなたの特定のfとgについてf = g \/ f <> gという証明です。 可能であれば、機能を比較することができますが、確かに異なっている複数の方法があるシステムを構築する方法がないことを意味します。
最後に、Pが確定不能であるということは、まだ{P} + {~P}以上の構成可能な機能がないということだけを意味しますが、それを公理として追加することは矛盾につながるわけではありません。それを追加するだけで、それは明らかではありませんでした。
「まず第一に...」から始まる2番目の文を理解できません。各x、yについてx = y \/x <> yという項を持つことは、決定性とはどういう意味ですか？ – Cryptostasis
決定可能性は '{x = y} + {x <> y}'です。これは、これらの項が等しいかどうかを判断できるアルゴリズムがあることを意味します。 'x = y \/x <> y'は、「どちらかが等しいか、どちらかではないが、どちらかを伝えているならば、どちらかといえば」を意味する。 'x = y \/x <> y'を持つときに、条件が等しいかどうかを知ることはできません。つまり、それは*建設的なものではありません。反対に '{x = y} + {x <> y}'があります。 –
あなたは今私を混乱させています：Coq.Logic.Decidableは*定義可能です（P：Prop）：= P \ /〜P *。 – Cryptostasis
関連すると思います：https://cstheory.stackexchange.com/questions/5158/prove-proof-irrelevance-in-coq – augurar
推論の誤りは、「p1」がタイプに対して同等ではないことです'nat - > nat'と判定できるので、無関係の証明は暗示されません。 – augurar