連言と二重否定の関係について
(二重否定除去|排中律)なしに$ \lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)を証明できること、もしくは証明できないことを証明せよ yuki_minoh.icon
$ P \land Q \implies \lnot\lnot(P\land Q)が自明
つまり$ (\lnot\lnot P\land\lnot\lnot Q) \implies P \land Qを示せれば題与の定理が手に入る
$ \lnot\lnot(P\land Q)を含意しつつ、$ \lnot\lnot P\land \lnot \lnot Qの仮定だけで示せるような、他の途中式を考える必要がある
そんなんある？
多分$ \lnot\lnot P\land \lnot \lnot Qに同値な変形じゃないと無理
$ \lnot\lnot P\land \lnot \lnot Qのベン図、3重円で理解できる気がする
できないと思うyuki_minoh.icon
知らんけど
直観主義集合論？という言葉を見かけたからそれをちゃんと調べれば書けたりするのかな
ベン図を見る限りでは偽っぽい
直観主義論理は通常の真理値を対応させられないので、ベン図で解析できませんtakker.icon
まぁそうですよねyuki_minoh.icon
できた
真だった
正直なところ、否定導入での爆発律（矛盾からは何を導出しても良い）の操作がおぼつかなさすぎる 本当にこれでいいの？って感じ
可能なだけ調べたけど、どれも「何を導出してもいい」となっていて腑に落ちない
「仮定を閉じる」必要があると思うんだけど、直感主義論理での閉じ方がわからなかった 二重否定しなくていいのか？一重否定でも閉じたことになるのか？
$ \lnot\lnot P\land \lnot \lnot Q \implies \lnot(\lnot P \lor \lnot Q)を証明し、その次に$ \lnot(\lnot P \lor \lnot Q) \implies \lnot\lnot(P\land Q)を証明する
$ \lnot\lnot P\land \lnot \lnot Q \implies \lnot(\lnot P \lor \lnot Q)の証明
1
$ \lnot\lnot P\land \lnot \lnot Q
仮定
2
$ \lnot P \lor \lnot Q
仮定
3
$ \lnot P
仮定
4
$ \lnot \lnot P
連言除去:1
5
$ \lnot(\lnot P \lor \lnot Q)
否定導入:2,3,4
6
$ \lnot Q
仮定
7
$ \lnot \lnot Q
連言除去:1
8
$ \lnot(\lnot P \lor \lnot Q)
否定導入:2,6,7
9
$ \lnot(\lnot P \lor \lnot Q)
選言除去:2,3,5,6,8
10
$ \lnot\lnot P\land \lnot \lnot Q \implies \lnot(\lnot P \lor \lnot Q)
含意導入:1,9
$ \lnot(\lnot P \lor \lnot Q) \implies \lnot\lnot(P\land Q)の証明
1
$ \lnot(\lnot P \lor \lnot Q)
仮定
2
$ \lnot(P\land Q)
仮定
3
$ P
仮定
4
$ Q
仮定
5
$ P \land Q
連言導入:3,4
5
$ \lnot Q
否定導入:2,5
6
$ \lnot P \lor \lnot Q
連言導入:5
7
$ \lnot P
否定導入:3,6
8
$ \lnot P \lor \lnot Q
連言導入:7
9
$ \lnot \lnot(P\land Q)
否定導入:2,8
この操作めっちゃくちゃ不安yuki_minoh.icon
普通に考えれば（？）$ \lnot \lnot P
10
$ \lnot(\lnot P \lor \lnot Q) \implies \lnot \lnot(P\land Q)
含意導入:1,9
ここ自力で証明できなかった部分takker.icon
検証します
yuki_minoh.icon正直めっちゃ不安な部分あるのでお願いしますw
うわまじじゃん!あってる。/icons/すごい.icontakker.icon
https://kakeru.app/5044f86f860d9f1cb8d17b47934d2a0b https://i.kakeru.app/5044f86f860d9f1cb8d17b47934d2a0b.svg
$ Pと$ Qを連続して仮定として導入して先に進めるとは思っていなかった
こんなに仮定を入れまくったら、元に戻れず詰まりそうな予感がしたので試してなかった
実際にはこんなにうまく証明できるとは……
2回(?)の仮定で3つの矛盾を導けるのがいいポイントっすよねyuki_minoh.icon
(2024-04-09) 二重否定を導く系の証明の常套手段としてよく使うようになりましたtakker.icon
mjkyuki_minoh.icon
嬉しい
いいヒントだった
これが証明できればもう題意も証明できたようなものですtakker.icon
$ \lnot(\lnot P \lor \lnot Q) \implies \lnot\lnot(P\land Q)から$ \lnot(P\land Q)\implies\lnot\lnot(\lnot P\lor\lnot Q)(弱いド・モルガンの法則)を導ける もともと$ \lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)を証明する目的は、直観主義論理下で$ \lnot(P\land Q)\implies\lnot\lnot(\lnot P\lor\lnot Q)が成立するかどうかを調べることでした
僕のみてない部分の証明も含めて見れたら嬉しいですyuki_minoh.icon
どこかに公開されてますかね
見つけました
/icons/hr.icon
以下メモ
1
$ P \land Q
仮定
2
$ P
連言除去:1
3
$ \lnot\lnot P
二重否定導入
4
Q
連言除去:1
5
$ \lnot\lnot Q
二重否定導入
6
$ \lnot\lnot P\land\lnot\lnot Q
連言導入: 3,5
7
$ \lnot\lnot(P\land Q)
二重否定導入:1
8
$ (\lnot\lnot P\land\lnot\lnot Q ) \land \lnot\lnot(P\land Q)
連言導入:6,7
9
$ P \land Q \implies (\lnot\lnot P\land\lnot\lnot Q ) \land \lnot\lnot(P\land Q)
$ \implies導入:1,8
Summer498.icon
問題を写す
(二重否定除去|排中律)なしに$ \lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)を証明できること、もしくは証明できないことを証明せよ 疑問
closed issue.icon$ \impliesはどう解釈するか？
$ \vdashと解釈してよいか・すべきか
open issue.iconその場合、どういう体系を使っているか
$ \vdashと$ \impliesを区別せず使ってますtakker.icon
本当は区別したほうがいい
実質同じ意味なので(数理論理学の深い話に立ち入らない限り)実害はない
$ \rightarrowや$ \Rightarrowと解釈してよいか・すべきか
これは、まぁ同じ意味で使われてるのしか見たことないしいいでしょ
ここでは線の少ない$ \rightarrowを用いることにする
$ \lnot\lnot P\cdots Q)全体を見て「証明できる/できない」と言っているので、全体が命題になっている
$ \vdashは(きっと)命題を構成しないので、これは$ \Rightarrowの方が良さそう
仮置き
証明に用いる論理体系が不明だが、取り敢えず、直観主義論理を用いる 次に、証明のためシークエント計算 LJ を用いる
問題文をシークエント計算風に書き直す
LJ で$ \vdash\lnot\lnot P\land\lnot\lnot Q\rightarrow\lnot\lnot(P\land Q)を証明できること、もしくは証明できないことを証明せよ
証明図
注: 下から読んでいくこと
最後(一番上)で二重否定除去を要求しているため、回答は「証明できない」
$ \begin{matrix}\frac{\displaystyle\frac{\lnot\lnot P\vdash P}{\lnot\lnot P\land\lnot\lnot Q\vdash P}(\land 左)\qquad\frac{\lnot\lnot Q\vdash Q}{\lnot\lnot P\land\lnot\lnot Q\vdash Q}(\land左)}{\displaystyle\lnot\lnot P\land\lnot\lnot Q\vdash P\land Q}&(\land右)\\\overline{\lnot(P\land Q),\lnot\lnot P\land\lnot\lnot Q\vdash}&(\lnot左)\\\overline{\lnot\lnot P\land\lnot\lnot Q\vdash\lnot\lnot(P\land Q)}&(\lnot右)\\\overline{\vdash\lnot\lnot P\land\lnot\lnot Q\rightarrow\lnot\lnot(P\land Q)}&(\rightarrow右)\end{matrix}
うるさい注意書き
$ \lnot左を適用した後に$ \lnot右を適用する動作をしているが、
これは二重否定生成であり、二重否定除去ではないことに注意
二重否定除去のためには$ \lnot右を適用した後に$ \lnot左を適用する
一番最後(一番上)の$ \land左の操作で恣意的に今後の見通しが良い方を選んでいるが、
選ばなかった方のルートを通ると$ \lnot\lnot Q\rightarrow Pや$ \lnot\lnot P\rightarrow Qを仮定する必要がありやはり証明できない
疑問
上でyuki minoh.iconが「できる」って言ってるのと食い違う結果が出た
takker.iconもできたtakker.icon
取り敢えず、どちらがどこをミスっているのかがわからない
ちゃんと証明してなかったので証明したtakker.icon
比較にどうぞ
引用されている定理が 3 つか 4 つもあって検証が大変そうやな(感想)Summer498.icon
定理1. $ \vdash\lnot P \land \lnot Q \rightarrow \lnot(P\lor Q)らしい→合ってる。LJで証明
$ \begin{matrix}{\displaystyle \begin{matrix}{P\vdash P}&(初期)\\\overline{P, \lnot P \vdash}&(\lnot左)\\\overline{P, \lnot P \land \lnot Q \vdash}&(\land左)\end{matrix}\qquad\begin{matrix}{Q\vdash Q}&(初期)\\\overline{Q, \lnot Q \vdash}&(\lnot 左)\\\overline{Q, \lnot P \land \lnot Q \vdash}&(\land左)\end{matrix}}\\\begin{matrix}\overline{(P\lor Q), \lnot P \land \lnot Q \vdash}&(\lor左)\\\overline{\lnot P \land \lnot Q \vdash \lnot(P\lor Q)}&(\lnot右)\\\overline{\vdash\lnot P \land \lnot Q \rightarrow \lnot(P\lor Q)}&(\rightarrow右)\end{matrix}\end{matrix}
$ \begin{matrix}P\vdash P&(初期)\\\overline{\lnot P,P\vdash}&(\lnot 左)\\\overline{P\vdash\lnot\lnot P}&(\lnot右)\\\overline{\vdash P\rightarrow\lnot\lnot P}&(\rightarrow右)\end{matrix}
定理3. $ \lnot(P\land Q)\rightarrow\lnot\lnot(\lnot P \lor\lnot Q)らしい→ 真ではないっぽい
$ \begin{matrix}\begin{matrix}\begin{matrix}{P\vdash P (初期), P\vdash Q(仮定)}&\\\overline{P\vdash P\land Q}&(\land右)\\\overline{P,\lnot(P\land Q)\vdash}&(\lnot左)\\\overline{\lnot(P\land Q)\vdash\lnot P}&(\lnot右)\end{matrix}\end{matrix}\\{\begin{matrix}\overline{\lnot(P\land Q)\vdash\lnot P \lor\lnot Q}&(\lor右)\\\overline{\lnot(\lnot P \lor\lnot Q),\lnot(P\land Q)\vdash}&(\lnot 左)\\\overline{\lnot(P\land Q)\vdash\lnot\lnot(\lnot P \lor\lnot Q)}&(\lnot 右)\\\overline{\vdash\lnot(P\land Q)\rightarrow\lnot\lnot(\lnot P \lor\lnot Q)}&(\rightarrow右)\end{matrix}}\end{matrix}
でもなんかおかしいぞ
$ P\rightarrow Qもしくは$ Q\rightarrow Pの仮定が必要←←なんか変
$ Q\rightarrow Pの方は$ (\lor右)の適用の際に残る方を$ \lnot Pの代わりに$ \lnot Qにすると出てくる
真ではないのはともかく、二重否定除去と関係のない理由で真ではなくなってるのがおかしく見える
右辺に 2 つの式が存在することを避けるために普段は行かないルートで計算をしたが、それで謎の仮定を要求された？
普段は行かないルート: $ (\lor右)のタイミング。
普段ならここで$ \lnot左したくなるが、そうすると右辺に式が二つ存在するタイミングがあるのでダメ
つまり、真であっても正しいルートで行かないと証明にならない？←これがなんか変に見える
そうでもない
解読中takker.icon
仮定$ P\vdash Qはどこで落としているんだろう
定理4. $ ((P\rightarrow Q)\rightarrow(\lnot Q\rightarrow \lnot P))らしい
定理 3 が 真ではないので、もういい
なんか帰着元の問題があるらしいSummer498.icon
これ定理 3 じゃね