量词可消去的线性序理论

杜芬芬，陈国龙

1.淮北师范大学数学科学学院，淮北，235000；2.宿州学院,宿州，234000

量词可消去的线性序理论

杜芬芬1，陈国龙2

1.淮北师范大学数学科学学院，淮北，235000；2.宿州学院,宿州，234000

量词消去法在模型论的证明中是应用很广的一种方法。本文主要讨论在语言L=<,0上的有首元但无末元的稠密线性序理论T和在语言L0=<上的无末元离散线性序理论T0的量词可消去性,及其在扩充语言L1=S,<下理论T0的量词消去性。

稠密；离散；线性序；量词消去

量词消去是模型论研究的重要工具，而对于可定义集上理论的研究，由于量词的存在使得研究变得相当复杂。由于一阶理论具有量词消去性质,所以对于该理论中公式的研究范围就可以缩小到无量词公式，这样就减少了研究的难度。

本文主要讨论有首元但无末元的稠密线性序理论和无末元的离散线性序理论。分别考虑语言L=<,0,语言L0=<及其扩充下的语言L1=S,<，其中<在它的模型中的解释是序关系,S被解释为后继函数。本文第1部分给出一些定义,第2部分证明理论T和T0分别在语言L=<,0和语言L1=S,<上具有量词消去性质，而T0在语言L0=<上量词不可消去的。

1 准备工作

定义1[1]设T为语言L中的理论，假如对T中的任意L-公式φ，存在无量词的L-公式ψ，使得

T╞φ↔ψ

则称理论T是量词可消去的。

定义2[2]设A,B是语言L的模型并且A⊆B。当下列条件成立时,称A为B的初等子模型,记作AB:对L中每一公式φx1，…，xn及A中每一n元组a1,…,an,都有

A╞φa1，…，an当且只当B╞φa1，…，an引理1[1]语言为L的理论T为量词可消去的当且仅当形为∃x∂1∧，…，∧∂k的所有公式量词可消去，这里∂i为L的原子公式或原子公式的否定。

引理2[2]设T是L中的理论,当T适合下列条件时,称为模型完全的:对T的任何模型A,B,若A⊆B,则AB。

2 主要结果的证明

定理1有首元但无末元的稠密线性序理论在语言L=<,0中是量词可消去的。

证明将该理论的公理集分类列在下面：

线性序公理：

A1∀x┐x

A2∀x∀y(x=y∨x

A3∀x∀y∀zx

稠密性公理：

B∀x∀y∃zx

首元0的公理：C1∀xx=0∨0

无末元的公理：C2∀x∃yx

根据引理1,只需要证明形为：

∃x∂1∧…∧∂r

(1)

的任意一个公式都可以等价到一个无量词公式。这里的∂i为L中原子公式或原子公式的否定，现在讨论∂i的多种可能形式。

假定t1和t2为语言中L的项，则它们可能为0,1或者变元，那么∂i一定为t1=t2，t1

又因为┐t1

奠基当r=1 时，公式(1)为∃xt1

归纳假定对一切r

∃x(x

(2)

其中ti,vi和ui为项，假定它们和x都不相同。假如ti=x或ui=x，那么(2)式可等价到假;如果vi=x，则(2)式可以归约到r=k-1的情形。

情形1当m>1时,(2)式可等价到：

(t1

∨┐x

该公式归约为r=k-1的情形。

当n>1时，那么(2)式可等价到：

(u1

该公式归约为r=k-1的情形。

情形2现在考察m=1,n=1的情形，则公式(2)可以写成:

∃xx

情形3其次考察m=0,n=1的情形，则公式(2)可写成:

∃xu1

如果l≠0，它等价到u1

情形4如果m=1,n=0，公式(2)可等价到：

∃xx

如果l≠0，它等价到v1

情形5最后考虑m=0,n=0的情形，则该公式可以等价到:

∃xx=v1∧…∧x=vl

那么该公式可以等价到真或假。

这样就证明了有首元但无末元的稠密线性序理论在语言L=<,0中是量词可消去的。

定理2无末元离散线性序的理论在语言L0=<中是量词不可消去的。

证明现将该理论公理集分类列在下面:

线性序公理:

A1∀x┐x

A2∀x∀y(x=y∨x

A3∀x∀y∀zx

D∀x∃yx

由Z╞T0,设Z0=Z∪1/3,可知Z0╞T0，显然Z⊆Z0。令Z0╞∃x0

定理3无末元的离散线性序理论在语言L1=S,<中是量词可消去的，这里的S是后继函数。

证明首先列出该理论的公理集。

线性序公理：

A1∀x┐x

A2∀x∀y(x=y∨x

A3∀x∀y∀zx

再定义后继函数和表示无末元的公理。

D1∀x∀yx

D2∀x∃yy=Sx

在一个语言L1中，项的一般形式为Sx=S，…，Sx(p次)，根据引理，只需证明形为

∃x∂1∧，…，∂r

(3)

的任意公式均可等价到一个无量词公式。这里∂i为L1中的原子公式或原子公式的否定。现在考察∂i的多种可能形式。

假定Sp1x1和Sp2x2为L1中的项，∂i必为Sp1x1

注意到┐(Sp1x1

下面使用归纳法证明，并归纳于原子公式∂i的个数r。

奠基r=1。

情形1Sp1x1

情形1.1x1和x2中至少有一个是x,比如x=x1,则∃xSp1x

情形1.2考虑x=x1=x2，那么如果p1

情形2Sp1x1=Sp2x2,则分为以下两种子情形。

情形2.1x1=x或x2=x,不失一般性，设x1=x,则∃xSp1x=Sp2x2或为真或为假，看是否存在首元。

情形2.2x1=x2=x,如果p1=p2,则该公式为真，否则为假。

下一步归纳证明的第2部分。

归纳假定对一切r

如果有某个∂i不含x，则可归约为k-1的情形,因此可设∂i中至少有一个x1或x2为x。如果某个∂i中有x1=x2=x，则该∂i形如Sp1x

下面将Spx=x1和Spx

∃x(x

(4)

这里ti，ui和vi均为形式为Spx的项，p为整数。

情形1当m>1时，公式(4)可等价到:

(t1

该公式归约为r=k-1的情形。

当n>1时，公式(4)可等价到:

u1

该公式归约为r=k-1的情形。

情形2现在考察m=1,n=1的情形，则公式(4)可写成:

∃xx

情形3考察m=0,n=1的情形，则公式(4)可写成:

∃xu1

如果l≠0，它等价到u1

情形4如果m=1,n=0，则公式(4)可写成:

∃xx

如果l≠0，它等价到v1

情形5最后考察m=0,n=0的情形,则该公式变为:

∃xx=v1∧…∧x=vl

那么该公式为真或假。

这样就证明了无终端离散线性序理论T0在语言L1=S,<中是量词可消去的。

[1]史念东.代数模型论引论[M].北京:科学出版社,2011:11-17

[2]王世强.模型论基础[M].北京:科学出版社,1987:1-10

[3]Marker D.Model Theory:An Introduction[M].北京:科学出版社,2007:71-83

[4]沈云付.素数阶群理论消去及复杂性[J].数学学报,2001,44(1):21-28

[5]沈绍恩.一类具有量词消去性质的偏序结构[J].科学通报,1992,23(37):13-14

(责任编辑：刘小阳)

2017-06-25

安徽省高校自然科学研究重大项目(KJ2014ZD31)。

杜芬芬(1992-)，女，安徽阜阳人，在读硕士研究生，研究方向：数理逻辑及其应用。

10.3969/j.issn.1673-2006.2017.10.025

O141.4

A

1673-2006(2017)10-0096-03