Tome of Knowledge 1.0.2

この著者は初心者として投稿しています。間違いや考慮が足りていない点が含まれている可能性が高いです。見つけたらコメント欄で優しく指摘してあげましょう。

$$\newcommand{aa}[0]{\unicode{x0259}} \newcommand{aaa}[0]{\unicode{x028C}} \newcommand{ae}[0]{\unicode{x00E6}} \newcommand{ae}[0]{\unicode{x1D02}} \newcommand{akebi}[0]{\unicode{x599B}} \newcommand{Be}[0]{\unicode{x0411}} \newcommand{be}[0]{\unicode{x0431}} \newcommand{beach}[0]{\unicode{x26F1}} \newcommand{beu}[0]{\unicode{x3142}} \newcommand{che}[0]{\unicode{x0447}} \newcommand{Che}[0]{\unicode{x0427}} \newcommand{cheu}[0]{\unicode{x314A}} \newcommand{CLASS}[0]{\texttt{CLASS}} \newcommand{cod}[0]{\texttt{cod}} \newcommand{coeq}[0]{\texttt{coeq}} \newcommand{COEQ}[0]{\texttt{COEQ}} \newcommand{coker}[0]{\mathrm{coker}} \newcommand{COLIM}[0]{\texttt{COLIM}} \newcommand{CRing}[0]{\texttt{CRing}} \newcommand{De}[0]{\unicode{x0414}} \newcommand{de}[0]{\unicode{x0434}} \newcommand{deu}[0]{\unicode{x3137}} \newcommand{dom}[0]{\texttt{dom}} \newcommand{e}[0]{\unicode{x044D}} \newcommand{E}[0]{\unicode{x042D}} \newcommand{earth}[0]{\unicode{x2641}} \newcommand{ee}[0]{\unicode{x026A}} \newcommand{eight}[0]{\unicode{x266A}} \newcommand{El}[0]{\unicode{x041B}} \newcommand{el}[0]{\unicode{x043B}} \newcommand{em}[0]{\unicode{x043C}} \newcommand{En}[0]{\unicode{x041D}} \newcommand{en}[0]{\unicode{x043D}} \newcommand{EPI}[0]{\texttt{EPI}} \newcommand{eq}[0]{\texttt{eq}} \newcommand{EQ}[0]{\texttt{EQ}} \newcommand{eu}[0]{\unicode{x3147}} \newcommand{fe}[0]{\unicode{x0444}} \newcommand{flat}[0]{\unicode{x266D}} \newcommand{four}[0]{\unicode{x2669}} \newcommand{ga}[0]{\unicode{x0433}} \newcommand{gear}[0]{\unicode{x26ED}} \newcommand{geu}[0]{\unicode{x3131}} \newcommand{Grp}[0]{\texttt{Grp}} \newcommand{heu}[0]{\unicode{x314E}} \newcommand{Hom}[0]{\texttt{Hom}} \newcommand{I}[0]{\unicode{x0418}} \newcommand{i}[0]{\unicode{x0438}} \newcommand{ik}[0]{\unicode{x0439}} \newcommand{Ik}[0]{\unicode{x0419}} \newcommand{ISO}[0]{\texttt{ISO}} \newcommand{Je}[0]{\unicode{x0416}} \newcommand{je}[0]{\unicode{x0436}} \newcommand{jeu}[0]{\unicode{x3148}} \newcommand{jjeu}[0]{\unicode{x3149}} \newcommand{jupiter}[0]{\unicode{x2643}} \newcommand{justice}[0]{\unicode{x2696}} \newcommand{ka}[0]{\unicode{x043A}} \newcommand{Ka}[0]{\unicode{x041A}} \newcommand{keu}[0]{\unicode{x314B}} \newcommand{kkeu}[0]{\unicode{x3132}} \newcommand{kou}[0]{\unicode{x2F58}} \newcommand{lmoon}[0]{\unicode{x263D}} \newcommand{LT}[0]{\texttt{LT}} \newcommand{LU}[0]{\texttt{LU}} \newcommand{MAGMA}[0]{\texttt{MAGMA}} \newcommand{Map}[0]{\texttt{Map}} \newcommand{mars}[0]{\unicode{x2642}} \newcommand{mercury}[0]{\unicode{x263F}} \newcommand{meu}[0]{\unicode{x3141}} \newcommand{MONO}[0]{\texttt{MONO}} \newcommand{Mya}[0]{\unicode{x042C}} \newcommand{mya}[0]{\unicode{x044C}} \newcommand{natural}[0]{\unicode{x266E}} \newcommand{neptune}[0]{\unicode{x2646}} \newcommand{neu}[0]{\unicode{x3134}} \newcommand{oa}[0]{\unicode{x0294}} \newcommand{oe}[0]{\unicode{x0153}} \newcommand{On}[0]{\texttt{On}} \newcommand{oo}[0]{\unicode{x0275}} \newcommand{ooo}[0]{\unicode{x0254}} \newcommand{ot}[0]{\texttt{OT}} \newcommand{pe}[0]{\unicode{x043F}} \newcommand{peu}[0]{\unicode{x314D}} \newcommand{pluto}[0]{\unicode{x2647}} \newcommand{po}[0]{\texttt{PO}} \newcommand{ppeu}[0]{\unicode{x3143}} \newcommand{qgear}[0]{\unicode{x26EE}} \newcommand{raa}[0]{\unicode{x0279}} \newcommand{Rel}[0]{\texttt{Rel}} \newcommand{reu}[0]{\unicode{x3139}} \newcommand{rmoon}[0]{\unicode{x263E}} \newcommand{RT}[0]{\texttt{RT}} \newcommand{RU}[0]{\texttt{RU}} \newcommand{saturn}[0]{\unicode{x2644}} \newcommand{scissors}[0]{\unicode{x2702}} \newcommand{Set}[0]{\texttt{Set}} \newcommand{Set}[0]{\texttt{Set}} \newcommand{seu}[0]{\unicode{x3145}} \newcommand{sh}[0]{\unicode{x0283}} \newcommand{sha}[0]{\unicode{x0448}} \newcommand{Sha}[0]{\unicode{x0428}} \newcommand{shaa}[0]{\unicode{x0255}} \newcommand{sharp}[0]{\unicode{x266F}} \newcommand{shcha}[0]{\unicode{x0449}} \newcommand{Shcha}[0]{\unicode{x0429}} \newcommand{Spec}[0]{\texttt{Spec}} \newcommand{sseu}[0]{\unicode{x3146}} \newcommand{suc}[0]{\mathfrak{S}} \newcommand{sun}[0]{\unicode{x2609}} \newcommand{sword}[0]{\unicode{x2694}} \newcommand{thaa}[0]{\unicode{x00F0}} \newcommand{TO}[0]{\texttt{TO}} \newcommand{tse}[0]{\unicode{x0446}} \newcommand{Tse}[0]{\unicode{x0426}} \newcommand{tteu}[0]{\unicode{x3138}} \newcommand{U}[0]{\unicode{x0423}} \newcommand{ui}[0]{\unicode{x044B}} \newcommand{Ui}[0]{\unicode{x042B}} \newcommand{uo}[0]{\unicode{x0264}} \newcommand{uranus}[0]{\unicode{x2645}} \newcommand{uu}[0]{\unicode{x00F8}} \newcommand{ve}[0]{\unicode{x0432}} \newcommand{venus}[0]{\unicode{x2640}} \newcommand{WO}[0]{\texttt{WO}} \newcommand{ya}[0]{\unicode{x044F}} \newcommand{Ya}[0]{\unicode{x042F}} \newcommand{Yel}[0]{\unicode{x042A}} \newcommand{yel}[0]{\unicode{x044A}} \newcommand{Yu}[0]{\unicode{x042E}} \newcommand{yu}[0]{\unicode{x044E}} \newcommand{yuu}[0]{\unicode{x028F}} \newcommand{Ze}[0]{\unicode{x0417}} \newcommand{ze}[0]{\unicode{x0437}} $$

