独立友好的逻辑（二）

3. IF 一阶逻辑的语法和语义

在文献中，人们可以找到本质上不同的“IF 一阶逻辑”表述。这些差异不仅限于语法——还可以找到应用不同语义思想的示例。

正如已经指出的，Skolem 函数和玩家 2 的策略函数之间存在系统联系。与 prenex 形式的公式相关，存在量词的 Skolem 函数是分配给前面全称量词的值的函数，但不是分配给前面的存在量词的值的函数。[15] Skolem 函数是仅将玩家 1 的动作作为参数的策略函数。通常，两人游戏中玩家的策略可以很好地利用任一玩家之前的选择。 Hodges (2007) 强调，不完美信息的语义所基于的概念——Skolem 函数或策略函数——是有区别的。 Hodges (1997a) 采用了记法约定，例如 Hintikka 写作 (∃y/∀x) 的地方是 (∃y/x)，因此标志着以任意策略函数形式表述的语义博弈与策略函数为实际上 Skolem 功能； (∃y/x) 中的变量 x 可以被任何语法上前面带有变量 x 的量词“绑定”。 Hodges建议采用前一种表述，而Hintikka（1991、1995、1996、2002）和Sandu（1993、1994）则采用后一种表述。 Hodges (2007: 119) 写道：

[W]e 将我的符号和一般游戏语义的逻辑称为斜线逻辑。近年来，该领域的许多作者（但从未是 Hintikka 本人）已将“IF 逻辑”这一名称转移为斜杠逻辑，但往往没有意识到其中的区别。在术语确定下来之前，我们必须警惕那些无法明确说明其语义的示例和证明。

Hodges 对斜杠逻辑和 IF 逻辑所做的区分有助于对文献中发现的 IF 一阶逻辑的不同表述的混杂进行排序。 [16]

3.1.句法

IF 一阶逻辑是一阶逻辑的扩展。现在，任何一阶公式都相当于一阶公式，其中没有变量同时出现为自由和束缚，并且其中没有两个嵌套量词携带相同的变量。满足这两个语法条件的公式将被称为正则公式。从今以后，我们系统地限制对常规一阶公式的关注。[17]词汇表（签名，非逻辑术语）是关系符号（每个符号都带有固定的元数）、函数符号（同样每个符号都带有固定的元数）和常量符号的任何可数集合 τ。词汇表τ的一阶逻辑将被称为FO[τ]。这里假设一阶逻辑的逻辑符号中存在恒等符号(=)。身份符号在语法上是二元关系符号，但其语义解释是固定的，而非逻辑术语中的项目的解释则不然。

如果所有出现的否定符号 ∼ 都紧接在原子公式之前，则 FO[τ] 的公式处于否定范式。词汇表 τ（或 IFL[τ]）的 IF 一阶逻辑的公式集合可以定义为最小集合，使得：

如果 是 FO[τ] 的负范式公式，则 是公式。

如果 phi 是一个公式，并且 phi 中的标记 (∃x) 出现在许多全称量词的句法范围内，其中包括 (∀y1),…,(∀yn)，则将 ( 的标记替换 phi 中的结果∃x) × (∃x/∀y1,…,∀yn) 是一个公式。

如果 phi 是一个公式，并且在 phi 中，∨ 的标记出现在许多全称量词的语法范围内，其中包括 (∀y1),…,(∀yn)，则将 phi 中 ∨ 的标记替换为 (∨) /∀y1,…,∀yn) 是一个公式。

如果 phi 是一个公式，并且在 phi 中，(∀x) 的记号出现在许多存在量词的句法范围内，其中包括 (∃y1),…,(∃yn)，则将 ( ∀x) × (∀x/∃y1,…,∃yn) 是一个公式。

如果 phi 是一个公式，并且在 phi 中，∧ 的标记出现在许多存在量词的语法范围中，其中包括 (∃y1),…,(∃yn)，则将 phi 中 ∧ 的标记替换为 (∧) /∃y1,…,∃yn) 是一个公式。

