∀P(∀A,B(P(A)∧A⊆B⇒P(B))⇔∀A,B(P(A∩B)⇒P(A)∧P(B)))

$ \forall P(\forall A\forall B(P(A)\land A\subseteq B\implies P(B))\iff\forall A\forall B(P(A\cap B)\implies P(A)\land P(B)))

証明

(L)⇒(R)

https://scrapbox.io/files/6a13e78665e24daf8cb5daf9.svg

code:L→R.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {L} {\forall A\forall B(P(A)\land A\subseteq B\implies P(B))}

\open

\hypo {PAB} {P(A\cap B)}

\have {ABA} {A\cap B\subseteq A}

\have {ABB} {A\cap B\subseteq B}

\have {PABABAPA} {P(A\cap B)\land A\cap B\subseteq A\implies P(A)} \Ae{L}

\have {PABABBPB} {P(A\cap B)\land A\cap B\subseteq B\implies P(B)} \Ae{L}

\have {PABABA} {P(A\cap B)\land A\cap B\subseteq A} \ai{PAB,ABA}

\have {PABABB} {P(A\cap B)\land A\cap B\subseteq B} \ai{PAB,ABB}

\have {PA} {P(A)} \ie{PABABAPA,PABABA}

\have {PB} {P(B)} \ie{PABABBPB,PABABB}

\have {PAPB} {P(A)\land P(B)} \ai{PA,PB}

\close

\have {a} {P(A\cap B)\implies P(A)\land P(B)} \ii{PAB-PAPB}

\close

\have {b} {\forall B(P(A\cap B)\implies P(A)\land P(B))} \Ai{a}

\close

\have {R} {\forall A\forall B(P(A\cap B)\implies P(A)\land P(B))} \Ai{b}

\end{nd}$

\end{document}

(R)⇒(L)

https://scrapbox.io/files/6a13e95465e24daf8cb5dfc7.svg

code:R→L.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {R} {\forall A\forall B(P(A\cap B)\implies P(A)\land P(B))}

\open

\hypo {PAAB} {P(A)\land A\subseteq B}

\have {PA} {P(A)} \ae{PAAB}

\have {AB} {A\subseteq B} \ae{PAAB}

\have {ABB} {A=A\cap B} \ie{AB}

\have {PAB} {P(A\cap B)} \by{=E}{PA,ABB}

\have {PABPAPB} {P(A\cap B)\implies P(A)\land P(B)} \Ae{R}

\have {PAPB} {P(A)\land P(B)} \ie{PAB,PABPAPB}

\have {PB} {P(B)} \ae{PAPB}

\close

\have {PAABPB} {P(A)\land A\subseteq B\implies P(B)} \ii{PAAB-PB}

\close

\have {a} {\forall B(P(A)\land A\subseteq B\implies P(B))} \Ai{PAABPB}

\close

\have {L} {\forall A\forall B(P(A)\land A\subseteq B\implies P(B))} \Ai{a}

\end{nd}$

\end{document}

code:L→R.tikz(tex)

\usepackage{fitch}

\usepackage{amsmath}

\begin{document}

$\Large\begin{nd}

\hypo {L} {\forall A\forall B(P(A)\land A\subseteq B\implies P(B))}

\open

\hypo {PAB} {P(A\cap B)}

\have {ABA} {A\cap B\subseteq A}

\have {ABB} {A\cap B\subseteq B}

\have {PABABAPA} {P(A\cap B)\land A\cap B\subseteq A\implies P(A)} \Ae{L}

\have {PABABBPB} {P(A\cap B)\land A\cap B\subseteq B\implies P(B)} \Ae{L}

\have {PABABA} {P(A\cap B)\land A\cap B\subseteq A} \ai{PAB,ABA}

\have {PABABB} {P(A\cap B)\land A\cap B\subseteq B} \ai{PAB,ABB}

\have {PA} {P(A)} \ie{PABABAPA,PABABA}

\have {PB} {P(B)} \ie{PABABBPB,PABABB}

\have {PAPB} {P(A)\land P(B)} \ai{PA,PB}

\close

\have {a} {P(A\cap B)\implies P(A)\land P(B)} \ii{PAB-PAPB}

\close

\have {b} {\forall B(P(A\cap B)\implies P(A)\land P(B))} \Ai{a}

\close

\have {R} {\forall A\forall B(P(A\cap B)\implies P(A)\land P(B))} \Ai{b}

\end{nd}$

\end{document}