1.0.2 一階述語論理の構成

(メタ)

$L$を言語, $A, B$を$L$-formulaとする.
(1) $(\neg A)^{\ast}$は$!A^{\ast}$と略記法として一致.
(2) $(!A)^{\ast}$は$\neg A^{\ast}$と略記法として一致.
(3) $(A \vee B)^{\ast}$は$A^{\ast} \land B^{\ast}$と略記法として一致.
(4) $(A \land B)^{\ast}$は$A^{\ast} \vee B^{\ast}$と略記法として一致.
(5) $(A \to B)^{\ast}$は$!A^{\ast} \land B^{\ast}$と略記法として一致.

略記法として一致するというメタ記法を$\sim$とおく.
\begin{align} (\neg A)^{\ast} &\sim (A \uparrow A)^{\ast} \\ &\sim A^{\ast} \downarrow A^{\ast} \\ &\sim !A^{\ast} \end{align}
略記法として一致するというメタ記法を$\sim$とおく.
\begin{align} (!A)^{\ast} &\sim (A \downarrow A)^{\ast} \\ &\sim A^{\ast} \uparrow A^{\ast} \\ \neg A^{\ast} \end{align}
略記法として一致するというメタ記法を$\sim$とおく.
\begin{align} (A \vee B)^{\ast} &\sim (\neg A \uparrow \neg B)^{\ast} \\ &\sim (\neg A)^{\ast} \downarrow (\neg B)^{\ast} \\ &\sim !A^{\ast} \downarrow !B^{\ast} \\ &\sim A^{\ast} \land B^{\ast} \end{align}
略記法として一致するというメタ記法を$\sim$とおく.
\begin{align} (A \vee B)^{\ast} &\sim (!A \downarrow !B)^{\ast} \\ &\sim (!A)^{\ast} \uparrow (!B)^{\ast} \\ &\sim \neg A^{\ast} \uparrow \neg B^{\ast} \\ &\sim A^{\ast} \vee B^{\ast} \end{align}
略記法として一致するというメタ記法を$\sim$とおく.
\begin{align} (A \to B)^{\ast} &\sim (\neg A \vee B)^{\ast} \\ &\sim (\neg A)^{\ast} \land B^{\ast} \\ &\sim !A^{\ast} \land B^{\ast} \end{align}