子句 (2) 和 (3) 允许全称量词列表为空 (n=0) 的简并情况。得到的表达式 (∃x/) 和 (∨/) 分别用通常的存在量词 (∃x) 和通常的析取 ∨ 来标识。第(4)、(5)条也有类似规定。

在合适的词汇中，以下各项都是一个公式：

(∀x)(∀y)(∃z/∀x)R(x,y,z,v),

(∀x)(∀y)(x=y(∨/∀x)Q(x,y)),

(∃x)(S(x)(∧/∃x)T(x)),

(∀x)(∃y)(∀z/∃y)(∃v/∀x)R(x,y,z,v)。

相比之下，以下符号序列都不是公式：

(∃y/∀x)P(x,y),

(∃x)(∃y/∃x)P(x,y),

(∀x)(∀y/∀x)P(x,y),

(∀x)(S(x)(∨/∃y)T(x))。

如果 是 IFL 公式，由上述子句根据某些 FO 公式 phi* 生成，则 phi 的自由变量就是 phi* 的自由变量。没有自由变量的 IFL 公式是 IFL 语句。[18]

3.2.语义学

使用 GTS 定义逻辑的语义是一个两步过程。第一步是定义相关的语义游戏。第二步是根据语义游戏定义“真”和“假”的概念；这是通过参考获胜策略的概念而发生的。语义游戏可以通过递归地指定与给定公式 相关的游戏开始的替代方式来定义。[19]

对于每个词汇 τ、IFL[τ] 公式 phi、模型（τ 结构）M 和变量分配 g，玩家 1 和玩家 2 之间的两人零和博弈 G(phi,M,g) 相关联。[ 20]如果 g 是变量赋值，则 g[x/a] 是变量赋值，否则与 g 类似，但将变量 x 映射到对象 a。

如果 phi=R(t1,…,tn) 且 M,g⊨R(t1,…,tn)，玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 phi=t1=t2 且 M,g⊨t1=t2，则玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 phi=∼R(t1,…,tn) 且 M,g⊭R(t1,…,tn)，玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 phi=∼t1=t2 且 M,g⊭t1=t2，则玩家 2 获胜（玩家 1 失败）；否则玩家 1 获胜（玩家 2 失败）。

如果 ψ=(ψ(∧/∃y1,…,∃yn)χ)，玩家 1 选择 θε{ψ,χ}，其余游戏如 G(θ,M,g) 所示。

如果 ψ=(ψ(∨/∀y1,…,∀yn)χ)，玩家 2 选择 θ∈{ψ,χ}，其余游戏如 G(θ,M,g) 所示。

如果 ψ=(∀x/∃y1,…,∃yn)ψ，玩家 1 从 M 中选择一个元素 a，剩下的游戏就如 G(ψ,M,g[x/a]) 所示。

如果 ψ=(∃x/∀y1,…,∀yn)ψ，玩家 2 从 M 中选择一个元素 a，剩下的游戏就如 G(ψ,M,g[x/a]) 所示。

请注意，独立性指示在游戏规则中不起任何作用。事实上，量词独立性将在策略层面上实现。

如果在全称量词 ∀y1,…,∀yn,∀z1 范围内的公式 Φ 中出现 (∨/∀y1,…,∀yn) 或 (∃x/∀y1,…,∀yn) 标记,…,∀zm（并且只有这些通用量词），游戏 G(phi,M,g) 中玩家 2 对于该令牌的策略函数为任意函数 f 满足以下条件：

f 的参数是玩家 1 选择的元素 a1,…,am 来解释量词 ∀z1,…,∀zm。当标记是析取时，值 f(a1,…,am) 是左或右析取；当标记是存在量词时，是域的元素。

