generated at
連言と二重否定の関係について
>(二重否定除去|排中律)なしに\lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)を証明できること、もしくは証明できないことを証明せよ

yuki_minoh
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
知らんけど
直観主義集合論?という言葉を見かけたからそれをちゃんと調べれば書けたりするのかな
ベン図を見る限りでは偽っぽい
直観主義論理は通常の真理値を対応させられないので、ベン図で解析できませんtakker
まぁそうですよねyuki_minoh
できた
真だった
正直なところ、否定導入での爆発律(矛盾からは何を導出しても良い)の操作がおぼつかなさすぎる
本当にこれでいいの?って感じ
可能なだけ調べたけど、どれも「何を導出してもいい」となっていて腑に落ちない
「仮定を閉じる」必要があると思うんだけど、直感主義論理での閉じ方がわからなかった
二重否定しなくていいのか?一重否定でも閉じたことになるのか?
\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
普通に考えれば(?)\lnot \lnot P
10
\lnot(\lnot P \lor \lnot Q) \implies \lnot \lnot(P\land Q)
含意導入:1,9
ここ自力で証明できなかった部分takker
検証します
yuki_minoh正直めっちゃ不安な部分あるのでお願いしますw
うわまじじゃん!あってる。すごいtakker
PQを連続して仮定として導入して先に進めるとは思っていなかった
こんなに仮定を入れまくったら、元に戻れず詰まりそうな予感がしたので試してなかった
実際にはこんなにうまく証明できるとは……
2回(?)の仮定で3つの矛盾を導けるのがいいポイントっすよねyuki_minoh
(2024-04-09) 二重否定を導く系の証明の常套手段としてよく使うようになりましたtakker
mjkyuki_minoh
嬉しい
途中式のインスピレーションは直観主義論理#結合子の定義不可能性 - Wikipediaから得た
いいヒントだった
これが証明できればもう題意も証明できたようなものですtakker
\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
どこかに公開されてますかね
見つけました
hr
以下メモ

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
問題を写す
>(二重否定除去|排中律)なしに\lnot\lnot P\land\lnot\lnot Q\implies\lnot\lnot(P\land Q)を証明できること、もしくは証明できないことを証明せよ
疑問
closed issue\impliesはどう解釈するか?
\vdashと解釈してよいか・すべきか
open issueその場合、どういう体系を使っているか
\vdash\impliesを区別せず使ってますtakker
本当は区別したほうがいい
実質同じ意味なので(数理論理学の深い話に立ち入らない限り)実害はない
\rightarrow\Rightarrowと解釈してよいか・すべきか
これは、まぁ同じ意味で使われてるのしか見たことないしいいでしょ
ここでは線の少ない\rightarrowを用いることにする
\lnot\lnot P\cdots Q)全体を見て「証明できる/できない」と言っているので、全体が命題になっている
\vdashは(きっと)命題を構成しないので、これは\Rightarrowの方が良さそう
仮置き
証明に用いる論理体系が不明だが、取り敢えず、直観主義論理を用いる
直観主義論理は、ちょうど古典論理から(二重否定除去|排中律)を制限したものであるため
次に、証明のためシークエント計算 LJ を用いる
LJ は直観主義論理の健全かつ完全な体系 https://ja.wikipedia.org/wiki/直観主義論理 なのでこれを用いる
LJ は LK の推論規則https://www2.yukawa.kyoto-u.ac.jp/~kanehisa.takasaki/edu/logic/logic9.htmlを適用していく際に、\vdashの右辺の論理式が高々1つになるように制限することで得られる
問題文をシークエント計算風に書き直す
> 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が「できる」って言ってるのと食い違う結果が出た
takkerもできたtakker
取り敢えず、どちらがどこをミスっているのかがわからない

ちゃんと証明してなかったので証明したtakker
比較にどうぞ
引用されている定理が 3 つか 4 つもあって検証が大変そうやな(感想)Summer498
定理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}
定理2. 二重否定導入: これはOK
\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
シークエント計算には不慣れなので時間かかる
仮定P\vdash Qはどこで落としているんだろう
定理4. ((P\rightarrow Q)\rightarrow(\lnot Q\rightarrow \lnot P))らしい
定理 3 が 真ではないので、もういい
なんか帰着元の問題があるらしいSummer498
これ定理 3 じゃね