【数学・論理学】$\lnot(P\lor Q)\vdash\lnot P\land\lnot Q$ の形式証明

ただの備忘録。命題論理のある体系での形式証明。 \begin{align*} \text{公理}&:P\rightarrow P\lor Q\\ \text{公理}&:\lnot(P\lor Q)\rightarrow(P\rightarrow\lnot(P\lor Q))\\ \text{仮定}&:\lnot(P\lor Q)\\ \text{2,3行からの推論}&:P\rightarrow\lnot(P\lor Q)\\ \text{公理}&:(P\rightarrow P\lor Q)\rightarrow( (P\rightarrow\lnot(P\lor Q) )\rightarrow\lnot P)\\ \text{1,5行からの推論}&:(P\rightarrow\lnot(P\lor Q) )\rightarrow\lnot P\\ \text{4,6行からの推論}&:\lnot P\\ \text{公理}&:Q\rightarrow P\lor Q\\ \text{公理}&:\lnot(P\lor Q)\rightarrow(Q\rightarrow\lnot(P\lor Q))\\ \text{3,9行からの推論}&:Q\rightarrow\lnot(P\lor Q)\\ \text{公理}&:(Q\rightarrow P\lor Q)\rightarrow( (Q\rightarrow\lnot(P\lor Q) )\rightarrow\lnot Q)\\ \text{8,11行からの推論}&:(Q\rightarrow\lnot(P\lor Q) )\rightarrow\lnot Q\\ \text{10,12行からの推論}&:\lnot Q\\ \text{公理}&:\lnot P\rightarrow(\lnot Q\rightarrow\lnot P\land\lnot Q)\\ \text{7,14行からの推論}&:\lnot Q\rightarrow\lnot P\land\lnot Q\\ \text{13,15行からの推論}&:\lnot P\land\lnot Q \end{align*}