玩家 1 对于 (∧/∃y1,…,∃yn) 和 (∀x/∃y1,…,∃yn) 代币的策略函数的概念可以双重定义。策略函数被解释为 Skolem 函数——这里不考虑在斜杠逻辑中运行的策略函数的更一般概念（参见第 3 节和第 6.1 小节的开头）。量词独立性将直接根据策略函数的参数来实现。

游戏 G(phi,M,g) 中玩家 2 的策略是她的策略函数的集合 F，每个函数对应 (∨/∀y1,…,∀yn) 和 (∃x/∀y1,… ,∀yn) 出现在 ψ 中。据说玩家 2 遵循策略 F，如果对于 (∨/∀y1,…,∀yn) 和 (∃x/∀y1,…,∀yn) 的每个标记，她必须在游戏 G(玩 phi,M,g) 时，她根据相应的策略函数确定移动。 G(phi,M,g) 中玩家 2 的获胜策略是策略 F，这样针对玩家 1 的任何移动序列，遵循策略 F 都会为玩家 2 带来胜利。策略和获胜策略的概念可以类似为玩家 1 定义。[21]

模型M中IFL公式在赋值g下的满足和不满意定义如下：[22]

（满足）当且仅当玩家 2 在游戏 G(phi,M,g) 中存在获胜策略时，在 g 下的 M 中满足 phi。

（不满意）当且仅当玩家 1 在游戏 G(phi,M,g) 中存在获胜策略时，在 g 下的 M 中 phi 不满意。

与 FO 一样，变量赋值不会影响句子的（不）满足，即不包含自由变量的公式。事实上，我们可以定义：[23]

（真值）当且仅当玩家 2 在游戏 G(phi,M) 中存在获胜策略时，在 M 中 phi 为真。

（虚假）当且仅当游戏 G(phi,M) 中玩家 1 存在获胜策略时，M 中的 phi 是错误的。

Φ 在 M 中为真这一事实将被表示为“M⊨Φ”。那么，写成 M⊭Φ 表明 Φ 在 M 中不为真。这并不意味着 Φ 在上述定义的意义上是假的。 M. 正如第 2 节末尾提到的，存在语义博弈，其中双方都没有获胜策略。

IFL 的语法可以通过删除限制来概括，根据该限制，否定符号只能出现在原子公式的前缀中。[24]。为了解释 GTS 中的否定，在游戏规范中添加了两个角色：“验证者”和“证伪者”。最初，玩家 1 的角色是“证伪者”，玩家 2 的角色是“证伪者”。验证者。角色可能会互换，但只有一个原因：当遇到否定符号时。所有定义语义游戏的条款都必须根据角色而不是玩家来重新表述。角色为“验证者”的玩家会针对析取和存在量词采取行动，同样，角色为“证伪者”的玩家会针对合取和全称量词采取行动。当遇到公式∼ψ时，玩家交换角色，游戏继续ψ。最后，如果遇到的原子公式为真，则“验证者”获胜，“证伪者”失败，否则收益反转。否定 ~ 被不同地称为强否定、双重否定或博弈论否定。 [25]它的工作原理正如人们所期望的那样：当且仅当其否定 ∼ phi 在 M 中为假时， phi 为真（参见 Sandu 1993）。

3.3.基本属性和概念

二价失败。 IFL 和模型 M 中存在句子 phi，使得 phi 在 M 中既不是真也不是假。考虑在一个模型上评估句子 (∀x)(∃y/∀x)x=y，该模型的域正好有两个元素：a 和b.玩家 1 没有获胜策略。如果他选择 a 来解释 ∀x，他就会输掉玩家 2 选择 a 来解释 (∃y/∀x) 的游戏。同样，如果玩家1选择B，他将失去玩家2同样选择b的比赛。玩家2也没有获胜策略。她的策略功能（∃Y/∀X）是常数（零位置函数）。有两个这样的常数：a和b。无论这些策略函数播放器2都假设，播放器1击败它。如果玩家2选择A，则玩家1赢得了他选择B的比赛；如果播放器2应用B，则玩家1赢得了他选择a的比赛。 Game G（ϕ，M）尚未确定：这两个玩家都有获胜的策略。[26]非确定性的概念也可以扩展到公式：