$L$を言語, $A$を$L$-formulaとする.
(1) $:: \neg\neg A \vdash A$.
(2) $:: A \vdash !!A$
(3) $:: A \vdash \neg\neg A$
(4) $:: !!A \vdash A$
(5) $:: \neg A \vdash !A$
(6) $:: !A \vdash \neg A$

\begin{align} \neg A &\vdash \neg A \\ \neg A \uparrow \neg A, \neg A, \neg A &\vdash \\ \neg A \uparrow \neg A, \neg A &\vdash \\ \neg\neg A, \neg A &\vdash \\ \neg\neg A, \neg A &\vdash \bot \\ \neg\neg A &\vdash A \end{align}
\begin{align} \neg\neg A &\vdash A \\ (\neg\neg A &\vdash A)^{\ast} \\ A^{\ast} &\vdash (\neg\neg A)^{\ast} \\ A^{\ast} &\vdash !(\neg A)^{\ast} \\ A^{\ast} &\vdash !!A^{\ast} \\ A &\vdash !!A \end{align}
\begin{align} A &\vdash A \\ A, \neg A &\vdash \bot \\ A, \neg A, \neg A &\vdash \bot \\ A, \neg A, \neg A &\vdash \\ A &\vdash \neg\neg A \end{align}
\begin{align} A &\vdash \neg\neg A \\ (A &\vdash \neg\neg A)^{\ast} \\ (\neg\neg A)^{\ast} &\vdash A^{\ast} \\ !(\neg A)^{\ast} &\vdash A^{\ast} \\ !! A^{\ast} &\vdash A^{\ast} \\ !!A &\vdash A \end{align}
\begin{align} \top &\vdash A, !A \\ \neg A &\vdash !A \end{align}
\begin{align} A, \neg A &\vdash \bot \\ \neg A &\vdash !A \end{align}

$L$を言語, $\Gamma$をcontextとする.
(1) $\top \vdash \Gamma :: \vdash \Gamma$
(2) $\Gamma \vdash \bot :: \Gamma \vdash$

\begin{align} \top \vdash \Gamma \\ \vdash \top \\ \vdash \Gamma \end{align}
\begin{align} \top \vdash \Gamma &:: \vdash \Gamma \\ (\top \vdash \Gamma)^{\ast} &:: (\vdash \Gamma)^{\ast} \\ \Gamma^{\ast} \vdash \bot &:: \Gamma^{\ast} \vdash \\ \Gamma \vdash \bot &:: \Gamma \vdash \end{align}

$L$を言語, $\Gamma, \Delta, \Sigma, \Pi, \Xi, \Upsilon$をcontext, $A, B$を$L$-formulaとする.
(1) $\Gamma, A \vdash \Delta :: \Gamma \vdash \Delta, \neg A$
(2) $\Delta \vdash A, \Gamma :: !A, \Delta \vdash \Gamma$
(3) $\Gamma \vdash \Delta, A :: \Gamma \vdash \Delta, A \vee B$
(4) $A, \Delta \vdash \Gamma :: A \land B, \Delta \vdash \Gamma$
(5) $\Gamma \vdash \Delta, B :: \Gamma \vdash \Delta, A \vee B$
(6) $B, \Delta \vdash \Gamma :: A \land B, \Delta \vdash \Gamma$
(7) $(\Gamma \vdash \Delta, A \vee B), (A, \Pi \vdash \Sigma), (B, \Xi \vdash \Upsilon) :: \Gamma, \Pi, \Xi \vdash \Delta, \Sigma, \Upsilon$
(8) $(A \land B, \Delta \vdash \Gamma), (\Sigma \vdash \Pi, A), (\Upsilon \vdash \Xi, B) :: \Upsilon, \Sigma, \Delta \vdash \Xi, \Pi, \Gamma$
(9) $(A, \Gamma \vdash \Delta), (B, \Sigma \vdash \Pi) :: A \vee B, \Gamma, \Sigma \vdash \Delta, \Pi$
(10) $(\Delta \vdash \Gamma, A), (\Pi \vdash \Sigma, B) :: \Delta, \Pi \vdash \Sigma, \Gamma, A \land B$
(11) $\Gamma, A \vdash \Delta, B :: \Gamma \vdash \Delta, A \to B$
(12) $(\Gamma \vdash \Delta, A), (B, \Sigma \vdash \Pi) :: A \to B, \Gamma, \Sigma \vdash \Delta, \Pi$
(13) $(\Gamma \vdash \Delta, A, \Pi), (\Sigma \vdash \Xi, A \to B, \Upsilon) :: \Gamma, \Sigma \vdash \Delta, \Pi, B, \Xi, \Upsilon$

