一意存在の同値変形
いずれここにもその証明の手順を書いておくつもり
書いていて、集合との関係を思いついた
書き出し終わると、とても当たり前のことだと気づくのだが、こういうのを自力で論理立てて導出するのがとても楽しいtakker.icon*3
https://kakeru.app/0e46f60bc1d0b68819a565b62fb56fa6 https://i.kakeru.app/0e46f60bc1d0b68819a565b62fb56fa6.svg
導出される論理式
$ \begin{dcases}\exists x \in A;P(x)\\\exists x \in A\forall y\in A; P(y)\implies x=y\end{dcases}\iff\exists x \in A;\begin{dcases}P(x)\\\forall y\in A;P(y)\implies x=y\end{dcases}
$ \impliedbyは自明。$ \impliesも成立するというのがこの論理式の主旨
導出メモ
https://kakeru.app/738ab7fc7e197ca11c6b9a5b80d4a44d https://i.kakeru.app/738ab7fc7e197ca11c6b9a5b80d4a44d.svg
もっと遡ると、等号の性質を使っている
この同値変形のコアとなる論理式
$ \left(\forall x,y\in A;\begin{dcases}P(x)\\P(y)\end{dcases}\implies x=y\right)\iff\left(\exist x\in A\forall y\in A;P(y)\implies x=y\right)
導出
https://kakeru.app/ea28178d0e6a4c982f9995a5d42ac126 https://i.kakeru.app/ea28178d0e6a4c982f9995a5d42ac126.svg
2021-03-08 01:03:05 もしかして二重否定除去なしに$ (L)\implies(R)は証明できない？ もし必要なのだとしたら、一体どこで使っているんだ？
2024-03-21 08:16:01 昨日か一昨日あたりに証明図を作れた
頭から書き起こしておく
https://scrapbox.io/files/6602155557a8ba00245549c7.svg
code:proof.tikz(tex)
\usepackage{fitch}
\usepackage{amsmath}
\begin{document}
$\Large\begin{nd}
\hypo {aapp} {\forall x\forall y(P(x)\land P(y)\implies x=y)}
\open
\hypo {ne} {\lnot\exists x\forall y(P(y)\implies x=y)}
\have {app} {\forall y(P(u)\land P(y)\implies u=y)} \Ae{aapp}
\open
\hypo {pu} {P(u)}
\have {ppuv} {P(u)\land P(v)\implies u=v} \Ae{app}
\open
\hypo {pv} {P(v)}
\have {pp} {P(u)\land P(v)} \ai{pu,pv}
\have {uv} {u=v} \ie{pp,ppuv}
\close
\have {puv} {P(v)\implies u=v} \ii{pv-uv}
\close
\have {ap} {\forall y(P(y)\implies u=y)} \Ai{puv}
\have {eap} {\exists x\forall y(P(y)\implies x=y)} \Ei{ap}
\have {b} {\bot} \ne{ne,eap}
\have {tu} {t=u} \be{b}
\close
\have {ptu} {P(u)\implies t=u} \ii{pu-tu}
\close
\have {apty} {\forall y(P(y)\implies t=y)} \Ai{ptu}
\have {eap} {\exists x\forall y(P(y)\implies x=y)} \Ei{apty}
\have {b} {\bot} \ne{ne,eap}
\close
\have {ab} {\forall t\bot} \Ai{b}
\have {b} {\bot} \Ae{ab}
\close
\have {nne} {\lnot\lnot\exists x\forall y(P(y)\implies x=y)} \ii{ne-b}
\end{nd}$
\end{document}
逆に、この論理式から二重否定除去を導けるかはわからない
もし導ければ、この論理式の証明に二重否定除去が不可欠だと示せる