（不确定性）在G IFF下，M在M中未确定的ϕ在G游戏G（ϕ，M，G）中没有赢家策略，也没有玩家2的胜利策略。

在IFL中，非真实性不会出现虚假性。也就是说，双重性在IFL中失败。但是，应该指出的是，由于对第三个真实价值或真实价值差距的假定，它不会失败（参见Hintikka 1991：20，55）。[27]相反，失败是整个语义理论（GTS）基本假设的结果。非确定性对应于结构性特性：在所考虑的模型中不存在某些函数的事实。

由于双重性的失败，排除中间的逻辑定律因双重否定而失败。实际上，ϕ在m iffm⊭（ϕ∨〜）中是未确定的。

逻辑等效性。如果句子ψ和IFL的χ在完全相同的模型中是真实的，而虚假性在完全相同的模型中是错误的，则它们是同等的。句子ψ和χ在逻辑上是等效的，如果它们既是真理等效又等同的句子。[28]由于双重性的失败，在IFL真相等价中，并不能保证逻辑等效性。

真理，虚假和独立迹象。 IFL的语法允许通用和存在量化符都被削减的公式，例如

ϕ：（∀X）（∃Y/∀X）（∀Z/∃Y）R（x，y，z）。

另一方面，在策略层面上实施了量词独立性。因此，当考虑一个公式的满意度（句子的真实）时，普遍量化器之后的独立指示是空置的。同样，当公式的不满（句子的虚假性）受到威胁时，生存量词之后的独立指示是空置的。句子ϕ在MIFF Player 2中是正确的，在Game G（ϕ，M）中具有获胜策略F = {C}。同样，这是指分别选择解释的任何元素A和B播放器1分别选择解释（∀x/∃Y），是（零位置）给出的（∃Y/∀X）的常数解释c ）策略函数C满足M（a，c，b）。 （分别是（∃Y/∀X）的恒定解释c在M中满足R（a，c，b）的恒定解释c，实际上，ϕ等同于包含不包含clash的通用量化词的句子：

ϕ在M iff中是正确的。

同样，ϕ是相当于包含不包含的存在量化词的句子的虚假性：ϕ是false m iff iff句子（∀x）（∃y）（∀z/∃y）r（x，y，z）是false其中。

3.4.如果一阶逻辑扩展

如果ϕ是fo的句子，则m if〜fif的模型是错误的，在m中，m iff ϕ在M中是不正确的。相比之下，在IFL虚假和非真实性中，ϕ是不正确的。可以引入IFL的扩展，可以在其中谈论句子的非真实性。为此，让我们引入一个新的否定符号。如果一阶逻辑（待表示为eIFL），则通过在操作�IFL的一组公式中获得扩展的公式（待表示）。

IFL的所有公式都是EIFL的公式。

如果ϕ和ψ是eifl的公式，则−d（ϕ∧ψ）和（ϕ∨ψ）也是如此。

因此，如果ϕ和ψ是IFL公式，例如找（−d）是EIFL公式；相比之下（∀X）¬ϕ并非。对于可能在量词范围内不出现的关键限制，请参见Hintikka（1991：49; 1996：148）。对于此限制的反例，请参见Hintikka（1996：148; 2002c），尤其是Hintikka（2006b），其中所谓的如果考虑一阶逻辑（FEIFL），则所谓的完全扩展。在FEIFL中，允许任何出现的发生，都遵循以下句法条件：如果（qx/w）是■发生的语法范围中的量词，则W中列出的所有量化词在w中列出的所有量词都同样在语法范围中发生的。

由矛盾的否定形成的EIFL公式的语义就是这样：