\begin{align} \Gamma, A &\vdash \Delta \\ \Gamma &\vdash !A, \Delta \\ !A &\vdash \neg A \\ \Gamma &\vdash \neg A, \Delta \\ \Gamma &\vdash \Delta, \neg A \end{align}
\begin{align} \Gamma, A \vdash \Delta &:: \Gamma \vdash \Delta, \neg A \\ (\Gamma, A \vdash \Delta)^{\ast} &:: (\Gamma \vdash \Delta, \neg A)^{\ast} \\ \Delta^{\ast} \vdash A^{\ast}, \Gamma^{\ast} &:: !A^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast} \\ \Delta \vdash A, \Gamma &:: !A, \Delta \vdash \Gamma \end{align}
\begin{align} \Gamma &\vdash \Delta, A \\ \Gamma, \neg A &\vdash \Delta \\ \neg B, \Gamma, \neg A &\vdash \Delta \\ \neg A, \neg B, \Gamma &\vdash \Delta \\ \Gamma &\vdash \Delta, \neg A \uparrow \neg B \\ \Gamma &\vdash \Delta, A \vee B \end{align}
\begin{align} \Gamma \vdash \Delta, A &:: \Gamma \vdash \Delta, A \vee B \\ (\Gamma \vdash \Delta, A)^{\ast} &:: (\Gamma \vdash \Delta, A \vee B)^{\ast} \\ A^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast} &:: A^{\ast} \land B^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast} \\ A, \Delta \vdash \Gamma &:: A \land B, \Delta \vdash \Gamma \end{align}
\begin{align} \Gamma &\vdash \Delta, B \\ \Gamma, \neg B &\vdash \Delta \\ \neg A, \Gamma, \neg B &\vdash \Delta \\ \neg A, \neg B, \Gamma &\vdash \Delta \\ \Gamma &\vdash \Delta, \neg A \uparrow \neg B \\ \Gamma &\vdash \Delta, A \vee B \end{align}
\begin{align} \Gamma \vdash \Delta, B &:: \Gamma \vdash \Delta, A \vee B \\ (\Gamma \vdash \Delta, A)^{\ast} &:: (\Gamma \vdash \Delta, A \vee B)^{\ast} \\ A^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast} &:: A^{\ast} \land B^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast} \\ A, \Delta \vdash \Gamma &:: A \land B, \Delta \vdash \Gamma \end{align}
\begin{align} A, \Pi &\vdash \Sigma \\ \Pi &\vdash \Sigma, \neg A \\ B, \Xi &\vdash \Upsilon \\ \Xi &\vdash \Upsilon, \neg B \\ \neg A \uparrow \neg B, \Pi, \Xi &\vdash \Sigma, \Upsilon \\ A \vee B, \Pi, \Xi &\vdash \Sigma, \Upsilon \\ \Gamma &\vdash \Delta, A \vee B \\ \Gamma, \Pi, \Xi &\vdash \Delta, \Sigma, \Upsilon \end{align}
\begin{align} (\Gamma \vdash \Delta, A \vee B), (A, \Pi \vdash \Sigma), (B, \Xi \vdash \Upsilon) &:: \Gamma, \Pi, \Xi \vdash \Delta, \Sigma, \Upsilon \\ ((\Gamma \vdash \Delta, A \vee B), (A, \Pi \vdash \Sigma), (B, \Xi \vdash \Upsilon))^{\ast} &:: (\Gamma, \Pi, \Xi \vdash \Delta, \Sigma, \Upsilon)^{\ast} \\ (A^{\ast} \land B^{\ast}, \Delta^{\ast} \vdash \Gamma^{\ast}), (\Sigma^{\ast} \vdash \Pi^{\ast}, A^{\ast}), (\Upsilon^{\ast} \vdash \Xi^{\ast}, B^{\ast}) &:: \Upsilon^{\ast}, \Sigma^{\ast}, \Delta^{\ast} \vdash \Xi^{\ast}, \Pi^{\ast}, \Gamma^{\ast} \\ (A \land B, \Delta \vdash \Gamma), (\Sigma \vdash \Pi, A), (\Upsilon \vdash \Xi, B) &:: \Upsilon, \Sigma, \Delta \vdash \Xi, \Pi, \Gamma \end{align}
\begin{align} A, \Gamma &\vdash \Delta \\ \Gamma &\vdash \Delta, \neg A \\ B, \Sigma &\vdash \Pi \\ \Sigma &\vdash \Pi, \neg B \\ \neg A \uparrow \neg B, \Gamma, \Sigma &\vdash \Delta, \Pi \\ A \vee B, \Gamma, \Sigma &\vdash \Delta, \Pi \\ \end{align}
\begin{align} (A, \Gamma \vdash \Delta), (B, \Sigma \vdash \Pi) &:: A \vee B, \Gamma, \Sigma \vdash \Delta, \Pi \\ ((A, \Gamma \vdash \Delta), (B, \Sigma \vdash \Pi))^{\ast} &:: (A \vee B, \Gamma, \Sigma \vdash \Delta, \Pi)^{\ast} \\ (\Delta^{\ast} \vdash \Gamma^{\ast}, A^{\ast}), (\Pi^{\ast} \vdash \Sigma^{\ast}, B^{\ast}) &:: \Pi^{\ast}, \Delta^{\ast} \vdash \Sigma^{\ast}, \Gamma^{\ast}, A^{\ast} \land B^{\ast} \\ (\Delta \vdash \Gamma, A), (\Pi \vdash \Sigma, B) &:: \Delta, \Pi \vdash \Sigma, \Gamma, A \land B \\ \end{align}
\begin{align} \Gamma, A &\vdash \Delta, B \\ \Gamma &\vdash \Delta, B, \neg A \\ \Gamma &\vdash \Delta, B, \neg A \vee B \\ \Gamma &\vdash \Delta, \neg A \vee B, B \\ \Gamma &\vdash \Delta, A \to B, B \\ \Gamma &\vdash \Delta, A \to B, \neg A \vee B \\ \Gamma &\vdash \Delta, A \to B, A \to B \\ \Gamma &\vdash \Delta, A \to B \end{align}
\begin{align} \neg A &\vdash !A \\ \Gamma &\vdash \Delta, A \\ !A, \Gamma &\vdash \Delta \\ \neg A, \Gamma &\vdash \Delta \\ B, \Sigma &\vdash \Pi \\ \neg A \vee B, \Gamma, \Sigma &\vdash \Delta, \Pi \\ A \to B, \Gamma, \Sigma &\vdash \Delta, \Pi \end{align}
\begin{align} \vdash A, \neg A \\ \end{align}

