跳到主要内容

千葉大学 融合理工学府 数学情報科学専攻 数学・情報数理学コース 2017年8月実施 専門 B10

Author

祭音Myyura (co-authored with GPT 6 Astra)

Description

等号付き一階古典述語論理を考え、ϕ\models\phi は論理的妥当性を表す。

(1) 二項関係記号 RR と一項関係記号 QQ に対して

ϕ=(xyR(x,y)zQ(z))\phi=(\exists x\forall y\,R(x,y)\to\forall z\,Q(z))

と同値な冠頭標準形を一つ求めよ。(2) 量化記号のない ϕ(x,y)\phi(x,y) に対して

xyϕ(x,y)    xθ(x)\models\exists x\forall y\,\phi(x,y)\iff\models\exists x\,\theta(x)

を満たす量化記号のない θ(x)\theta(x) を求めよ。(3) 二項関数記号を少なくとも一つ含む可算言語 LL について、任意の論理式を量化記号のない式に写し ϕ    F(ϕ)\models\phi\iff\models F(\phi) を満たす写像 FF は計算可能でないことを示せ。Church の定理を用いてよい。

题目描述

考虑带等号的一阶经典逻辑。(1) 将给定蕴涵式化为等价的前束范式。(2) 给定无量词公式 ϕ(x,y)\phi(x,y),求无量词 θ(x)\theta(x),使两个存在句的逻辑有效性满足上式等价。(3) 对包含至少一个二元函数符号的可数语言,证明保持有效性且输出无量词公式的变换不可能可计算,可用 Church 不可判定性定理。

Kai

(1) 変数の捕獲が生じないように量化子を移動すれば

xyz(¬R(x,y)Q(z))\boxed{\forall x\exists y\forall z\,(\neg R(x,y)\lor Q(z))}

を得る(通常どおり領域は空でないとする)。

(2) ϕ\phi に現れない一項関数記号 ff を新たに加えて

θ(x)=ϕ(x,f(x))\boxed{\theta(x)=\phi(x,f(x))}

とする。左辺が妥当ならば、任意の拡大構造で yϕ(a,y)\forall y\phi(a,y) を満たす aa をとれ、特に ϕ(a,f(a))\phi(a,f(a)) が成立する。

逆に左辺が妥当でないならば、ある構造で xy¬ϕ(x,y)\forall x\exists y\neg\phi(x,y) が成立する。各 aa に反例となる bab_a を選び f(a)=baf(a)=b_a と解釈すれば、拡大構造で x¬θ(x)\forall x\neg\theta(x)。従って右辺も妥当でない。これは新しい関数記号を用いた妥当性の保存であり、二つの式が同一構造で同値であるという主張ではない。

(3) 等号を含む量化記号のない式の妥当性は決定可能である。実際、その否定を選言標準形にし、各連言の充足可能性を調べればよい。有限個の出現項に対し、等式から生成される合同閉包を計算し、不等式の両辺や、真偽が逆に指定された同じ述語の引数組が同一視されるかを検査する。矛盾がなければ項の同値類上にモデルを構成できる。

もし FF が計算可能ならば、入力 ϕ\phi から F(ϕ)F(\phi) を計算し、その妥当性を上記手続きで決定することで LL の一階論理の妥当性を決定できる。これは Church の定理に反する。