1 一階述語論理

1.1 通常の論理記号

word(,p) … \(\top\)  \({\perp}\)
word(p,p) … \(\neg\)
word(pp,p) … \(,\)  \(\mathbin{\rm o\!r}\)  \(\Rightarrow\)  \(\Leftrightarrow\)
word(vp,p)R … \(\forall\)  \(\exists\)
word(ss,p) … \(=\)
word(cc,p) … \(=\)

1.2 高度な論理記号

word+(pp,p) … \({\bf ,}\,\)  \(\Longrightarrow\)  \(\Longleftrightarrow\)
lower … \(P {\bf ,}\, Q\) ≃ \(P , Q\)
lower … \(P \Longrightarrow Q\) ≃ \(P \Rightarrow Q\)
lower … \(P \Longleftrightarrow Q\) ≃ \(P \Leftrightarrow Q\)

word+(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
lower … \(A \stackrel{{\tt /}}{\mathbin{{\sf p}}} B\) ≃ \(\neg ( A \mathbin{{\sf p}} B )\)

1.3 andを含む略記法

2以上の自然数\({\tt n}\)に対し
abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
abbr … \(X_{1} \mathbin{{\sf p}_{1}} X_{2} \cdots \mathbin{{\sf p}_{\tt n\,{\text -}\,1}} X_{\tt n}\) ≈ \(( X_{1} \mathbin{{\sf p}_{1}} X_{2} ) , \cdots , ( X_{\tt n\,{\text -}\,1} \mathbin{{\sf p}_{\tt n\,{\text -}\,1}} X_{\tt n} )\)

1.4 量化子の略記法

1以上の自然数\({\tt n}\)に対し
abbr … \(\forall x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( P )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( P )\)
abbr … \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} \Longrightarrow ( P ) )\)
abbr … \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \mathop{{\sf A}} , \cdots , x_{\tt n} \mathop{{\sf A}} , ( P ) )\)

2以上の自然数\({\tt n}\)に対し
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\forall x_{1} \cdots \forall x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} P\) ≈ \(\exists x_{1} \cdots \exists x_{\tt n} ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)
abbr … \(\forall^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\forall x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} \Longrightarrow ( P ) )\)
abbr … \(\exists^* x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . P\) ≈ \(\exists x_{1} , \cdots , x_{\tt n} \mathop{{\sf A}} . ( x_{1} \neq x_{2} , \cdots\!\cdots , x_{\tt n\,{\text -}\,1} \neq x_{\tt n} , ( P ) )\)