$L$を言語, $A, B, C$を$L$-formulaとする.
(1) $:: \vdash A \to A$
(2) $:: !A \land A \vdash $
(3) $:: A \vdash A \vee A$
(4) $:: A \land A \vdash A$
(5) $:: A \vee A \vdash A$
(6) $:: A \vdash A \land A$
(7) $:: A \vee B \vdash B \vee A$
(8) $:: A \land B \vdash B \land A$
(9) $:: (A \vee B) \vee C \vdash A \vee (B \vee C)$
(10) $:: A \land (B \land C) \vdash (A \land B) \land C$
(11) $:: A \vee (B \vee C) \vdash (A \vee B) \vee C$
(12) $:: (A \land B) \land C \vdash A \land (B \land C)$
(13) $:: A \vee (B \land C) \vdash (A \vee B) \land (A \vee C)$
(14) $:: (A \land B) \vee (A \land C) \vdash A \land (B \vee C)$
(15) $:: (A \vee B) \land (A \vee C) \vdash A \vee (B \land C)$
(16) $:: A \land (B \vee C) \vdash (A \land B) \vee (A \land C)$
(17) $:: \neg (A \land B) \vdash \neg A \vee \neg B$
(18) $:: \neg A \land \neg B \vdash \neg (A \vee B)$
(19) $:: \neg A \vee \neg B \vdash \neg (A \land B)$
(20) $:: \neg (A \vee B) \vdash \neg A \land \neg B$
(21) $::A \to B, A \vdash B$
(22) $:: A \to B \vdash \neg B \to \neg A$
(23) $:: \neg B \to \neg A \vdash A \to B$
(24) $:: A \to B, B \to C \vdash A \to C$