m，g⊨− ϕ iff m，g⊭ϕ。

从GTS的角度来看，结缔组织以不寻常的方式行事。对于IFL的所有连接器，都有一个游戏规则（可以看作是指定连接的含义）。对于矛盾的否定，没有游戏规则，并且没有用语义游戏的游戏来解释其语义。一个公式达式在全球范围内说，整个游戏G（ϕ，m，g）。如果ϕ是句子，则说m在m中是正确的，就是要说玩家2在游戏G（ϕ，m）中没有获胜策略。如果同样，确实存在G（ϕ，m）中的播放器2的获胜策略，则根据M中的规定是错误的。[31] [31]

不仅不是IFL的公式，而且通常也不能在IFL中表达它（请参阅第4.2节）。被排除的中间定律对矛盾的否定存在：对于所有句子ϕ和所有模型m，实际上是m⊨（ϕ∨前）。在第5节中，将看到Hintikka在讨论数学哲学中的问题时如何提议利用EIFL。

4。if一阶逻辑的金属特性

Hintikka和Sandu在几个出版物中讨论了IFL的金属特性。[32]在提出它们时，将参考存在于存在的二阶逻辑（ESO）； [33]进一步的重要概念是Skolemization和Skolem正常形式的IFL公式的概念。对于这些概念的确切定义，可以咨询补充文件。简而言之，通过在一阶公式中允许对关系和函数符号的存在量化来获得ESO。 IFL公式ϕ的Skolemization SK [ϕ]是较大词汇的一阶公式。它用函数符号来解释ϕ的存在量化符和分离符符号如何取决于前面的通用量词。例如，词汇{r}的ifl句子ϕ =（∀y）（∀ [ϕ] =（∀X）（∀Z）R（x，f（x），z，h（z））的词汇{r，f，h}。它的SkoLem正常形式再次是ESO句子SK [ϕ] =（∃F）（∃H）（∀X）（∀Z）R（x，f（x），x），z，h（z））。一阶句子SK [ϕ]不得与二阶句子SK [ϕ]混淆。

4.1.一阶逻辑和存在的二阶逻辑

游戏理论与FO的Tarskian语义。 FO的公式集是一组IFL公式的适当子集。 FO的标准语义不是GTS提供的语义，而是Tarskian语义，递归地指定了满意度关系m，g⊨ϕ。如果假定了选择的公理，则[34] FO的两个语义一致：

定理（假设AC）。 （Hodges 1983：94，Hintikka＆Kulas 1985：6-7）让τ为任何词汇，m nτ结构，g任何可变分配，以及任何fo [τ]公式。然后，M，G⊨ϕ在标准意义上具有IFF，在Game G（ϕ，M，G）中有一个胜利的策略。[35]

与ESO有关。 IFL和ESO是可以间隔的：[36]

定理（假设AC）ESO和IFL具有相同的表达能力。

也就是说，（1）对于每个IFL [τ]公式ϕ都有一个ESO [τ]公式ϕ'，使得对于所有τ结构M和可变分配G，我们都有：M，G⊨DASTIS：M，G⊨DASIFFm，g⊨fm，g⊨d ′。实际上，SK [ϕ]是合适的ESO公式。 （2）对于每个ESO [τ]公式ψ都有一个IFL [τ]公式ψ'，因此M，G⊨ψIffm，g⊨ψ'对于所有τ结构m和可变分配g。这是从以下事实转化为FPO的事实（Enderton 1970，Walkoe 1970），可以再次将其转化为IFL。

Hintikka认为，IFL实际上是一阶逻辑：实体的量化变量范围是个人，语义游戏玩家运作的所有实体也是如此。 （有关此想法的讨论，请参见第5.1节。）Interlatslatibalsible定理的一部分是一个事实：如果接受Hintikka的有争议的主张，这意味着ESO的表达能力实际上可以在第一个上实现 - 订单级别。