ふぇぇ

Masaki Hara @qnighy

処理系に弱いところがあってcoinductionが矛盾した(本当)

スマートコン @mr_konn

弱くて矛盾するなら、強くしても矛盾するのでは

Masaki Hara @qnighy

@qnighy Coqの話です

スマートコン @mr_konn

Coq って矛盾してたのか……

V-alg-d（ZZ） @alg_d

つまりCoqで任意の命題が証明できるの??

Masaki Hara @qnighy

@alg_d Coqの理論というか論理であるpCICはZFCで裏付けられていることになっているけど実際の処理系はたまにバグが見つかってFalseが証明できる．

Masaki Hara @qnighy

@alg_d ただし僕が今紹介しているのは，任意の命題P,Qに対してPとQが同値ならばP=Qとしてよいという公理 (Coqの推論規則からは出てこない) を仮定したときに矛盾するというもの．

V-alg-d（ZZ） @alg_d

@qnighy ふぇぇ

Masaki Hara @qnighy

@alg_d ふぇぇ

Masaki Hara @qnighy

alg_dさんにふぇぇを返した

V-alg-d（ZZ） @alg_d

@qnighy ナイスふぇぇ !

Masaki Hara @qnighy

@alg_d ナイスナイスふぇぇ！

スマートコン @mr_konn

@qnighy @alg_d ぇぇふ

スマートコン @mr_konn

ふぇぇを無効化した

こばし @n_shin16

alg_dさんのふぇぇを観測した

V-alg-d（ZZ） @alg_d

@n_shin16 ふぇぇ

こばし @n_shin16

@alg_d ふぇぇ

あせろり @Aserorirori

ふぇぇ #とは

V-alg-d（ZZ） @alg_d

何がふぇぇだ数学教えろお前ら

あせろり @Aserorirori

ほんまこれ

スマートコン @mr_konn

Coq って矛盾してたのか……

Masaki Hara @qnighy

@mr_konn 現行のCoqは命題P,Qに対して(P<->Q) -> P = Q を仮定すると矛盾するバグがある

スマートコン @mr_konn

@qnighy やば

スマートコン @mr_konn

(P <-> Q) → P = Q が矛盾、つまり外延性公理が成り立たないみたいな感じに見える