\begin{align} A &\vdash A \\ &\vdash A \to A \end{align}
\begin{align} &\vdash A \to A \\ (A \to A)^{\ast} &\vdash \\ !A \land A &\vdash \end{align}
\begin{align} A &\vdash A \\ A &\vdash A \vee A \end{align}
\begin{align} A &\vdash A \vee A \\ (A \vee A)^{\ast} &\vdash A^{\ast} \\ A^{\ast} \land A^{\ast} &\vdash A^{\ast} \\ A \land A &\vdash A \end{align}
\begin{align} A \vee A &\vdash A \vee A \\ A &\vdash A \\ A \vee A &\vdash A \end{align}
\begin{align} A \vee A &\vdash A \\ A^{\ast} &\vdash (A \vee A)^{\ast} \\ A^{\ast} &\vdash A^{\ast} \land A^{\ast} \\ A &\vdash A \land A \end{align}
\begin{align} A \vee B &\vdash A \vee B \\ A &\vdash A \\ A &\vdash B \vee A \\ B &\vdash B \\ B &\vdash B \vee A \\ A \vee B &\vdash B \vee A \end{align}
\begin{align} B \vee A &\vdash A \vee B \\ (A \vee B)^{\ast} &\vdash (B \vee A)^{\ast} \\ A^{\ast} \land B^{\ast} &\vdash B^{\ast} \land A^{\ast} \\ A \land B &\vdash B \land A \end{align}
\begin{align} (A \vee B) \vee C &\vdash (A \vee B) \vee C \\ A \vee B &\vdash A \vee B \\ A &\vdash A \vee (B \vee C) \\ B &\vdash B \\ B &\vdash B \vee C \\ B &\vdash A \vee (B \vee C) \\ A \vee B &\vdash A \vee (B \vee C) \\ C &\vdash C \\ C &\vdash B \vee C \\ C &\vdash A \vee (B \vee C) \\ (A \vee B) \vee C &\vdash A \vee (B \vee C) \end{align}
\begin{align} (A \vee B) \vee C &\vdash A \vee (B \vee C) \\ (A \vee (B \vee C))^{\ast} &\vdash ((A \vee B) \vee C)^{\ast} \\ A^{\ast} \land (B^{\ast} \land C^{\ast}) &\vdash (A^{\ast} \land B^{\ast}) \land C^{\ast} \\ A \land (B \land C) &\vdash (A \land B) \land C \\ \end{align}
\begin{align} A \vee (B \vee C) &\vdash A \vee (B \vee C) \\ A &\vdash A \\ A &\vdash A \vee B \\ A &\vdash (A \vee B) \vee C \\ B \vee C &\vdash B \vee C \\ B &\vdash B \\ B &\vdash A \vee B \\ B &\vdash (A \vee B) \vee C \\ C &\vdash C \\ C &\vdash (A \vee B) \vee C \\ B \vee C &\vdash (A \vee B) \vee C \\ A \vee (B \vee C) &\vdash (A \vee B) \vee C \end{align}
\begin{align} A \vee (B \vee C) &\vdash (A \vee B) \vee C \\ (A \vee (B \vee C))^{\ast} &\vdash ((A \vee B) \vee C)^{\ast} \\ (A^{\ast} \land B^{\ast}) \land C^{\ast} &\vdash A^{\ast} \land (B^{\ast} \land C^{\ast}) \\ (A \land B) \land C &\vdash A \land (B \land C) \end{align}
\begin{align} A \vee (B \land C) &\vdash A \vee (B \land C) \\ A &\vdash A \\ A &\vdash A \vee B \\ A &\vdash A \vee C \\ A &\vdash (A \vee B) \land (A \vee C) \\ B &\vdash B \\ B \land C &\vdash B \\ B \land C &\vdash A \vee B \\ C &\vdash C \\ B \land C &\vdash C \\ B \land C &\vdash A \vee C \\ B \land C &\vdash (A \vee B) \land (A \vee C) \\ A \vee (B \land C) &\vdash (A \vee B) \land (A \vee C) \end{align}
\begin{align} A \vee (B \land C) &\vdash (A \vee B) \land (A \vee C) \\ (A \vee (B \land C))^{\ast} &\vdash ((A \vee B) \land (A \vee C))^{\ast} \\ A^{\ast} \land (B^{\ast} \vee C^{\ast}) &\vdash (A^{\ast} \land B^{\ast}) \vee (A^{\ast} \land C^{\ast}) \\ A \land (B \vee C) &\vdash (A \land B) \vee (A \land C) \end{align}
\begin{align} (A \vee B) \land (A \vee C) &\vdash A \vee B \\ A &\vdash A \\ A &\vdash A \vee (B \land C) \\ (A \vee B) \land (A \vee C) &\vdash A \vee C \\ A, B &\vdash A \\ A, B &\vdash A \vee (B \land C) \\ C, B &\vdash B \\ C, B &\vdash C \\ C, B &\vdash B \land C \\ C, B &\vdash A \vee (B \land C) \\ B &\vdash A \vee (B \land C) \\ (A \vee B) \land (A \vee C) &\vdash A \vee (B \land C) \end{align}
\begin{align} (A \vee B) \land (A \vee C) &\vdash A \vee (B \land C) \\ (A \vee (B \land C))^{\ast} &\vdash ((A \vee B) \land (A \vee C))^{\ast} \\ A^{\ast} \land (B^{\ast} \vee C^{\ast}) &\vdash (A^{\ast} \land B^{\ast}) \vee (A^{\ast} \land C^{\ast}) \\ A \land (B \vee C) &\vdash (A \land B) \vee (A \land C) \end{align}
\begin{align} A &\vdash A \\ A &\vdash A \vee B \\ &\vdash A \vee B, \neg A \\ B &\vdash B \\ B &\vdash A \vee B \\ &\vdash A \vee B, \neg B \\ &\vdash A \vee B, A \vee B, \neg A \land \neg B \\ &\vdash A \vee B, \neg A \land \neg B \\ !(A \vee B) &\vdash \neg A \land \neg B \\ \neg (A \vee B) &\vdash !(A \vee B) \\ \neg (A \vee B) &\vdash \neg A \land \neg B \end{align}
\begin{align} \neg (A \vee B) &\vdash \neg A \land \neg B \\ (\neg A \land \neg B)^{\ast} &\vdash (\neg (A \vee B))^{\ast} \\ !A^{\ast} \vee !B^{\ast} &\vdash !(A^{\ast} \land B^{\ast}) \\ \neg A^{\ast} &\vdash !A^{\ast} \\ \neg A^{\ast} &\vdash !A^{\ast} \vee !B^{\ast} \\ \neg A^{\ast} &\vdash !(A^{\ast} \land B^{\ast}) \\ \neg B^{\ast} &\vdash !B^{\ast} \\ \neg B^{\ast} &\vdash !A^{\ast} \vee !B^{\ast} \\ \neg B^{\ast} &\vdash !(A^{\ast} \land B^{\ast}) \\ \neg A^{\ast} \vee \neg B^{\ast} &\vdash !(A^{\ast} \land B^{\ast}) \\ !(A^{\ast} \land B^{\ast}) &\vdash \neg (A^{\ast} \land B^{\ast}) \\ \neg A^{\ast} \land \neg B^{\ast} &\vdash \neg (A^{\ast} \land B^{\ast}) \\ \neg A \land \neg B &\vdash \neg (A \land B) \end{align}
\begin{align} \neg A \vee \neg B &\vdash \neg A \vee \neg B \\ A &\vdash A \\ A \land B &\vdash A \\ !A, A \land B &\vdash \\ A \land B, !A &\vdash \\ !A &\vdash \neg (A \land B) \\ \neg A &\vdash !A \\ \neg A &\vdash \neg (A \land B) \\ B &\vdash B \\ A \land B &\vdash B \\ !B, A \land B &\vdash \\ A \land B, !B &\vdash \\ !B &\vdash \neg (A \land B) \\ \neg B &\vdash !B \\ \neg B &\vdash \neg (A \land B) \\ \neg A \vee \neg B &\vdash \neg (A \land B) \end{align}
\begin{align} \neg A \vee \neg B &\vdash \neg (A \land B) \\ (\neg (A \land B))^{\ast} &\vdash (\neg A \vee \neg B)^{\ast} \\ !(A^{\ast} \vee B^{\ast}) &\vdash !A^{\ast} \land !B^{\ast} \\ !A^{\ast} \land !B^{\ast} &\vdash !A^{\ast} \\ !A^{\ast} &\vdash \neg A^{\ast} \\ !A^{\ast} \land !B^{\ast} &\vdash \neg A^{\ast} \\ !A^{\ast} \land !B^{\ast} &\vdash !B^{\ast} \\ !B^{\ast} &\vdash \neg B^{\ast} \\ !A^{\ast} \land !B^{\ast} &\vdash \neg B^{\ast} \\ !A^{\ast} \land !B^{\ast} &\vdash \neg A^{\ast} \land \neg B^{\ast} \\ !(A^{\ast} \vee B^{\ast}) &\vdash \neg A^{\ast} \land \neg B^{\ast} \\ \neg (A^{\ast} \vee B^{\ast}) &\vdash !(A^{\ast} \vee B^{\ast}) \\ \neg (A^{\ast} \vee B^{\ast}) &\vdash \neg A^{\ast} \land \neg B^{\ast} \\ \neg (A \vee B) &\vdash \neg A \land \neg B \end{align}
\begin{align} A &\vdash A \\ B &\vdash B \\ A \to B, A &\vdash B \end{align}
\begin{align} A \to B, A &\vdash B \\ A \to B, A, !B &\vdash \\ \neg B &\vdash !B \\ A \to B, A, \neg B &\vdash \\ A, A \to B, \neg B &\vdash \\ A \to B, \neg B &\vdash \neg A \\ A \to B &\vdash \neg B \to \neg A \end{align}
\begin{align} A &\vdash A \\ A, !A &\vdash \\ \neg A &\vdash !A \\ A, \neg A &\vdash \\ B &\vdash B \\ &\vdash B, \neg B \\ \neg B \to \neg A, A &\vdash B \\ \neg B \to \neg A &\vdash A \to B \end{align}
\begin{align} A \to B, A &\vdash B \\ B \to C, B &\vdash C \\ A \to B, A, B \to C &\vdash C \\ A \to B, B \to C, A &\vdash C \\ A \to B, B \to C &\vdash A \to C \end{align}

