∀x∃y(P(x)∧Q(y))⇒∃y∀x(P(x)∧Q(y))
証明の求め方
最初、$ \forall x\exist y(P(x)\land Q(y))\implies\forall xP(x)\land\exist yQ(y)\implies\exist y\forall x(P(x)\land Q(y))という経路に気づいて、そのように証明図を書いた
その後、より短くなるようrefactoringした
code:proof.tikz(tex)
\usepackage{fitch}
\begin{document}
$\Large\begin{nd}
\hypo {h} {\forall x\exists y(P(x)\land Q(y))}
\have {upq} {\exists y(P(u)\land Q(y))} \Ae{h}
\hypo {vpq} {P(u)\land Q(v)}
\have {vq} {Q(v)} \ae{vpq}
\have {wpq} {\exists y(P(w)\land Q(y))} \Ae{h}
\hypo {zpq} {P(w)\land Q(z)}
\have {zp} {P(w)} \ae{zpq}
\close
\have {p} {P(w)} \Ee{wpq,zpq-zp}
\have {pq} {P(w)\land Q(v)} \ai{p,vq}
\close
\have {apq} {\forall x(P(x)\land Q(v))} \Ai{pq}
\have {eapq} {\exists y\forall x(P(x)\land Q(y))} \Ei{apq}
\close
\have {eapq2} {\exists y\forall x(P(x)\land Q(y))} \Ee{upq,vpq-eapq}
\close
\have {aeapq} {\forall u\exists y\forall x(P(x)\land Q(y))} \Ai{eapq2}
\have {e} {\exists y\forall x(P(x)\land Q(y))} \Ae{aeapq}
\end{nd}$
\end{document}