$L$を言語, $A, B$を$L$-formula, $\Gamma$をcontextとする.
(1) $A, B \vdash \Gamma :: A \land B \vdash \Gamma$
(2) $\Gamma \vdash A, B :: \Gamma \vdash A \vee B$
(3) $A \land B \vdash \Gamma :: A, B \vdash \Gamma$
(4) $\Gamma \vdash A \vee B :: \Gamma \vdash A, B$

\begin{align} A, B &\vdash \Gamma \\ A \land B, B &\vdash \Gamma \\ B, A \land B &\vdash \Gamma \\ A \land B, A \land B &\vdash \Gamma \\ A \land B &\vdash \Gamma \end{align}
\begin{align} A, B \vdash \Gamma &:: A \land B \vdash \Gamma \\ (A, B \vdash \Gamma)^{\ast} &:: (A \land B \vdash \Gamma)^{\ast} \\ \Gamma^{\ast} \vdash B^{\ast}, A^{\ast} &:: \Gamma^{\ast} \vdash A^{\ast} \vee B^{\ast} \\ \Gamma \vdash B, A &:: \Gamma \vdash A \vee B \\ \Gamma \vdash A, B &:: \Gamma \vdash A \vee B \end{align}
\begin{align} A &\vdash A \\ B &\vdash B \\ A, B &\vdash A \land B \\ A \land B &\vdash \Gamma \\ A, B &\vdash \Gamma \end{align}
\begin{align} A \land B \vdash \Gamma &:: A, B \vdash \Gamma \\ (A \land B \vdash \Gamma)^{\ast} &:: (A, B \vdash \Gamma)^{\ast} \\ \Gamma^{\ast} \vdash A^{\ast} \vee B^{\ast} &:: \Gamma^{\ast} \vdash B^{\ast}, A^{\ast} \\ \Gamma \vdash A \vee B &:: \Gamma \vdash B, A \\ \Gamma \vdash A \vee B &:: \Gamma \vdash A, B \end{align}

$L$を言語, $x$を変数記号, $s, t, u, T_2, \dots, T_n$を$L$-term, $A$をアリティ$n$の関数記号とする.
(1) $::s = t \vdash t = s$
(2) $::s = t, t = u \vdash s = u$
(3) $::s = t \vdash A(s, T_2, \dots, T_n) = A(t, T_2 \dots, T_n)$

\begin{align} s = t, s = s &\vdash t = s \\ &\vdash s = s \\ s = t &\vdash t = s \end{align}
\begin{align} t = u, s = t &\vdash s = u \\ s = t, t = u &\vdash s = u \end{align}
\begin{align} s = t, A(s, T_2, \dots, T_n) = A(s, T_2, \dots, T_n) &\vdash A(s, T_2, \dots, T_n) = A(t, T_2, \dots, T_n) \\ &\vdash A(s, T_2, \dots, T_n) = A(s, T_2, \dots, T_n) \\ s = t &\vdash A(s, T_2, \dots, T_n) = A(t, T_2, \dots, T_n) \end{align}

$L$を言語, $x$を変数記号, $s, t, u, T_2, \dots, T_n$を$L$-term, $A$をアリティ$n$の関数記号とする.
(1) $\neg\forall x [A(x)] \vdash \exists x [\neg A(x)]$
(2) $\forall x [\neg A(x)] \vdash \neg \exists x [A(x)]$
(3) $\neg\exists x [A(x)] \vdash \forall x [\neg A(x)]$
(4) $\exists x [\neg A(x)] \vdash \neg\forall x [A(x)]$

投稿日：15日前

数学の力で現場を変えるアルゴリズムエンジニア募集 - Mathlog served by OptHub

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。

投稿者

未見姫ゆめ

169

self-containedに数学を書ききることを大目標にしています. Youtubeチャンネル:未見姫ゆめ【学術:Academic】

他の人のコメント

コメントはありません。

読み込み中

未見姫ゆめ

Tome of Knowledge 1.0.2