代数命题逻辑 algebraic propositional (Ramon Jansana)

首次发表于 2016 年 12 月 12 日星期一;实质性修订于 2022 年 5 月 20 日星期五。

乔治·布尔是第一个将逻辑以代数风格的数学理论形式呈现的人。在他的工作中,以及 19 世纪代数逻辑传统中的其他代数学家的工作中,仍然没有区分形式语言和数学严格语义的概念。这个传统中的代数学家所做的是建立代数理论(布尔代数和关系代数等)并在其中包含逻辑解释。

弗雷格和罗素的作品引入了一种不同的逻辑方法。在这些作品中,逻辑系统由形式语言和演绎演算组成,即一组公理和一组推理规则。让我们(在本条目中)将这样的一对称为逻辑演绎系统,而在演算中可推导出的公式称为其定理(现在在代数逻辑中,将这类演算称为希尔伯特式,在证明复杂性理论中称为弗雷格系统)。在弗雷格和罗素的方法中,对于所使用的形式语言,缺乏任何形式(数学)语义。唯一存在的语义是直观的、非正式的语义。

弗雷格和罗素引入的系统是经典逻辑系统,但很快其他逻辑学家开始考虑非经典逻辑系统。最早有影响力的引入与经典逻辑不同的逻辑的尝试仍然遵循弗雷格-罗素的传统,即提供一个没有任何形式语义的逻辑演绎系统。这些尝试导致了 C.I.刘易斯(1918 年,1932 年)提出的第一个模态系统,以及 Heyting(1930 年)对直觉主义逻辑的公理化。

Frege 和 Russell 逻辑推理系统设计的基本思想是,定理应该是与逻辑真理或逻辑有效性(直观上)相对应的公式。逻辑推论的概念并不是发展的核心,这也是沿着 C.I. Lewis 的第一个模态系统的脚步设计的许多非经典逻辑系统的情况。这种情况影响了一些非经典逻辑研究通常的呈现方式,有时也影响了其真正的发展。然而,逻辑推论的概念一直是逻辑传统上处理的概念。Tarski 再次将其置于现代逻辑的中心,无论是语义上还是句法上。如今,在上个世纪的不同逻辑的不同代数处理的基础上,围绕逻辑推论的概念形成了逻辑代数化的一般理论。

逻辑推论的概念对于这种一般理论的发展比定理和逻辑有效性的概念更加有成果。在建立逻辑代数化的一般理论的过程中,最早的尝试可以在 Rasiowa(1974)对蕴涵逻辑类的研究中找到,以及 Wójcicki(1988)对命题逻辑的一般性质的系统性介绍,这些研究主要由波兰逻辑学家进行,他们在 20 世纪上半叶跟随 Tarski、Lindenbaum、Łukasiewicz 等人的研究。

直到 20 世纪 20 年代,代数和逻辑矩阵(代数与一组指定元素的集合)才开始被视为逻辑推理系统的模型,即为逻辑形式语言提供形式语义学。此外,它们还被用来定义具有与已知逻辑推理系统的定理集相似属性的公式集,特别是具有替代实例封闭性的属性;不久之后,逻辑矩阵也被用来定义逻辑作为推理关系。

代数逻辑可以用非常一般的术语描述为通过将代数类、逻辑矩阵类和其他与代数相关的数学结构与逻辑相关联来研究逻辑的学科,并将逻辑可能具有的属性与相关代数(或代数相关结构)的属性相关联,以便通过理解这些代数来更好地理解所讨论的逻辑。

通过对特定逻辑的代数研究,上个世纪逐渐出现了关于逻辑代数化的一般理论,其目的是在过程中更或多或少明确地获得与逻辑可能具有的属性相关的代数类(或代数相关结构)的代数性质的一般且有信息量的结果。这些代数研究在某种程度上假设了将任何给定逻辑与一类代数关联为其自然代数对应物的过程的隐含概念。该一般理论的发展在 20 世纪 80 年代初加速并巩固,引入了可代数化逻辑的概念,此时也开始越来越明确地对于应该作为与给定逻辑关联的自然代数的类别进行假设。

在这个条目中,我们集中讨论将命题逻辑代数化作为推理关系的一般理论。这个理论已经发展成为被称为抽象代数逻辑(AAL)的领域。这个条目可以作为对这个领域的初步介绍。


1. 抽象的推论关系

塔斯基(Tarski)关于 20 世纪 20 年代和 30 年代演绎科学方法论的研究(1930a,1930b,1935,1936)在抽象上研究了公理化方法,并首次引入了抽象的推论操作概念。塔斯基主要考虑的是不同的数学公理化理论。在这些理论中,从公理中证明出来的句子是它们的推论,但(当然)几乎所有的推论都不是逻辑真理;在这些理论的适当形式化下,可以使用像弗雷格(Frege)或罗素(Russell)的逻辑演算来推导出公理的推论。塔斯基建立了一个框架来研究将一组公理分配给其推论的操作的最一般性质。

给定一个逻辑演绎系统 H 和一个任意的公式集合 X,如果存在一个有限的公式序列,其中任何一个公式属于 X 或是 H 的公理,或是由序列中前面的公式通过 H 的推理规则之一得到的,那么公式 a 在 H 中从 X 中可演绎出来。这样的序列是 H 中具有前提或假设 X 的 a 的演绎(或证明)。令 Cn(X)为从公式集合 X 中作为前提或假设在 H 中可演绎出来的公式集合。这个集合被称为 X 的推论集合(相对于逻辑演绎系统 H)。Cn 是一个将公式集合应用于获得新的公式集合的操作。它具有以下属性:对于每个公式集合 X,

  1. X⊆Cn(X)

  2. Cn(Cn(X))=Cn(X)

  3. Cn(X)=⋃{Cn(Y):Y⊆X,Y 有限}

第三个条件规定了 Cn(X)等于从 X 的有限子集可推导出的公式的并集。塔斯基将这些属性作为公理化定义了推论操作的概念。事实上,他补充说存在一个公式 x,使得 Cn({x})是所有公式的集合 A,并且这个集合必须是有限的或者与自然数集的基数相等。条件(3)暗示了更弱但重要的单调性条件。

  1. 如果 X⊆Y⊆A,则 Cn(X)⊆Cn(Y)。

为了包括文献中出现的逻辑系统的整个类别,需要比 Tarski 的定义稍微更一般的定义。我们将说,对于任意集合 A 上的抽象推论操作 C 是一个操作,它作用于 A 的子集并给出 A 的子集,并且对于所有的 X,Y⊆A 满足上述条件(1)、(2)和(4)。如果 C 还满足(3),我们称之为有限推论操作。

推论操作不仅存在于逻辑中,还存在于数学的许多领域。抽象推论操作在普遍代数和格论中被称为闭包算子。在拓扑学中,将拓扑空间的子集映射到其拓扑闭包的操作是一个闭包算子。实际上,集合 A 上的拓扑可以被认为是满足额外条件 C(∅)=∅ 和 C(X∪Y)=C(X)∪C(Y)的 A 上的闭包算子。

给定一个作用于集合 A 上的结果操作 C,A 的子集 X 被称为 C-闭合,或者是 C 的闭集,如果 C(X)=X。

一种不同但在数学上等价的(形式的)方法是考虑公式集合上的结果关系,而不是结果操作。对于形式语言的公式集合,一个(抽象的)结果关系 ⊢ 是一个在公式集合和公式之间的关系,满足以下条件:

  1. 如果 a∈X,则 X⊢a

  2. 如果 X⊢a 且 X⊆Y,则 Y⊢a。

  3. 如果 X⊢a 且对于每个 b∈X,Y⊢b,则 Y⊢a。

如果此外它满足有限性,则

  1. 如果 X⊢a,则存在一个有限集合 Y⊆X,使得 Y⊢a。

给定一个逻辑演绎系统 H,如果在 H 中从 X 推导出 a,则定义的关系 ⊢(根据我们已经看到的)是一个有限的推论关系。然而,我们不仅习惯于根据句法定义推论关系,还习惯于根据语义定义推论关系。例如,我们使用真值赋值定义经典命题推论,使用结构定义一阶命题推论,使用 Kripke 模型定义直觉主义命题推论等。有时,这些模型论定义的推论关系定义了非有限的推论关系,例如,无穷形式语言的推论关系和所谓标准语义的二阶逻辑的推论关系。

一般来说,对于集合 A(不一定是某个形式语言的公式集合),抽象的推论关系是 A 的子集与 A 元素之间的关系 ⊢,满足上述条件(1)-(3)。如果还满足条件(4),则称其为有限的。如果 ⊢ 是一个抽象的推论关系,并且 X⊢a,则我们可以说 X 是前提或假设的集合,a 是根据 ⊢ 的结论,a 是由 X 推出的,或者根据 ⊢ 是 X 所蕴含的。抽象的推论关系对应于 Koslow 的蕴涵结构;参见 Koslow 1992,该作者引入了与逻辑(广义上)相关但不同的推论关系的方法。

集合 A 上的结果操作与 A 上的抽象结果关系一一对应。从结果操作 C 到结果关系 ⊢C 的转换,以及从结果关系 ⊢ 到结果操作 C⊢ 的转换是简单的,并且由定义给出:

X⊢Ca 当且仅当 a∈C(X)且 a∈C⊢(X)当且仅当 X⊢a。

此外,如果 C 是有限的,则 ⊢C 也是有限的;如果 ⊢ 是有限的,则 C⊢ 也是有限的。

对于逻辑蕴涵的一般讨论,请参见《逻辑蕴涵》条目。

2. 作为蕴涵关系的逻辑

在本节中,我们定义了命题逻辑是什么,并解释了与之相关的基本概念。我们将在下文中简称命题逻辑(如下所定义)为逻辑系统。

逻辑学中研究的推论关系的主要特征之一是它们的形式特征。这大致意味着,如果一个句子 a 从一组句子 X 中推出,并且我们有另一个句子 b 和另一组与 a 和 X 分别具有相同形式的句子 Y,那么 b 也从 Y 中推出。在命题逻辑中,这归结为说,如果我们统一地用其他句子替换 X∪{a}中句子的基本子句,得到 Y 和 b,那么 b 从 Y 中推出。(读者可以在“逻辑推论”条目中找到有关形式性概念的更多信息。)

要将逻辑学的形式特征的概念转化为严格的定义,我们需要引入命题语言的概念和替换的概念。

命题语言(简称语言)L 是一组联结词,即一组符号,每个符号的 arity n 告诉我们,如果 n=0,则该符号是一个命题常量;如果 n>0,则该联结词是一元的、二元的、三元的等等。例如{∧,∨,→,⊥,⊤}是(或可以是)几种逻辑的语言,如经典逻辑和直觉主义逻辑(⊥ 和 ⊤ 是 0 元的,其他联结词是二元的);{¬,∧,∨→,□,◊}是几种模态逻辑的语言(¬,□,◊ 是一元的,其他联结词是二元的);{∧,∨,→,∗,⊤,⊥,1,0}是多值逻辑和线性逻辑片段的语言(⊥,⊤,1 和 0 是命题常量,其他符号是二元联结词)。

给定一个语言 L 和一组命题变量 V(与 L 不相交),L 的公式或 L-公式的定义如下:

  1. 每个变量都是一个公式。

  2. 每个 0 元符号都是一个公式。

  3. 如果 ∗ 是一个联结词,n>0 是它的元数,则对于所有的公式 ϕ1,…,ϕn,∗ϕ1…ϕn 也是一个公式。

对于 L 的一个替换 σ 是一个从变量集合 V 到 L 的公式集合的映射。它告诉我们在进行替换时,哪个公式必须替换哪个变量。如果 p 是一个变量,则 σ(p)表示替换 σ 分配给 p 的公式。将替换 σ 应用于公式 ϕ 的结果是从 ϕ 中同时替换变量 p1,…,pk 为相应的公式 σ(p1),…,σ(pk)得到的公式 σ(ϕ)。通过这种方式,替换 σ 给出了一个满足以下条件的从公式集合到自身的唯一映射 σ:

  1. 对于每个变量 p,σ(p)=σ(p)。

  2. σ(†)=†,对于每个 0 元连词†,

  3. σ(∗ϕ1…ϕn)=∗σ(ϕ1)…σ(ϕn),对于每个元数为 n>0 的连词 ∗ 和公式 ϕ1,…,ϕn。

如果存在一个替换 σ,使得将其应用于 ϕ 得到 ψ,则公式 ψ 是公式 ϕ 的替换实例,即如果 σ(ϕ)=ψ。

为了避免不必要的复杂性,我们在接下来的讨论中假设所有逻辑都使用同一个可数集合 V 的变量,以便 L 的公式定义仅依赖于 L。逻辑系统(或简称逻辑)由语言 L 和在 L 的公式集上的蕴涵关系 ⊢ 给出,该关系在形式上对于每个替换 σ、每个公式集 Γ 和每个公式 ϕ 都成立,

如果 Γ⊢ϕ,则 σ [Γ] ⊢σ(ϕ)

其中 σ [Γ] 是通过将替换 σ 应用于 Γ 中的公式而获得的公式集。满足这一性质的语言的公式集上的蕴涵关系被称为结构性的,也被文献中称为替换不变。它们首次在 Łoś 和 Suszko 的 1958 年的论文中被考虑。Tarski 只明确考虑了对于某些蕴涵关系,闭合集合也闭合于替换实例;他从未(至少明确地)考虑过蕴涵关系的替换不变条件。

我们将逻辑系统称为字母 L,并可能带有下标,我们设定 L=⟨L,⊢L⟩ 和 Ln=⟨Ln,⊢Ln⟩,并理解 L(Ln)是 L(Ln)的语言,⊢L(⊢Ln)是其推论关系。如果 ⊢L 是有限推论关系,则逻辑系统 L 是有限的。

逻辑系统的推论关系可以通过多种方式给出,有些使用证明论工具,其他使用语义手段。可以使用类似希尔伯特样式公理系统、根式演算或自然演绎样式演算等证明系统来定义一个替换不变的推论关系。也可以使用数学对象类(代数、克里普克模型、拓扑模型等)和满足关系来语义地定义一个替换不变的推论关系。

如果 L1=⟨L,⊢L1⟩ 是一个通过证明系统定义 ⊢L1 的逻辑系统,而 L2=⟨L,⊢L2⟩ 是同一语言上通过语义定义 ⊢L2 的逻辑系统,我们称用于定义 ⊢L1 的证明系统对于定义 ⊢L2 的语义是完备的,如果 ⊢L1 包含在 ⊢L2 中,即如果 Γ⊢L1ϕ 蕴含 Γ⊢L2ϕ。如果另一个包含成立,则称证明系统相对于定义 ⊢L2 的语义是完全的,即当 Γ⊢L2ϕ 蕴含 Γ⊢L1ϕ 时。

一个 L 逻辑系统的理论 Γ 被称为逻辑系统 L 的理论,或者 L-理论,如果它在关系 ⊢L 下是封闭的,也就是说,每当 Γ⊢Lϕ 时,ϕ∈Γ 也成立。换句话说,L 的理论是 L-公式集合上的随附操作 C⊢L 的闭集。为了简化符号,我们用 CL 来表示这个随附操作。如果 ∅⊢Lϕ,则 ϕ 是 L 的定理(或有效性)。然后 CL(∅)是 L 的定理集合,也是 L 的最小理论。L 的所有理论集合将用 Th(L)表示。

给定一个逻辑系统 L,随附操作 CL 是替换不变的,这意味着对于每个 L-公式集合 Γ 和每个替换 σ,σ [CL(Γ)] ⊆CL(σ [Γ])。此外,对于 L 的每个理论 T,我们有一个新的随附操作 CTL 定义如下:CTL(Γ)=CL(T∪Γ),即 CTL(Γ)是根据 L 从 Γ 和 T 推导出的公式集合。事实证明,当且仅当 T 在替换下是封闭的时,CTL 是替换不变的。

如果 L 是一个逻辑系统,Γ,Δ 是 L-公式集合,我们将使用符号 Γ⊢LΔ 来说明对于每个 ψ∈Δ,Γ⊢Lψ。因此,当且仅当 Δ⊆CL(Γ)时,Γ⊢LΔ。

如果 L=⟨L,⊢L⟩ 和 L′=⟨L′,⊢L′⟩ 是逻辑系统,其语言满足 L′⊆L(因此所有 L′-公式都是 L-公式),且对于每个 L′-公式 Γ 和每个 L′-公式 ϕ,当且仅当 Γ⊢L′ϕ 时,Γ⊢Lϕ,我们称 L′是 L 的一个片段(实际上是 L′的片段),而 L 是 L′的扩展。

3. 一些逻辑的例子

我们在本文中提供了一些逻辑系统的例子,以方便读者参考。在可能的情况下,我们会提到相应的条目。

我们使用标准约定,用(ϕ∗ψ)代替 ∗ϕψ 表示二元连接词,并在公式中省略外部括号。

3.1 经典命题逻辑

我们将经典命题逻辑 CPL 的语言定义为集合 Lc={∧,∨,→,⊤,⊥},其中 ∧,∨,→是二元连接词,⊤,⊥ 是命题常量。我们假设推论关系由通常的真值表方法定义(⊤ 被解释为真,⊥ 被解释为假),如下所示,

Γ⊢CPLϕ 当且仅当为 Γ 中的每个 ψ 分配 true 的真值赋值将 true 分配给 ϕ。

∅⊢CPLϕ 的公式是永真式。请注意,使用语言 Lc,公式 ϕ 的否定定义为 ϕ→⊥。有关更多信息,请参阅关于经典逻辑的条目。

3.2 直觉主义命题逻辑

我们将直觉命题逻辑的语言视为与经典命题逻辑相同,即集合{∧,∨,→,⊤,⊥}。随附关系由以下希尔伯特风格的演算定义。

公理

所有形式为的公式

C0.

C1.

ϕ→(ψ→ϕ)

C2.

ϕ→(ψ→(ϕ∧ψ))

C3.

(ϕ∧ψ)→ϕ

C4.

(ϕ∧ψ)→ψ

C5.

ϕ→(ϕ∨ψ)

C6.

ψ→(ϕ∨ψ)

C7.

(ϕ∨ψ)→((ϕ→δ)→((ψ→δ)→δ))

C8.

(ϕ→ψ)→((ϕ→(ψ→δ))→(ϕ→δ))

C9.

⊥→ϕ

推理规则

(假言推理)ϕ,ϕ→ψ/ψ

有关直觉逻辑的条目,请参阅更多信息。

3.3 本地正常模态逻辑

我们在这里考虑的模态逻辑语言是通过添加一元连接词 □ 来扩展 Lc 的集合 Lm={∧,∨,→,¬,□,⊤,⊥}。在模态逻辑的标准文献中,一个正常的模态逻辑被定义为一组具有特定属性的公式,而不是一个推理关系。一个正常的模态逻辑是 Lm 的公式集 Λ,其中包含了经典逻辑语言的所有重言式,形式为 □(ϕ→ψ)→(□ϕ→□ψ)的公式,并且在以下规则下封闭:

(Modus Ponens)(Modal Generalization)(Substitution)ϕ,ϕ→ψ/ψϕ/□ϕϕ/σ(ϕ),对于每个替换 σ

注意,集合 Λ 在替换实例下是封闭的,即对于每个替换 σ,如果 ϕ∈Lm,则 σ(ϕ)∈Lm。

最小的正常模态逻辑称为 K,并且可以通过希尔伯特风格的演算公理化,其中包括经典逻辑的重言式和公式 □(ϕ→ψ)→(□ϕ→□ψ),以及推理规则 Modus Ponens 和模态概括。请注意,由于我们在公理的呈现中使用了模式,可推导公式的集合在替换规则下是封闭的。

对于一个正常的模态逻辑 Λ,与之相关联的是由 Λ 中的所有公式作为公理,以及唯一的推理规则 Modus Ponens 所定义的推理关系。由此推理关系给出的逻辑系统称为 Λ 的局部推理。我们用 lΛ 表示它。它的定理是 Λ 的元素,并且满足以下条件:

Γ⊢lΛϕ 当且仅当 ϕ∈Λ,或者存在 ϕ1,…,ϕn∈Γ,使得(ϕ1∧…∧ϕn)→ϕ∈Λ。

3.4 全局正常模态逻辑

另一个自然与每个正常模态逻辑 Λ 相关联的推论关系,由 Λ 的公式和推理规则 Modus Ponens 和 Modal Generalization 定义的演算。由此推论关系给出的逻辑系统称为 Λ 的全局推论,用 gΛ 表示。它具有与局部 lΛ 相同的定理,即 Λ 的元素。lΛ 和 gΛ 之间的区别在于它们允许从非空前提集中得出的推论。例如,我们有 p⊢gK□p,但 p⊬lK□p。这种差异对它们的代数行为产生了巨大影响。

有关模态逻辑的更多信息,请参阅模态逻辑条目。读者可以在 Kracht 2006 中找到有关模态逻辑作为推论关系的具体信息。

3.5 没有指数的直觉线性逻辑

我们将没有指数的直觉线性逻辑的语言定义为集合 {∧,∨,→,∗,0,1,⊤,⊥},其中 ∧,∨,→,∗ 是二元连接词,而 0,1,⊤,⊥ 是命题常量。我们用 ILL 表示这个逻辑。下面的公理和推理规则提供了这个逻辑的希尔伯特样式公理化。

公理

L1.

1

L2.

(ϕ→ψ)→((ψ→δ)→(ϕ→δ))

L3.

(ϕ→(ψ→δ))→(ψ→(ϕ→δ))

L4.

ϕ→(ψ→(ϕ∗ψ))

L5.

(ϕ→(ψ→δ))→((ϕ∗ψ)→δ)

L6.

1→(ϕ→ϕ)

L7.

(ϕ∧ψ)→ϕ

逻辑 8.

(ϕ∧ψ)→ψ

L9.

ψ→(ϕ∨ψ)

L10.

ϕ→(ϕ∨ψ)

L11.

((ϕ→ψ)∧(ϕ→δ))→(ϕ→(ψ∧δ))

L12.

((ϕ→δ)∧(ψ→δ))→((ϕ∨ψ)→δ)

L13.

ϕ→⊤

L14.

⊥→ψ

推理规则

(假言推理)(附加)ϕ,ϕ→ψ/ψϕ,ψ/ϕ∧ψ

0 元连接词 0 用于通过 ¬ϕ:=ϕ→0 来定义否定。没有特定的公理模式涉及 0。

有关更多信息,请参阅关于线性逻辑的条目。

3.6 关于相关逻辑系统 R

我们考虑的语言是集合{∧,∨,→,¬},其中 ∧,∨,→是二元连接词,而 ¬ 是一元连接词。可以通过直觉线性逻辑的规则(不包括指数)和该逻辑的公理 L2、L3、L7-L12 以及随附性公理来给出 R 的希尔伯特样式公理化。

  1. (ϕ→(ϕ→ψ))→(ϕ→ψ)

  2. (ϕ→¬ψ)→(ψ→¬ψ)

  3. (ϕ∧(ψ∨δ))→((ϕ∧ψ)∨ϕ∧δ))

  4. ¬¬ϕ→ϕ

有关更多信息,请参阅关于相关逻辑的条目。

4. 代数

特定逻辑的代数研究首先必须提供其形式语言及其代数语义,使用一类代数来理解该逻辑的性质。在本节中,我们介绍了命题逻辑的形式语言如何得到代数解释。在下一节中,我们将讨论逻辑系统的代数语义是什么。

我们首先描述了命题逻辑代数研究中涉及的前两个步骤。为了赋予命题语言代数解释,这两个步骤都是必需的。为了阐述它们,我们将假设读者已经了解一阶逻辑(参见经典逻辑和一阶模型论的条目),并将称之为代数一阶语言,或简称为代数语言,具有相等性而没有任何关系符号,因此这些语言只有操作符号(也称为函数符号),如果有的话,位于其非逻辑符号集合中。

我们即将阐述的这两个步骤可以概括为一个口号:

命题公式是术语。

第一步是将任何命题语言 L 的公式视为具有 L 作为其操作符集的代数一阶语言的术语。这意味着(i)L 的每个 n 元连词被视为具有 n 元的操作符(因此 L 的每个 0 元符号被视为个体常量),以及(ii)L 的命题公式被视为这个一阶语言的术语;特别是命题变量是一阶语言的变量。从这个角度来看,L-公式的定义与 L-术语的定义完全相同。我们将称具有 L 作为其操作符集的代数语言为 L-代数语言。

第二步是以与一阶语言的术语在结构中的解释方式相同的方式解释命题公式。这样,L-代数的概念就发挥作用了。在给定的集合 A 上,n 元连词由 A 上的 n 元函数解释(一种将 A 的元素分配给每个序列 ⟨a1,…,an⟩ 的映射)。这个过程是逻辑系统(如经典逻辑和 Łukasiewicz 和 Post 的有限值逻辑)的真值表解释的一般化。在这些情况下,给定参与的真值集合,解释连词的函数由其真值表给出。

引入代数的一种方法是将其作为某种代数一阶语言的模型。我们遵循一个等价的路径,并使用命题语言的设置来给出代数的定义。设 L 是一个命题语言。L 型代数,或简称为 L-代数,是一个集合 A,称为 A 的载体或宇宙,以及对于 L 中的每个联结词 ∗,具有 ∗ 的元数的函数 ∗A(如果 ∗ 是 0 元的,则 ∗A 是 A 的一个元素)。如果代数 A 的载体是一个单元素集,则代数 A 是平凡的。

L-代数 A 上的赋值是一个从变量集合到其载体 A 的映射 v。代数与赋值一起被用来以组合的方式解释 L 的公式,假设 L 的联结词 ∗ 在 L-代数 A 中由函数 ∗A 解释。设 A 是 L 型代数,v 是 A 上的一个赋值。复合公式 ∗ϕ1…ϕn 的值通过将解释 ∗ 在 A 中的函数 ∗A 应用于先前计算的公式 ϕ1,…,ϕn 的值 v(ϕ1),…,v(ϕn)来计算。准确地说,公式 ϕ 的值 v(ϕ)按如下递归方式定义:

  1. 对于每个变量 p,v(p)=v(p),

  2. v(†)=†A,如果†是一个 0 元连接词

  3. v(∗ϕ1…ϕn)=∗A(v(ϕ1),…,v(ϕn)),如果 ∗ 是一个 n 元(n>0)连接词。

注意,通过这种方式,我们得到了一个从 L-公式集合到 A 的载体的映射 v。值得注意的是,在估值下,公式的值仅取决于实际出现在公式中的命题变量。因此,如果 ϕ 是一个公式,我们使用符号 ϕ(p1,…,pn)来表示出现在 ϕ 中的变量在列表 p1,…,pn 中,对于代数 A 的给定元素 a1,…,an,我们用 ϕA [a1,…,an] 来指代在任何对 A 上的估值 v 下,使得 v(p1)=a1,…,v(pn)=an 时 ϕ(p1,…,pn)的值。

代数逻辑研究的第三个基本步骤是将语言 L 的公式集转化为一个代数,即 L 的公式代数,记为 FmL。这个代数的载体是 L 的公式集,操作定义如下。对于每个 n 元连词 ∗(其中 n>0),函数 ∗FmL 是将每个公式元组(ϕ1,…,ϕn)(其中 n 是 ∗ 的元数)映射到公式 ∗ϕ1…ϕn 的映射,对于每个 0 元连词†,†FmL 是†。如果不会引起混淆,我们省略 FmL 中的下标,并写成 Fm。

4.1 通用代数和模型论的一些概念

代数是一种特殊类型的结构或模型。L-代数是 L-代数一阶语言的结构或模型。因此,一阶语言的模型论概念适用于它们(参见关于经典逻辑和一阶模型论的条目)。我们需要一些这些概念。它们也被用于通用代数,通用代数在某种程度上可以被认为是代数语言的模型论。我们介绍我们需要的概念的定义。

给定类型为 L 的代数 A,A 的一个同余关系是指满足以下兼容性属性的 A 上的等价关系 θ:对于每个 n 元连结符 ∗∈L,对于每个 a1,…,an,b1,…,bn∈A,

如果 a1θb1,…,anθb1,则 ∗A(a1,…,an)θ∗A(b1,…,bn)。

给定 A 的一个同余关系 θ,我们可以通过将被 θ 关联的元素进行等同来缩减代数。所得到的代数是 A 模 θ 的商代数。它用 A/θ 表示,其载体是由 A 中元素 a 的 θ 等价类 [a] 组成的集合 A/θ,操作定义如下:

  1. †A/θ=[†A],对于每个 0 元连词†,

  2. ∗A/θ([a1],…,[an])=[∗A(a1,…,an)],对于每个元数为 n 且 n>0 的连词 ∗。

兼容性属性确保了定义的准确性。

设 A 和 B 为 L-代数。从 A 到 B 的同态 h 是一个从 A 到 B 的映射,满足对于每个 0 元符号†∈L 和每个 n 元连词 ∗∈L

  1. h(†A)=†B

  2. h(∗A(a1,…,an))=∗B(h(b1),…,h(bn)),对于所有的 a1,…,an∈A。

如果存在从 A 到 B 的同态映射,该映射是从 A 到 B 的一个满射,则我们说 B 是 A 的同态像。从 A 到 B 的同态映射是一个同构映射,如果它是从 A 到 B 的一个一对一和满射映射。如果存在从 A 到 B 的同构映射,我们说 A 和 B 是同构的,并且 B 是 A 的同构像(或副本)。

设 A 和 B 为 L-代数。如果满足以下条件,A 是 B 的子代数:(1)A⊆B,(2)B 中 L 的零元符号的解释属于 A,并且 A 在 B 中解释非零元符号的函数下是封闭的,(3)A 中零元符号的解释与 B 中的解释相同,并且 L 中其他符号在 A 上的解释是它们在 B 中解释的限制。

关于一阶模型论的直积(在那里称为乘积)和超积的概念,请参阅有关一阶模型论的条目。

4.2 类别和准类别

提供命题逻辑语义的大多数代数类别都是准类别,而在大多数情况下是类别。类别和准类别理论是普遍代数的主要研究课题之一。

L-代数的等式类是一种可以通过非常简单的方式(通过等式)在 L-代数语言中定义的 L-代数类。L-等式是一个公式 ϕ≈ψ,其中 ϕ 和 ψ 是 L-代数语言的项(如果我们从命题逻辑的角度来看,则是 L-公式),'≈'是等式的形式符号(始终解释为恒等关系)。如果对于代数 A 的每个赋值 v,v(ϕ)=v(ψ),则等式 ϕ≈ψ 在代数 A 中成立,或者说 A 是 ϕ≈ψ 的模型。这与说 ϕ≈ψ 的全称闭包是根据带有等式的一阶逻辑的通常语义在 A 中为真的句子完全相同。L-代数的等式类是一类 L-代数,它是给定的一组 L-等式的所有模型的类别。

一个 L-代数的准等式类是使用 L-代数语言定义的一种类,比等式类稍微复杂一些。一个合适的 L-准等式是形如 ⋀i≤nϕi≈ψi→ϕ≈ψ 的公式。一个 L-准等式是上述形式的公式,但可能具有空的前提,此时它只是等式 ϕ≈ψ。因此,L-准等式包括合适的 L-准等式和 L-等式。如果一个 L-准等式在 L-代数 A 中成立,或者说该代数是它的模型,那么准等式的全称闭包在 A 中是真的。一个 L-代数的准等式类是一类代数,它是给定的一组 L-准等式的模型类。由于等式也是准等式,所以每个等式类都是准等式类。反之不成立。此外,由于在平凡代数中,适当的代数语言的所有等式和准等式都是成立的,所以等式类和准等式类都是非空的。

代数的等式类和准等式类可以通过它们所具有的闭包性质来表征。一个非空的 L-代数类是一个变种,如果它在子代数、直积和同态像下是封闭的。如果它在子代数、直积、超积、同构像下是封闭的,并且包含一个平凡代数,那么它是一个准变种。很容易看出,等式类是变种,而准等式类是准变种。Birkhoff 定理指出,所有的变种都是等式类,而 Malcev 定理指出,所有的准变种都是准等式类。

由非空类 K 的 L-代数生成的多样性是包括 K 并且在子代数、直积和同态像下封闭的最小的 L-代数类。它也是满足 K 中方程的模型的代数类。例如,由经典逻辑的两个真值代数生成的多样性是布尔代数类。如果我们将该代数限制为仅包括合取和析取操作,它将生成分配格的多样性;如果我们将其限制为仅包括合取和析取操作以及 ⊤ 和 ⊥ 的解释,它将生成有界分配格的多样性。

由类 K 的 L-代数生成的准多样性是包括 K、平凡代数并且在子代数、直积、超积和同构像下封闭的最小的 L-代数类。

L-代数的 SP 类是包含平凡代数并且在同构像、子代数和直积下封闭的 L-代数类。因此,准多样性和多样性都是 SP 类。由类 K 的 L-代数生成的 SP 类是包括 K、平凡代数并且在子代数、直积和同构像下封闭的最小的 L-代数类。

5. 代数语义学

“代数语义学”这个术语在文献中一直以来都被宽泛地使用着。为了给一个逻辑提供一个代数语义,就是要在一类代数中解释它的语言,为一个公式(在一个估值下)在这类代数中定义一个满足的概念,并且通常为逻辑的定理证明一个完备性和一致性定理。如今,对于逻辑系统有一个精确的代数语义概念。它是由 Blok 和 Pigozzi 在 Blok&Pigozzi 1989 年引入的。在这个概念中,我们以数学上精确的术语陈述了在文献中发现的特定逻辑系统的众多所谓代数语义的共同之处。我们在本节中介绍这个概念。为了激发定义的动机,我们首先讨论了几个例子,强调它们共享的相关属性。读者不需要了解在例子中我们所提到的提供代数语义的代数类。重要的是它的存在。

命题逻辑的代数语义的原型例子是布尔代数类 BA,它是经典逻辑的代数语义,以及 Heyting 代数类 HA,它是直觉主义逻辑的代数语义。每个布尔代数和每个 Heyting 代数 A 都有一个根据它们的自然顺序确定的最大元素;这个元素通常用 1A 表示,并解释命题常量符号 ⊤。它被视为给出代数语义的特殊元素。这两个逻辑的代数语义工作方式如下:

令 L 为经典或直觉逻辑,令 K(L)为相应的布尔代数或哈斯廷代数的类。有以下关系成立:

Γ⊢Lϕ 当且仅当对于每个 A∈K(L)和每个在 A 上的赋值 v,如果对于所有的 ψ∈Γ,v(ψ)=1A,则 v(ϕ)=1A。

这是 BA 和 HA 分别作为经典逻辑和直觉逻辑的代数语义的确切内容。上述表达式中从左到右的蕴含是一个代数的声音定理,而从右到左的蕴含是一个代数的完备性定理。

有一些逻辑学,其代数语义在文献中以与上述模式稍有不同的方式提供。让我们考虑《无指数直觉线性逻辑》第 3.5 节中的示例。我们用 IL0 表示在 Troelstra 1992 中定义的带零的 IL-代数类(但适应了 ILL 的语言)。每个 A∈IL0 都是一个带有额外操作的格,因此具有其格序 ≤A。这个格序有一个最大元素,我们将其作为 ⊤ 的解释。在这些代数 A 中的每一个上,都有一个指定元素 1A(常量 1 的解释),它可能与最大元素不同。它成立:

Γ⊢ILLϕ 当且仅当 对于每个 A∈IL0 和每个在 A 上的赋值 v,如果对于所有的 ψ∈Γ,都有 1A≤Av(ψ),那么 1A≤Av(ϕ)。

在这种情况下,人们不仅考虑每个代数 A 中的一个指定元素,而是一组指定元素,即大于或等于 1A 的元素,以提供定义。让我们用 D(A) 表示这个集合,并注意到 D(A)={a∈A:1A∧Aa=1A}。因此,

Γ⊢ILLϕ 当且仅当对于每个 A∈IL0,如果 v [Γ] ⊆D(A),则 v(ϕ)∈D(A)。

仍然存在更复杂的情况。其中之一是关联逻辑系统 R。考虑在 Font&Rodríguez 1990 中定义的代数类 Ral(也参见 Font&Rodríguez 1994),并在那里用'R'表示。对于每个 A∈Ral,我们考虑集合 E(A):{a∈A:a∧A(a→Aa)=a→Aa}。然后 Ral 被称为 R 的代数语义,因为以下条件成立:

Γ⊢Rϕ 当且仅当对于每个 A∈Ral 和每个在 A 上的估值 v,如果 v [Γ] ⊆E(A),则 v(ϕ)∈E(A)。

上述示例中的共同模式是,代数语义由

  1. 一类代数 K 给出,

  2. 在 K 中的每个代数中,有一组指定元素扮演着 1A 在经典逻辑和直觉逻辑中的角色(更准确地说是集合{1A}的角色),

  3. 这组指定元素可以通过方程式来定义(在每个代数上以相同的方式),因为它是代数中满足方程式(即其解)的元素的集合。对于 BA 和 HA,方程式是 p≈⊤。对于 Ral,方程式是 p→(p∧p)≈p→p,对于 IL0,方程式是 1∧p≈1。

Blok 和 Pigozzi 关于代数语义的主要观点来自于上述(3)中提到的认识,即在已知逻辑的代数语义中考虑的指定元素集实际上是一个方程的解集,而当研究人员试图为新的逻辑获得代数语义时,实际上是在以等式的方式在每个代数中统一定义一组指定元素,以获得代数的完备性和一致性定理,尽管这些术语并没有明确地表述。

现在我们可以阐述代数语义的数学精确概念了。为了发展一个富有成果和普遍性的逻辑代数化理论,需要进行一些超越已知具体例子的概括。在代数语义的定义中,我们将从单个方程转向一组方程,在指定元素的可定义性条件中。

在陈述 Blok 和 Pigozzi 的定义之前,我们需要引入一种符号约定。给定一个代数 A 和一个包含一个变量的方程集 Eq,我们用 Eq(A)表示满足 Eq 中所有方程的 A 的元素集合。然后,如果存在一个代数类 K 和一个包含一个变量的方程集 Eq,使得对于每个 A∈K 和每个在 A 上的赋值 v,如果 v [Γ] ⊆Eq(A),则 Γ⊢Lϕ 当且仅当 v(ϕ)∈Eq(A),则逻辑 L 被称为具有代数语义。在这种情况下,我们说代数类 K 是 L 的 Eq-代数语义,或者(K,Eq)是 L 的代数语义。如果 Eq 由一个单一的方程 δ(p)≈ε(p)组成,我们将简单地说 K 是 δ(p)≈ε(p)-代数语义。事实上,Blok 和 Pigozzi 在他们的代数语义定义中要求 Eq 应该是有限的。但更一般地说是更好的。该定义明确包括了例子中遇到的情况。

(**)

Γ⊢Lϕ iff for every A∈K and every valuation v on A, if v [Γ] ⊆Eq(A), then v(ϕ)∈Eq(A).

In this situation we say that the class of algebras K is an Eq-algebraic semantics for L, or that the pair (K,Eq) is an algebraic semantics for L. If Eq consists of a single equation δ(p)≈ε(p) we will simply say that K is a δ(p)≈ε(p)-algebraic semantics for L. In fact, Blok and Pigozzi required that Eq should be finite in their definition of algebraic semantics. But it is better to be more general. The definition clearly encompasses the situations encountered in the examples.

如果 K 是 L 的一个有限逻辑 Eq-代数语义的 Eq-代数语义,并且 Eq 是有限的,那么由 K 生成的拟变种也是一个 Eq-代数语义。如果我们考虑生成的变种,一般情况下不成立。因此,在发展有限逻辑代数化理论时,习惯上将代数的语义类视为生成它们的任意子类的代数语义,而不是任意子类。相反,如果一个拟变种是一个有限 L 的 Eq-代数语义,并且 Eq 是有限的,那么生成它的任何子类也是 Eq-代数语义。

在最好的情况下,逻辑的典型代数语义是一个变种,例如上面讨论的所有例子。但也有一些情况不是这样的(参见 Blok&Pigozzi 1989)。

一个拟变种可以是一个逻辑的 Eq-代数语义,也可以是另一个逻辑的 Eq'-代数语义(其中 Eq 和 Eq'不同)。例如,由于 Glivenko 的定理(参见直觉逻辑条目),Heyting 代数类是经典逻辑的{¬¬p≈1}-代数语义,也是直觉逻辑的标准{p≈1}-代数语义。此外,不同的代数拟变种可以是同一逻辑的 Eq-代数语义。已知存在一个拟变种,它包含了布尔代数的变种,同时也是经典命题逻辑的{p≈1}-代数语义。还已知对于某些具有代数语义(相对于某个方程集)的逻辑,与逻辑对应的自然代数类不是它的代数语义(对于任何方程集)。一个满足这种情况的例子是局部正常模态逻辑 lK。最后,有些逻辑没有任何代数语义。

这些事实突显了对一对(K,Eq)的好的标准的需求,以在某些情况下为逻辑 L 提供自然的代数语义。其中一个标准是 L 是一个具有(K,Eq)作为代数语义的可代数逻辑。另一个标准是 K 是与逻辑 L 相关的自然代数类。关于逻辑系统的自然代数类的概念将在第 8 节中讨论,而关于可代数逻辑的概念将在第 9 节中讨论。

有兴趣的读者可以参考 Blok&Rebagliato 2003 年的研究,该研究致力于逻辑的代数语义,以及 Moraschini 即将发表的关于该主题的最新结果(在本文中,证明了局部正常模态逻辑 lK 的自然代数类,即模态代数类,不是它的代数语义(对于任何一组方程))。

存在一种特殊且重要的逻辑类型,具有代数语义,包括经典逻辑和直觉逻辑。这就是所谓的断言逻辑类。

令 K 为具有常数项的代数语言中的代数类,即一个公式 ϕ(p1,…,pn),对于每个代数 A∈K 和元素 a1,…,an,b1,…,bn∈A,有 ϕA [a1,…,an]=ϕA [b1,…,bn],也就是说,在 K 中的每个代数中,无论我们如何解释 ϕ 中的变量在 A 上,ϕ 都取相同的值。我们用 ϕA 表示这个值。因此,ϕ 在 K 中的代数中作为一个常数(相对于 K 中的代数),ϕA(对于 A∈K)可以被看作是一个指定的元素。

给定一个具有常数项 ϕ 的代数语言中的代数类 K,(K,ϕ)的断言逻辑 LϕK 定义如下:

对于每个 A∈K(L)和每个在 A 上的赋值 v,如果对于所有的 ψ∈Γ,v(ψ)=ϕA,则 Γ⊢LϕKϕ,则 v(ϕ)=ϕA。

当存在一个代数语言 L 的代数类 K 和一个常数项 ϕ 使得 L = LϕK 时,逻辑系统 L 是 assertional 的。

最近对 assertional 逻辑的研究是由 Albuquerque 等人在 2018 年进行的。我们将读者引向这篇论文,在后面的章节中,我们介绍了 Leibniz 和 Frege 逻辑系统中 assertional 逻辑的分类,并讨论了一些例子。

6. 逻辑矩阵

在上一节中,我们看到为了为逻辑提供代数语义,在许多情况下需要在每个代数中考虑一组指定元素,而不是单个指定元素。在我们讨论的例子中,指定元素的集合可以通过一个方程在代数中定义。这促使我们在第 5 节中定义了代数语义。对于许多逻辑来说,为了获得与代数语义类似的语义,使用与它们自然相关的代数类,我们需要为每个代数提供一组指定元素,这些元素不能仅通过代数语言的方程来定义,甚至不能仅通过使用该语言来定义。正如我们之前提到的,一个发生这种情况的例子是正常模态逻辑 K 的局部推论。此外,请记住,有些逻辑根本没有代数语义。

要赋予每个逻辑以一种代数性质的语义,至少需要考虑代数以及一组指定元素,而不需要使用相应的代数语言来定义它。这些对是逻辑矩阵。塔斯基在 20 世纪 20 年代定义了逻辑矩阵的一般概念,但这个概念在之前的工作中已经隐含在卢卡西维奇、伯奈斯、波斯特等人的工作中,他们在独立证明中或者用来定义不同于经典逻辑的逻辑时使用了真值表。逻辑矩阵是一个对 ⟨A,D⟩,其中 A 是一个代数,D 是 A 的宇宙的子集;D 的元素被称为矩阵的指定元素,因此 D 被称为指定元素的集合(有些作者称之为矩阵的真值集)。逻辑矩阵首先被用作特定逻辑系统的定理模型,例如在麦金西和塔斯基的工作中,还用来定义具有与逻辑系统的定理集相似属性的公式集,即在替换实例下封闭。这是卢卡西维奇的 n 值逻辑和他的无穷值逻辑的情况。而塔斯基首先将逻辑矩阵视为定义这种集合的一般工具。

在本条目中解释的逻辑矩阵的一般理论主要归功于波兰逻辑学家,从 1949 年的洛斯开始,继续到洛斯和苏斯科的 1958 年,借鉴了林登鲍姆的先前工作。在洛斯和苏斯科的论文中,矩阵首次被用作逻辑系统(按我们的意义)的模型,并用来定义这种系统的系统。

在本节的其余部分,我们使用现代术语介绍逻辑矩阵理论的相关概念。

给定一个逻辑 L,如果对于任何 Γ⊢Lϕ 的情况下,逻辑矩阵 ⟨A,D⟩ 是 L 的一个模型,那么对于矩阵 A 上的每个赋值 v,如果 v 将 Γ 的元素映射到某个指定值(即 D 的一个元素),那么 v 也将 ϕ 映射到一个指定值。当 ⟨A,D⟩ 是 L 的一个模型时,称 D 是代数 A 的一个 L-过滤器。代数 A 的 L-过滤器集合在逻辑系统的代数化理论中起着关键作用。我们将在后面讨论这一点。

逻辑矩阵类 M 被称为逻辑 L 的矩阵语义,如果

(*)

对于每个 ⟨A,D⟩∈M 和每个在 A 上的赋值 v,如果 v [Γ] ⊆D,则有 Γ⊢Lϕ 当且仅当 v(ϕ)∈D。

从左到右的蕴涵表明 L 相对于 M 是完备的,而另一个蕴涵表明它是完全的。换句话说,如果 M 是 L 的矩阵语义,那么 M 中的每个矩阵都是 L 的模型,而且对于每个 Γ 和 ϕ,使得 Γ⊬Lϕ,存在一个在 M 中证明这个事实的 L 的模型 ⟨A,D⟩,即存在一个在模型上的赋值,将 Γ 中的公式发送到指定的元素,将 ϕ 发送到非指定元素。

逻辑矩阵也用于语义上定义逻辑。如果 M=⟨A,D⟩ 是一个逻辑矩阵,那么由以下关系定义:

Γ⊢Mϕ 当且仅当对于 A 上的每个赋值 v,如果对于所有的 ψ∈Γ,v(ψ)∈D,则 v(ϕ)∈D。

是一个替换不变的推论关系;因此 ⟨L,⊢M⟩ 是一个逻辑系统。同样,我们可以通过将条件 (*) 视为推论关系的定义来定义一类矩阵 M 的逻辑。在关于多值逻辑的条目中,读者可以找到几种以这种方式定义的逻辑。

每个逻辑(无论如何定义)都有一个矩阵语义。此外,每个逻辑都有一个矩阵语义,其元素具有以下性质:矩阵 ⟨A,D⟩ 是简化的,如果 A 中没有两个不同的元素以相同的方式行为。我们说在 ⟨A,D⟩ 中 a,b∈A 以相同的方式行为,如果对于每个公式 ϕ(q,p1,…,pn) 和所有元素 d1,…,dn∈A,当且仅当 ϕA [a,d1,…,dn] ∈D 时,ϕA [b,d1,…,dn] ∈D。因此,如果存在一个公式 ϕ(q,p1,…,pn) 和元素 d1,…,dn∈A,使得 ϕA [a,d1,…,dn] 和 ϕA [b,d1,…,dn] 中的一个属于 D,但不是两者都属于 D,则 a,b∈A 以不同的方式行为。在 ⟨A,D⟩ 中以相同方式行为的关系是 A 的一个同余关系。这个关系在 Blok & Pigozzi 1986, 1989 中被称为矩阵 ⟨A,D⟩ 的 Leibniz 同余,并用 ΩA(D) 表示。它可以被描述为 A 的最大同余关系,与 D 兼容,即不将 D 中的元素与不在 D 中的元素相关联。Leibniz 同余的概念在 Blok 和 Pigozzi 在 1980 年代开发的逻辑系统代数化的一般理论中起着基础性的作用。读者可以参考 Font, Jansana, & Pigozzi 2003 和 Czelakowski 2001,了解有关这一时期围绕 Leibniz 同余概念的发展的详细信息。

每个矩阵 M 都可以通过识别其 Leibniz 同余关系相关的元素将其转化为一个简化矩阵。这个矩阵被称为 M 的简化,并通常用 M∗ 表示。一个矩阵及其简化是相同逻辑系统的模型,由于简化矩阵没有冗余元素,因此作为逻辑系统的矩阵语义的简化矩阵类通常被视为值得研究的矩阵类;它们更适合用代数术语来编码具有它们作为矩阵语义的逻辑的属性。

每个逻辑系统都有一个简化矩阵语义(即由简化矩阵组成的矩阵语义)的证明如下。设 L 是一个逻辑系统。考虑在公式代数上的矩阵 ⟨FmL,T⟩,其中 T 是 L 的一个理论。这些矩阵被称为 L 的 Lindenbaum 矩阵。很容易看出,这些矩阵的类是 L 的一个矩阵语义。由于一个矩阵及其简化是相同逻辑的模型,L 的 Lindenbaum 矩阵的简化构成了 L 的一个矩阵语义,而且是一个简化的矩阵语义。此外,任何包括 L 的简化 Lindenbaum 矩阵的简化矩阵模型类都自动成为 L 的一个完全矩阵语义。特别地,所有简化的 L 矩阵模型的类是 L 的一个完全矩阵语义。我们用 RMatr(L)表示这个类。

上述证明可以看作是 Lindenbaum-Tarski 方法的推广,用于证明我们将在下一节讨论的代数完备性定理。

在逻辑代数化理论中,RMatr(L)矩阵代数的类在代数化逻辑中起着重要的作用,它被表示为 Alg∗L。长期以来,它被认为是与给定逻辑 L 相关联的自然代数类。例如,在上述例子中,作为不同逻辑的代数语义的代数类(布尔代数,Heyting 代数等)恰好是相应逻辑 L 的 Alg∗L 类。事实上,Alg∗L 类与 1990 年代之前研究的所有逻辑 L 的自然代数类完全一致。在 1990 年代,由于对以前未研究的几种逻辑的了解,一些作者提出了另一种定义代数类的方法,这种方法应被视为与给定逻辑 L 相关联的代数对应物。对于许多逻辑 L,它确实导致了 Alg∗L 类,但对于其他逻辑,它给出了一个适当扩展的类。我们将在第 8 节中讨论它。

7. 用于证明代数完备性定理的 Lindenbaum-Tarski 方法

现在我们讨论最常用的用于证明代数类 K 是逻辑 L 的 δ(p)≈ε(p)-代数语义的 Lindenbaum-Tarski 方法。这是证明在第 5 节提到的例子的代数类是相应逻辑的代数语义的标准方法。

林登鲍姆-塔斯基方法在逻辑代数化理论的重要概念阐述方面做出了两方面的贡献。它构成了布洛克和皮戈齐的可代数逻辑概念的基础,并通过对其进行反思,可以为每个逻辑定义一个合理的代数类。我们将在第 8 节中讨论这个问题。

林登鲍姆-塔斯基方法可以概述如下。为了证明一个代数类 K 是逻辑 L 的 δ(p)≈ε(p)-代数语义,首先要证明 K 为 L 提供了一个合理的 δ(p)≈ε(p)-语义,即如果 Γ⊢Lϕ,则对于每个 A∈K 和每个在 A 中的赋值 v,如果 Γ 中的公式的值满足 δ(p)≈ε(p),那么 ϕ 的值也满足。其次,另一个方向,即完备性部分,是通过所谓的林登鲍姆-塔斯基方法来证明的。这种方法利用 L 的理论来获得公式代数的矩阵,然后将这些矩阵缩减,以便为每个矩阵获得一个代数在 K 中,并且其指定元素的集合是满足 δ(p)≈ε(p)的代数元素的集合。我们将逐步描述这种方法。

设 L 是第 5 节中讨论的逻辑之一。设 K 是我们在那里考虑的相应的代数类,δ(p)≈ε(p)是涉及声音和完备性定理的一个变量的方程。为了证明完备性定理,可以按照以下步骤进行。给定任何一组公式 Γ:

  1. 考虑 Γ 的理论 CL(Γ)={ϕ:Γ⊢Lϕ},我们用 T 表示,通过使用公式 p↔q 定义了一种二元关系 θ(T)在公式集合上,如下所示:⟨ϕ,ψ⟩∈θ(T)当且仅当 ϕ↔ψ∈T。

  2. 证明了 θ(T)是 FmL 上的一个同余关系。与公式 ϕ 相关的公式集合 [ϕ] 通过 θ(T)被称为 ϕ 的等价类。

  3. 通过识别由 θ(T)相关的公式,得到了一个新的矩阵 ⟨Fm/θ(T),T/θ(T)⟩,即 Fm/θ(T)是 Fm 模除 θ(T)的商代数,而 T/θ(T)是 T 的元素的等价类的集合。回想一下,商代数的代数运算定义如下:∗Fm/θ(T)([ϕ1],…,[ϕn])=[∗ϕ1…ϕn] 和†Fm/θ(T)=[†]。

  4. 证明了 θ(T)是与 T 相容的关系,即如果 ⟨ϕ,ψ⟩∈θ(T)且 ϕ∈T,则 ψ∈T。这意味着 ϕ∈T 当且仅当 [ϕ] ⊆T 当且仅当 [ϕ] ∈T/θ(T)。

  5. 证明了矩阵 ⟨Fm/θ(T),T/θ(T)⟩ 是简化的,Fm/θ(T)属于 K,并且 T/θ(T)是 Fm/θ(T)中满足方程 δ(p)≈ε(p)的元素的集合。

完备性定理的证明如下进行。根据(4)和(5),对于每个公式 ψ,如果 Γ⊢Lψ,则 [ψ] 满足方程 δ(p)≈ε(p)在代数 Fm/θ(T)中。因此,考虑将每个变量 p 映射到其等价类 [p] 的估值 id,其对所有公式的扩展 id(ϕ)=[ϕ],对于每个公式 ϕ,我们有对于每个公式 ψ,

Γ⊢Lψ 当且仅当 id(ψ)满足 Fm/θ(T)中的方程 δ(p)≈ε(p)。

因此,根据(5),由于 Fm/θ(T)∈K,如果 Γ⊬Lϕ,则存在一个代数 A∈K(即 Fm/θ(T))和一个估值 v(即 id),使得 v [Γ] 的元素满足 A 上的方程,但 v(ϕ)不满足。

当 Lindenbaum-Tarski 方法成功时,它表明了代数类{Fm/θ(T):T 是 L 的一个理论}是 L 的一个 δ(p)≈ε(p)-代数语义。因此,它还表明了每个包含集合{Fm/θ(T):T 是 L 的一个理论}且对 L 是 δ(p)≈ε(p)-合理的代数类 K 也是 L 的一个 δ(p)≈ε(p)-代数语义。

让我们对刚刚描述的 Lindenbaum-Tarski 方法进行一些评论。第一个评论对于导致与逻辑相关的代数类的概括是重要的。其他评论是为了获得代数逻辑概念定义中的条件。

  1. 条件(4)和(5)意味着 θ(T)实际上是 ⟨FmL,T⟩ 的 Leibniz 同余关系。

  2. 当 Lindenbaum-Tarski 方法成功时,通常在每个属于 K 的代数 A 中,由方程 δ(p↔q)≈ε(p↔q)定义的关系,即将 δ(p)≈ε(p)中的字母 p 替换为定义了一个理论的同余关系的公式 p↔q 的结果,是 A 上的恒等关系。

  3. 对于每个公式 ϕ,在 L 中,公式 δ(p/ϕ)↔ε(p/ϕ)和 ϕ 是互可推导的(即 ϕ⊢Lδ(p/ϕ)↔ε(p/ϕ)和 δ(p/ϕ)↔ε(p/ϕ)⊢Lϕ)。

由 Blok 和 Pigozzi 引入的可代数化逻辑概念,我们将在第 9 节中讨论,可以粗略地描述为:如果逻辑 L 具有代数语义(K,Eq),其中(1)K 包含在与 L 相关的自然代数类 Alg∗L 中,且(2)(K,Eq)是代数语义的事实可以通过稍微推广的 Lindenbaum-Tarski 方法证明。

8. 逻辑系统的自然代数类

现在我们将讨论两个被认为与逻辑 L 相关的代数的自然类的定义。这两个定义都可以看作是从 Lindenbaum-Tarski 方法的抽象中产生的,我们将沿着这条路径介绍它们。这些抽象的共同特点是它们忽略了 Lindenbaum-Tarski 方法中关系 θ(T)的具体定义方式。

值得注意的是,尽管如此,对于许多逻辑来说,这两个定义都导致了相同的类。从这两个定义得到的类已经被用于许多特定逻辑的代数研究中(对于某些逻辑来说是一个定义,对于其他逻辑来说是另一个定义),被认为是值得研究的自然类。

在第 6 节中,我们已经遇到了第一个概括,当时我们展示了每个逻辑都有一个简化矩阵语义。它导致了代数类 Alg∗L。它的定义是 Lindenbaum-Tarski 方法的概括,这是因为在文献中使用 Lindenbaum-Tarski 方法的完备性证明中,与 L-理论相关的关系 θ(T)实际上是矩阵 ⟨FmL,T⟩ 的 Leibniz 同余,因此矩阵 ⟨Fm/θ(T),T/θ(T)⟩ 是它的简化形式。正如我们在第 6 节中提到的,对于每个逻辑 L,对于包含所有矩阵 ⟨Fm/ΩFmL(T),T/ΩFmL(T)⟩(其中 T 是 L 的一个理论)的 L-声音矩阵类 M 来说,它是 L 的一个完备简化矩阵语义。从这个角度来看,矩阵的 Leibniz 同余的概念可以被看作是对任意矩阵的一种概括,这个概念来自于 Lindenbaum-Tarski 方法证明完备性的思路。按照这种推理方式,逻辑 L 的简化矩阵模型的代数类 Alg∗L 是与 L 相关的一种非常自然的代数类。它是该逻辑的简化矩阵模型的代数的类。

{A/ΩA(F):A 是一个 L-代数,F 是 A 的 L-滤子}。

第二种推广 Lindenbaum-Tarski 方法的方式使用了一个不同的事实,即在第 3 节讨论的例子中,关系 θ(T) 也是由条件定义的关系 Ω∼FmL(T),该条件为

⟨ϕ,ψ⟩∈Ω∼FmL(T) 当且仅当 ∀T′∈Th(L),∀p∈V,∀γ(p)∈FmL(T⊆T′⇒(γ(p/ϕ)∈T′⇔γ(p/ψ)∈T′))。

对于每个逻辑 L 和每个 L 理论 T,以这种方式定义的关系 Ω∼FmL(T)是与扩展 T 的所有 L 理论兼容的最大同余关系。因此,成立 Ω∼FmL(T)=⋂T′∈Th(L)TΩFmL(T′),其中 Th(L)T={T′∈Th(L):T⊆T′}。关系 Ω∼FmL(T)被称为 T 的 Suszko 同余关系(相对于 L)。Suszko 在 1977 年以等价的方式定义了它。

对于每个逻辑 L,Suszko 同余关系的概念可以扩展到其矩阵模型。L 的矩阵模型 ⟨A,D⟩ 的 Suszko 同余关系(相对于 L)是 A 的与包括 D 的每个 L 过滤器兼容的最大同余关系,即由 Ω∼AL(D)=⋂D′∈FiL(A)DΩA(D′)给出。其中 FiL(A)D={D′:D′是 A 的 L 过滤器且 D⊆D′}。请注意,与 Leibniz 同余的内在概念不同,L 的矩阵模型的 Suszko 同余关系不是矩阵的内在属性:它在很大程度上取决于所考虑的逻辑。关于矩阵的 Suszko 同余关系的理论已经在 Czelakowski 2003 中得到发展,并在 Albuquerque&Font&Jansana 2016 中继续。

以与 Leibniz 同余的概念导致约化矩阵的概念相同的方式,Suszko 同余的概念导致 Suszko 约化矩阵的概念。L 的矩阵模型如果其 Suszko 同余关系是恒等关系,则为 Suszko 约化。然后,L 的 Suszko 约化矩阵模型的代数类是另一个被视为与 L 相关联的自然代数类。它是

AlgL={A/Ω∼AL(F):A 是一个 L-代数,F 是 A 的 L-滤子}。

在抽象代数逻辑中,这个类被认为是与 L 相关的自然类别的代数对应物。

对于任意逻辑 L,类别 AlgL 和 Alg∗L 之间的关系是 AlgL 是 Alg∗L 在子直积下的闭包,特别地,Alg∗L⊆AlgL。一般情况下,这两个类别可能是不同的。例如,如果 L 是经典命题逻辑的(∧,∨)-片段,那么 AlgL 是分配格的种类(一直被认为是与 L 相关的自然类别的代数),而 Alg∗L 则是它的真子集——事实上,Alg∗L 不是一个拟种类。然而,对于许多逻辑 L,特别是在接下来的几节中要讨论的可代数化和原代数化逻辑,以及当 Alg∗L 是一个种类时,类别 AlgL 和 Alg∗L 是相等的。这个事实可以解释为什么在 20 世纪 80 年代,在非原代数化逻辑的代数研究被认为不值得追求之前,这两个定义之间的概念差异是不需要的,因此也没有被考虑(甚至没有被发现)。

9. 当一个逻辑可代数化时,这意味着什么?

可代数化逻辑被认为是与其代数对应物之间具有最强可能联系的逻辑。这一要求要求逻辑的代数对应物应该是一个代数语义,但需要比这更强大的逻辑与代数对应物之间的连接。这种更强大的连接存在于已知的行为最佳的特定逻辑中。数学上精确的可代数化逻辑的概念表征了这种类型的联系。Blok 和 Pigozzi 在 Blok&Pigozzi 1989 中引入了这个基本概念,它的引入可以被认为是 20 世纪 80 年代抽象代数逻辑领域的统一和发展的起点。Blok 和 Pigozzi 仅为有限逻辑定义了可代数化逻辑的概念。后来,Czelakowski 和 Herrmann 将其推广到任意逻辑,并在定义中放宽了一些条件。我们在这里介绍广义概念。

我们在第 7 节中说过,粗略地说,当逻辑 L 可代数化时,1)它具有代数语义,即,存在一个代数类 K 和一组方程 Eq(p),使得 K 是 L 的 Eq-代数语义,2)这个事实可以通过使用略微推广的 Lindenbaum-Tarski 方法来证明,而且,3)K⊆Alg∗L。Lindenbaum-Tarski 方法的推广(如我们在第 7 节中描述的)在步骤(5)中允许使用一个变量的方程集 Eq(p)(与代数语义的定义中已经做过的一样),并且以类似的方式允许使用最多两个变量的公式集 Δ(p,q)来扮演理论的公式 p↔q 在定义理论的同余时的角色。然后,给定一个理论 T,与 T 兼容的公式代数上的最大同余关系 θ(T)由以下方式定义:

⟨ϕ,ψ⟩∈θ(T) 当且仅当 Δ(p/ϕ,q/ψ)⊆T.

在精确定义可代数化逻辑之前,我们需要一些符号约定。给定一个变量的方程集合 Eq(p) 和一个公式 ϕ,令 Eq(ϕ) 为通过将 Eq 中的所有方程中的变量 p 替换为 ϕ 而得到的方程集合。如果 Γ 是一个公式集合,那么

Eq(Γ):=⋃ϕ∈ΓEq(ϕ)。

同样地,给定一个包含两个变量 Δ(p,q)和一个等式 δ≈ε 的公式集合,让 Δ(δ,ε)表示通过在 Δ 中的所有公式中将 p 替换为 δ,将 q 替换为 ε 所得到的公式集合。此外,如果 Eq 是一个等式集合,那么

Δ(Eq)=⋃δ≈ε∈EqΔ(δ,ε)。

给定一个包含两个变量 p 和 q 的等式集合 Eq(p,q),这个集合在每个代数 A 上定义了一个二元关系,即满足 Eq(p,q)中的所有等式的 A 中元素 a 和 b 的集合。在标准模型论符号中,这个集合是关系

{⟨a,b⟩:a,b∈A 且 A⊨Eq(p,q)[a,b]}.

代数逻辑的形式定义如下。如果存在一个代数类 K,一个变量为 p 的方程集 Eq(p),和一个变量为 p 和 q 的公式集 Δ(p,q),那么逻辑 L 是可代数化的。

  1. K 是 L 的 Eq-代数语义,即 K 是 L 的 Eq-代数语义。

Γ⊢Lϕ 当且仅当对于每个 A∈K 和每个在 A 上的估值 v,如果 v [Γ] ⊆Eq(A),则 v(ϕ)∈Eq(A)。

  1. 对于每个 A∈K,由两个变量的方程集 Eq(Δ(p,q))定义的关系是 A 上的恒等关系。

对于这样的一类代数 K,存在集合 Eq(p)和 Δ(p,q)具有这两个性质,称为 L 的等价代数语义。集合 Δ 称为等价公式集,集合 Eq 称为定义方程集。

定义的条件意味着:

  1. 在公式集合 Δ(Eq)中,p 在 L 中与之相互推导,即 Δ(Eq)⊢Lp 和 p⊢LΔ(Eq)。

  2. 对于每个 L 理论 T,⟨FmL,T⟩ 的 Leibniz 同余关系是由 Δ(p,q)定义的关系,即 ⟨ϕ,ψ⟩∈ΩFm(T)当且仅当 Δ(p/ϕ,q/ψ)⊆T。

  3. 如果 Δ 和 Δ'是两组等价公式集合,Δ⊢LΔ'且 Δ'⊢LΔ。同样地,如果 Eq(p)和 Eq'(p)是两组定义方程集合,对于每个代数 A∈K,Eq(A)=Eq'(A)。

  4. 代数类 Alg∗L 也满足条件(1)和(2),因此它是 L 的等价代数语义。此外,它是一个 SP 类,并包括其他所有作为 L 的等价代数语义的代数类。因此,它被称为 L 的最大等价代数语义。

  5. 对于每个 A∈Alg∗L,存在唯一的 L-滤子 F,使得矩阵 ⟨A,F⟩ 是简化的,而这个滤子就是集合 Eq(A)。或者换句话说,L 的简化矩阵模型类是{⟨A,Eq(A)⟩:A∈Alg∗L}。

Blok 和 Pigozzi 在 1989 年的 Blok&Pigozzi 中对可代数化逻辑的定义仅适用于有限逻辑,并且他们还要求定义方程和等价公式的集合应该是有限的。今天我们说,如果等价公式集合 Δ 和定义方程集合 Eq 都可以取为有限集,则可代数化逻辑是有限可代数化的。我们说,如果逻辑是 Blok-Pigozzi 可代数化(BP-可代数化),则它是有限的并且有限可代数化的。

如果 L 是有限的并且有限可代数化的,则 Alg∗L 不仅是一个 SP 类,而且是一个准变种,并且它是由任何等价的代数语义 K 生成的准变种。

我们刚刚看到,在可代数化逻辑中,代数类 Alg∗L 起着重要的作用。此外,在这些逻辑中,通过两种推广 Lindenbaum-Tarski 方法获得的代数类是相同的,即 Alg∗L=AlgL——这是因为对于任何可代数化逻辑 L,Alg∗L 在子直积下是封闭的。因此,对于每个可代数化逻辑 L,它的代数对应物 AlgL 是它最大的等价代数语义,无论对 Lindenbaum-Tarski 方法的推广采取何种观点。

代数化逻辑(实例化为 Alg∗L)的定义的条件(1)和(2)编码了代数化逻辑 L 及其代数类 AlgL 之间存在非常强的联系,以至于这个代数类通过 AlgL 的代数性质反映了 L 的元逻辑性质,反之亦然。

代数化逻辑的定义可以等价地表述为逻辑与与之相关的等式推理关系 ⊨K 之间的翻译,其中 K 是其等价代数语义的任何选择,这个关系在选择等价代数语义时是相同的。

一类代数 K 的等式推理 ⊨K 定义如下。

{ϕi≈ψi:i∈I}⊨Kϕ≈ψ 当且仅当对于每个 A∈K 和每个 A 上的估值 v,如果对于所有 i∈I,v(ϕi)=v(ψi),那么 v(ϕ)=v(ψ)。

所需的翻译由定义方程集和等价公式集给出。一个变量的方程集 Eq(p)定义了从公式到方程集的翻译:每个公式被翻译成方程集 Eq(ϕ)。类似地,一个两个变量的公式集 Δ(p,q)定义了从方程到公式集的翻译:每个方程 ϕ≈ψ 被翻译成公式集 Δ(ϕ,ψ)。

代数化逻辑定义中的条件(1)可以重新表述为 Γ⊢Lϕ 当且仅当 Eq(Γ)⊨KEq(ϕ),条件(2)可以表述为 p≈q⊨KEq(Δ(p,q))和 Eq(Δ(p,q))⊨Kp≈q。

这两个条件意味着

  1. {ϕi≈ψi:i∈I}⊨Kϕ≈ψ 当且仅当 Δ({ϕi≈ψi:i∈I})⊢LΔ(ϕ,ψ)

而上述条件(3)是随附的

p⊢LΔ(Eq(p))和 Δ(Eq(p))⊢Lp。

因此,一个可代数化的逻辑 L 通过将公式翻译为由一组定义方程给出的方程集合,并且通过等价公式集合给出的方程翻译为公式集合的方式,忠实地在其等价代数语义的等式逻辑中被解释(条件(1))。而其等价代数语义的等式逻辑通过将方程翻译为由一组方程给出的公式集合,并且通过等价方程集合给出的公式翻译为方程集合的方式,忠实地在逻辑 L 中被解释(条件(9))。此外,这两种翻译是彼此的逆(条件(2)和(3)),在逻辑等价的模态下。通过这种方式,我们可以看到 L 与其最大等价代数语义之间的联系非常紧密,并且 L 的属性应该转化为相关联的等式推理关系的属性。当然,这种关系实际上具有的属性取决于代数类 AlgL 的属性。

给定逻辑 L 的一个代数语义(K,Eq),强调它仅仅是一个代数语义和它是一个使 L 可代数化的代数语义之间的区别的一种方式是,由方程集合 Eq 给出的公式到方程的翻译是可逆的,即存在一个称为 Δ 的方程到公式的翻译,由一个包含两个变量的公式集合给出,满足上述条件(9),并且 Eq 和 Δ 提供互为逆的翻译(即,条件(2)和(3)成立)。

一个可代数化逻辑 L 与其最大等价代数语义之间的链接,由定义方程集和等价公式集给出,使我们能够证明一系列将 L 的性质与 AlgL 的性质相关联的一般定理。这些定理通常被称为桥梁定理。我们将举三个例子。

第一个涉及演绎定理。要证明一个将演绎定理的存在与代数性质相关联的一般定理,首先需要定义一个适用于任何逻辑的演绎定理的概念。如果逻辑 L 具有演绎-分离性质,则存在一个有限的公式集 Σ(p,q),对于每个公式集 Γ 和所有公式 ϕ,ψ

Γ∪{ϕ}⊢Lψ 当且仅当 Γ⊢LΣ(ϕ,ψ)。

注意,这是标准演绎定理(上述表达式中从左到右的方向)和 Modus Ponens(等同于从右到左的蕴含)的一般化,多个逻辑学对于连接词→都有。在这些情况下,Σ(p,q)={p→q}。

定理 1。 一个有限且有限可代数化的逻辑 L 具有演绎-分离性质,当且仅当 AlgL 中的代数的主相对同余是等式可定义的。

第二个定理涉及到克雷格插值。插值的几个概念适用于任意逻辑。我们只考虑其中之一。如果逻辑 L 对于推理关系具有克雷格插值性质,那么无论 Γ⊢Lϕ 以及 ϕ 的变量集与 Γ 中公式的变量集有非空交集,都存在一个有限的公式集 Γ',其变量集包含在 ϕ 和 Γ 中公式的变量集的交集中,使得 Γ⊢LΓ'且 Γ'⊢Lϕ。

定理 2。 设 L 是一个有限且有限可代数化的逻辑,具有演绎-分离性质。那么当且仅当 AlgL 具有合并性质时,L 具有克雷格插值性质。

最后,第三个定理涉及 Beth 可定义性质。感兴趣的读者可以在 Font, Jansana&Pigozzi 2003 中找到定义。在我们所处的一般情况下,该性质过于复杂,无法在此处陈述。

定理 3。 有限且有限可代数化的逻辑具有 Beth 性质,当且仅当范畴中以 AlgL 中的代数为对象,代数同态为态射的满同态是满同态。

其他与代数可化逻辑的性质及其自然代数类的性质相关的结果可以在 Raftery 2011、2013 中找到。它们分别涉及具有演绎-分离性质的性质的推广,以及推广了经典逻辑和直觉逻辑的不一致引理的性质。此外,在 Torrens 2008 中,提出了一个关于经典逻辑和直觉逻辑之间类似 Glivenko 定理的抽象概念,并与代数化逻辑的情况下的代数性质相关联。最近,Raftery 2016 提出了与可接受规则和结构完备性相关的桥梁定理,而 Lávička 等人在 2021 年研究了与弱排中性质相关的桥梁定理。

对于一些代数是某种代数可化逻辑的等价代数语义的类,很久以来已经知道对于类中的每个代数,代数的同余格和代数的子集格之间存在一个同构,这个同构具有重要的代数意义。例如,在布尔代数和 Heyting 代数中,这些子集是格过滤器,而在模态代数中,它们是在解释 □ 的操作下封闭的格过滤器。在所有这些情况下,这些集合恰好是相应的代数可化逻辑 L 的 L-过滤器。

代数化逻辑可以通过在其代数对应物的代数上的同余和逻辑过滤器之间存在这种同构来进行表征。为了阐明这种表征,我们需要一些定义。设 L 是一个逻辑。对于代数 A(相对于 L),Leibniz 算子是从 A 的 L-过滤器到 A 的同余集合的映射,它将 A 的每个 L-过滤器 D 映射到其 Leibniz 同余 ΩA(D)。我们说逻辑 L 的 Leibniz 算子与类 K 中代数之间的同态的逆元交换,如果对于每个从代数 A∈K 到代数 B∈K 的同态 h 和每个 B 的 L-过滤器 D,h−1 [ΩB(D)]=ΩA(h−1 [D])。

定理 4。 逻辑 L 是可代数化的当且仅当对于每个 A∈AlgL 的代数 A,Leibniz 算子与 AlgL 中的代数之间的同态的逆元交换,并且它是 A 的所有 L-过滤器的集合(按包含关系排序)和 A 的同余集合 θ 的集合之间的同构,其中 A/θ∈AlgL,同样按包含关系排序。

定理提供了对上述已知同构以及其他类别的代数同构的逻辑解释。例如,群的同余和正规子群之间的同构可以通过存在一个可代数化的逻辑 L 来解释,其中群的类别是其最大等价代数语义,群的正规子群是其 L-滤子。

代数化逻辑的一个不同但相关的特征描述如下:

定理 5。 如果且仅当在公式代数 FmL 的代数上,将每个理论 T 发送到其 Leibniz 同余的映射与从 FmL 到 FmL 的同态的逆元交换,并且它是 L 的理论集 Th(L)和 FmL 的同余集 θ 的集合之间的同构,其中 FmL/θ∈AlgL,按包含顺序排序。

10. 逻辑的分类

不幸的是,并非每个逻辑都是可代数化的。非可代数化逻辑的典型例子是正常模态逻辑 K 的局部推论。让我们讨论这个例子。

本地模态逻辑 lK 和相应的全局模态逻辑 gK 不仅不同,而且它们的元逻辑属性也不同。例如,lK 对于→具有演绎-分离性质:

Γ∪{ϕ}⊢lKψ 当且仅当 Γ⊢lKϕ→ψ。

但是 gK 根本没有演绎-分离性质。

逻辑 gK 是可代数化的,而 lK 不是。gK 的等价代数语义是模态代数的种类 MA,等价公式集合是{p↔q},定义方程集合是{p≈⊤}。有趣的是,lK 和 gK 有相同的代数对应物(即 AlglK=AlggK),即模态代数的种类。

从这个例子中可以得出一个教训,即逻辑 L 的代数对应物 AlgL 不一定完全编码 L 的属性。模态代数类编码了 gK 的属性,因为这个逻辑是可代数化的,因此 gK 和 AlggK 之间的联系是尽可能强的。但是,模态代数类 AlglK 本身无法完全编码 lK 的属性。

导致 gK 和 lK 之间的这种差异的原因是 gK 的简化矩阵模型类是{⟨A,{1A}⟩:A∈MA},但是 lK 的简化矩阵模型类适当地包含了这个类,因此对于一些代数 A∈MA,除了{1A}之外,还存在一些其他的 lK-filter F,使得 ⟨A,F⟩ 是简化的。这个事实提供了一种方法来证明 lK 不能通过从代数中等式定义简化矩阵的 lK-filter 来代数化;如果可以的话,那么对于每个 A∈AlglK,都会存在一个唯一的 lK-filter F 使得 ⟨A,F⟩ 是简化的。

尽管如此,我们可以在逻辑 lK 中执行 Lindenbaum-Tarski 方法的一些步骤。我们可以通过使用两个变量的公式以统一的方式定义每个 lK 理论的 Leibniz 同余。但在这种特殊情况下,公式集必须是无限的。设 Δ(p,q)={□n(p↔q):n 为自然数},其中对于每个公式 ϕ,□0ϕ 为 ϕ,对于 n>0 的 □nϕ 是在前面有 n 个方框的公式(□…□ϕ)。然后,对于每个 lK 理论 T,由 ⟨ϕ,ψ⟩∈θ(T) iff {□n(ϕ↔ψ):n 为自然数}⊆T 定义的关系 θ(T)是 T 的 Leibniz 同余。

在这种情况下,出现了两个具有相同 Leibniz 同余的不同 lK 理论,而这在 gK 中是不成立的。

is the Leibniz congruence of T. In this case, it happens though that there are two different lK-theories with the same Leibniz congruence, something that does not hold for gK.

具有以下特性的逻辑 L:存在一个由两个变量定义的公式集合(可能是无限的)Δ(p,q),在每个 L 理论 T 中,它定义了其 Leibniz 同余,即对于所有 L 公式 ϕ,ψ,⟨ϕ,ψ⟩∈ΩFm(T)当且仅当 Δ(ϕ,ψ)⊆T,被称为等价逻辑。如果 Δ(p,q)是有限的,则该逻辑被称为有限等价逻辑。在每个 L 理论中定义其 Leibniz 同余的 Δ(p,q)集合被称为 L 的等价公式集。很明显,每个可代数化逻辑都是等价逻辑,每个有限可代数化逻辑都是有限等价逻辑。

根据定义,逻辑 lK 是等价逻辑,并且可以证明它不是有限等价逻辑。局部模态逻辑 lS4 是一个非可代数化逻辑的例子,它是有限等价逻辑。lS4 的等价公式集为{□(p↔q)}。

逻辑 L 的等价公式集应被视为广义双条件,即集合中的公式共同具有双条件的相关特性,例如在经典逻辑中,使其适用于定义其理论的 Leibniz 同余。这在以下等价公式集的句法特征化中非常明显。

定理 6. 如果一个逻辑 L 的 L-公式集合 Δ(p,q)是一个等价公式集合,那么它就是逻辑 L 的等价公式集合。

(RΔ)

⊢LΔ(p,p)

(MPΔ)

p,Δ(p,q)⊢Lq

(SΔ)

Δ(p,q)⊢LΔ(q,p)

(TΔ)

Δ(p,q)∪Δ(q,r)⊢LΔ(p,r)

(ReΔ)

Δ(p1,q1)∪…∪Δ(pn,qn)⊢LΔ(∗p1…pn,∗q1…qn),对于每个具有大于 0 的 n 元连接词 ∗ 的 L。

定理中存在一些冗余。条件(SΔ)和(TΔ)可以从(RΔ),(MPΔ)和(ReΔ)推导出来。

等价逻辑首次被视为一类值得研究的逻辑,见 Prucnal&Wroński 1974,并在 Czelakowski 1981 中进行了广泛研究;另请参阅 Czelakowski 2001。

我们已经提到,可代数化逻辑是等价逻辑。等价逻辑和可代数化逻辑之间的区别可以从以下代数命题的句法特征化中看出:

定理 7. 如果且仅当存在一个 L-公式集合 Δ(p,q)和一个 L-方程集合 Eq(p),满足上述条件(RΔ)-(ReΔ),L 逻辑 L 是可代数化的。并且 p⊢LΔ(Eq(p))和 Δ(Eq(p))⊢Lp。

定理中的集合 Δ(p,q)是 L 的等价公式集合,集合 Eq(p)是定义方程集合。

有一些逻辑不是等价的,但具有一组公式的属性,这些公式在某种弱意义上集体表现出许多逻辑中的蕴涵→的行为。也就是说,在等价公式集的句法特征化中具有(RΔ)和(MPΔ)的属性,即

(R⇒)

⊢L [p⇒p]

(MP⇒)

p,[p⇒q] ⊢Lq

如果一个逻辑是有限的,并且具有一组具有这些属性的公式,那么总是存在一个具有相同属性的有限子集。具有一组具有上述属性(1)和(2)的公式(有限或无限)的逻辑被称为原代数逻辑。因此,每个等价逻辑和可代数化逻辑都是原代数逻辑。

Protoalgebraic logics were first studied by Czelakowski, who called them non-pathological, and slightly later by Blok and Pigozzi in Blok & Pigozzi 1986. The label 'protoalgebraic logic' is due to these last two authors.

The class of protoalgebraic logics turned out to be the class of logics for which the theory of logical matrices works really well in the sense that many results of universal algebra have counterparts for the classes of reduced matrix models of these logics and many methods of universal algebra can be adapted to its study; consequently the algebraic study of protoalgebraic logics using their matrix semantics has been extensively and very fruitfully pursued. But, as we will see, some interesting logics are not protoalgebraic.

An important characterization of protoalgebraic logics is via the behavior of the Leibniz operator. The following conditions are equivalent:

  1. L 是原代数的。

  2. 对于 L-理论的集合,Leibniz 算子 ΩFmL 在包含关系下是单调的,即如果 T⊆T'是 L-理论,则 ΩFmL(T)⊆ΩFmL(T')。

  3. 对于每个代数 A,Leibniz 算子 ΩA 在 A 的 L-滤子集合上是单调的,与包含关系有关。

由于 Leibniz 运算符的单调性属性,对于每个原代数逻辑 L,代数类 Alg∗L 在子直积下是封闭的,因此它等于 AlgL。因此,对于原代数逻辑,我们遇到的两种将代数类与逻辑相关联的方式,正如我们已经提到的,产生相同的结果。

通过 Leibniz 运算符的行为,还可以对等价逻辑和有限等价逻辑进行表征。读者可以参考 Czelakowski 2001 和 Font&Jansana&Pigozzi 2003。

在他的 Raftery 2006b 中,Raftery 研究了我们在定义之后给出的代数逻辑性质列表中的第 7 个条件。该条件是:

对于每个 A∈Alg∗L,L 的简化矩阵模型的类是{⟨A,Eq(A)⟩:A∈Alg∗L},其中 Eq(p)是 L 的定义方程集合。

具有满足此属性的方程集 Eq(p)的逻辑,即对于每个 A∈Alg∗L,L 的简化矩阵模型的类是{⟨A,Eq(A)⟩:A∈Alg∗L},被称为真值方程逻辑,这个名称是在 Raftery 2006b 中引入的。一些真值方程逻辑是原代数逻辑,但其他一些不是。稍后我们将看到最后一种的一个例子。

真值方程逻辑中的原代数逻辑实际上是 Czelakowski&Jansana 2000 年已经研究过的弱代数逻辑。每个可代数化逻辑都是弱代数逻辑。事实上,可代数化逻辑是等值逻辑中的真值方程逻辑。但并非每个弱代数逻辑都是等值逻辑。一个例子是由正交格中的矩阵 ⟨A,{1}⟩ 确定的逻辑,其中 A 是正交格,1 是其最大元素(参见 Czelakowski&Jansana 2000 年和 Malinowski 1990 年)。

到目前为止,我们考虑的逻辑类别是被称为莱布尼兹层次的主要类别,因为它的成员是可以通过莱布尼兹运算符的行为来表征的逻辑类别。我们只描述了层次结构中最重要的逻辑类别。读者可以参考 Czelakowski 2001 年、Font、Jansana 和 Pigozzi 2003 年、Font 2016 年和 2022 年的更多信息。特别是,Czelakowski 2001 年广泛收集了其出版时已知的莱布尼兹层次的不同类别的信息,而 Font 2016 年则是一本非常适合学习莱布尼兹层次和抽象代数逻辑的介绍性教材,可以了解到关于莱布尼兹层次和抽象代数逻辑的最重要的事实。

在本条目中考虑的莱布尼兹层次的类别之间的关系总结如下图所示:

图。莱布尼兹层次

最近,Leibniz 层次结构在 Cintula&Noguera 2010、2016 年得到了完善。其思想是考虑一组公式 [p⇒q],而不是等价公式集合 Δ(对应于双条件)。这组公式 [p⇒q] 具有通常条件(→)的几个特性,其中包括原代数逻辑定义中的(R⇒)和(MP⇒)。集合 [p⇒q] 应满足其对称化 [p⇒q] ∪ [q⇒p] 是一组等价公式。当集合 [p⇒q] 只有一个元素时,会出现新的类别。关于此的详细信息可以在最近的书籍 Cintula&Noguera 2021 中找到。这本书也可以作为从蕴涵的角度撰写的抽象代数逻辑的入门。

11. 替换原则

在抽象代数逻辑中,有两类不属于 Leibniz 层次结构的逻辑得到了广泛研究。它们是从与 Leibniz 运算符的行为不同的角度定义的,即从逻辑可能具有的替换原则的角度来定义。

一个逻辑系统 L 可能具有的最强替换原则,例如古典逻辑、直觉主义逻辑及其所有公理扩展所共享的,它表明对于任何公式集 Γ,任何公式 ϕ,ψ,δ 和任何变量 p,

如果 Γ,ϕ⊢Lψ 和 Γ,ψ⊢Lϕ,则 Γ,δ(p/ϕ)⊢Lδ(p/ψ)和 Γ,δ(p/ψ)⊢Lδ(p/ϕ),

其中 δ(p/ϕ)和 δ(p/ψ)是通过将 ϕ 和 ψ 分别替换 p 而得到的公式。一些作者将这种替换性质视为 Frege 关于真理组合性的形式对应物。满足这种强替换性质的逻辑被称为 Fregean,见 Font&Jansana 1996,并在 Czelakowski&Pigozzi 2004a、2004b 中进行了深入研究。

许多重要的逻辑不满足强替换性质,例如几乎所有的模态逻辑(局部或全局),但是一些逻辑,例如正常模态逻辑的局部蕴涵关系,满足一个较弱的替换原则:对于所有的公式 ϕ, ψ, δ,

如果 ϕ ⊢L ψ 和 ψ ⊢L ϕ,则 δ(p/ϕ) ⊢L δ(p/ψ) 和 δ(p/ψ) ⊢L δ(p/ϕ)。

满足这个较弱替换性质的逻辑被 Wójcicki 称为自扩展的(例如,在 Wójcicki 1969, 1988 中),而在 Humberstone 2005 中被称为同余的。我们将使用第一个术语,因为它在抽象代数逻辑文献中似乎更常见。必须提到的是,自扩展逻辑的所有片段都是自扩展的,类似的事实在 Fregean 逻辑中也成立。此外,自扩展和 Fregean 之间的差异不仅出现在像正常模态逻辑的局部蕴涵关系这样的原代数逻辑中,也出现在非原代数逻辑中。Belnap 和 Dunn 的四值逻辑(有关信息请参见 Font 1997)是自扩展的、非原代数的和非 Fregean 的。

自我扩展逻辑从多个角度来看具有非常良好的行为。它们的系统研究始于 Wójcicki 1969 年,并在 Font&Jansana 1996 年的抽象代数逻辑背景下继续进行;Jansana 2005 年,2006 年;以及 Jansana&Palmigiano 2006 年。

在 Leibniz 层次结构的任何一个类别中,都存在自我扩展和非自我扩展的逻辑,也存在非原代数逻辑的类别。这些事实表明,导致考虑 Leibniz 层次结构中的类别的观点和导致将自我扩展逻辑和 Frege 逻辑定义为值得整体研究的逻辑类别的观点在很大程度上是不同的。尽管如此,抽象代数逻辑的当今研究趋势之一是确定两种观点之间的相互作用,并研究在穿越这两种分类时产生的逻辑类别。实际上,替换原则与 Suszko 同余(因此与 Leibniz 同余)之间存在联系。如果逻辑 L 满足强替换原则,那么对于每个 L-理论 T,其 Suszko 同余是相对于 T 的互可推导关系,即关系{⟨ϕ,ψ⟩:T,ϕ⊢Lψ 和 T,ψ⊢Lϕ}。如果逻辑 L 满足弱替换原则,那么 L 的定理集的 Suszko 同余是互可推导关系{⟨ϕ,ψ⟩:ϕ⊢Lψ 和 ψ⊢Lϕ}。

从替换原则的角度研究逻辑系统导致了我们在第 14 节中阐述的所谓 Frege 层次结构。

12. 超越原代数逻辑

并非所有有趣的逻辑都是原代数逻辑。在本节中,我们将简要讨论四个非原代数逻辑的例子:合取和析取逻辑、正模态逻辑、lK 的严格蕴涵片段和 Visser 的次直觉逻辑。它们都是自扩展的。在下一节中,我们将阐述抽象逻辑和广义矩阵的语义,这有助于发展一个真正通用的逻辑系统代数化理论。正如我们将看到的,透过逻辑矩阵模型理论的视角在一个重要方面发生了变化。

12.1 合取和析取逻辑

这个逻辑是经典命题逻辑的{∧,∨,⊥,⊤}片段。因此它的语言是集合{∧,∨,⊤,⊥},其推论关系由

Γ⊢ϕ 当且仅当 Γ⊢CPLϕ。

结果表明它也是直觉主义命题逻辑的{∧,∨,⊥,⊤}片段。我们用 L{∧,∨}来表示它。

逻辑 L{∧,∨}不是原代数,但它是弗雷格式的。代数类 AlgL{∧,∨}是有界分配格的种类,这是与 L{∧,∨}相关联的代数类,但代数类 Alg∗L{∧,∨}严格包含在其中。实际上,这个最后的代数类不是拟种类,但它仍然足够好以进行一阶定义。

逻辑 L{∧,∨}因此是一个自然的例子,其中其缩减矩阵模型的代数类不是预期与之对应的正确代数类(参见 Font&Verdú 1991,其中详细研究了该逻辑)。这个例子的属性及其在 Font&Verdú 1991 中的处理激发了 Font&Jansana 1996 对 Brown&Suszko 1973 中考虑的命题逻辑模型类型,即抽象逻辑的系统研究。

12.2 正模态逻辑

正模态逻辑是局部正常模态逻辑 lK 的{∧,∨,□,◊,⊥,⊤}片段。我们用 PML 表示它。这种逻辑在计算机科学中具有一定的兴趣。

逻辑 PML 不是原代数的,它不是真值等式的,它是自扩展的,也不是弗雷格式的。它的代数对应物 AlgPML 是 Dunn 在 Dunn 1995 中引入的正模态代数类。这种逻辑在 Jansana 2002 中从抽象代数逻辑的角度进行了研究。代数类 AlgPML 与 Alg∗PML 不同。

12.3 Visser 的次直觉逻辑

这种逻辑是直觉逻辑语言中的逻辑,它与最普通的模态逻辑 K 具有与直觉逻辑与正常模态逻辑 S4 相同的关系。它是在 Visser 1981 年引入的(以基本命题逻辑的名义),并由 Ardeshir、Alizadeh 和 Ruitenburg 等多位作者进行了研究。它不是原代数的,它是真值等式的,它是弗雷格式的(因此也是自扩展的)。

12.4 本地模态逻辑 lK 的严格蕴涵片段

模态逻辑语言的严格蕴涵是使用 □ 运算符和材料蕴涵→来定义的。我们将使用 ⇒ 表示严格蕴涵。它的定义是 ϕ⇒ψ:=□(ϕ→ψ)。我们称之为本地模态逻辑 lK 的严格蕴涵片段的逻辑 SilK 的语言是 L={∧,∨,⊥,⊤,⇒}。我们可以通过系统地将 L-公式 ϕ 中的每个形式为 ψ⇒δ 的子公式替换为 □(ψ→δ),并重复此过程直到没有 ⇒ 的出现来将 L 的公式翻译为模态语言的公式。让我们用 ϕ∗ 表示 ϕ 的翻译,用 Γ∗ 表示 Γ 中公式的翻译。那么 SilK 的蕴涵关系的定义是:

Γ⊢SilKϕ 当且仅当 Γ∗⊢lKϕ∗。

逻辑 SilK 既不是原代数的,也不是真值等式的。它是自扩展的,但不是弗雷格式的。它的代数对应物 AlgSilK 是具有 lK 的严格蕴涵性质的有界分配格的类。这个代数类在 Celani&Jansana 2005 年中被引入和研究,其中它的成员被称为弱 Heyting 代数。AlgSilK 与 Alg∗SilK 不重合。

逻辑 SilK 属于所谓的次直觉逻辑家族,就像 Visser 的逻辑一样。关于这些逻辑的信息,可以参考 Celani&Jansana 2003 年的文献。

读者可以在 2017 年的 Albuquerque 等人的著作中找到更多关于有趣的非代数逻辑的信息。

13. 抽象逻辑和广义矩阵

给定逻辑的逻辑矩阵模型可以被看作是其理论的代数推广,更准确地说,是其 Lindenbaum 矩阵的推广。它们来自于以逐个考虑逻辑的理论及其类似物逻辑滤波器(也逐个考虑)为中心的局部视角。但是,正如我们将看到的,逻辑的性质通常取决于将其理论作为一堆整体行为的全局行为;或者换句话说,取决于其推理关系。对这种全局行为的考虑引入了对逻辑系统语义设计的全局视角。与逻辑矩阵相比,我们将要定义的抽象逻辑可以被看作是逻辑本身及其扩展的代数推广。当我们认真考虑全局视角时,它们是需要考虑的自然对象。

设 L 为一个命题语言。一个 L-抽象逻辑是一个二元组 A=⟨A, C ⟩,其中 A 是一个 L-代数,C 是 A 上的一个抽象推论运算。

给定一个逻辑系统 L,一个 L-抽象逻辑 A=⟨A,C⟩ 是 L 的一个模型,如果对于每个公式集合 Γ 和每个公式 ϕ,

Γ⊢Lϕ 当且仅当对于 A 上的每个估值 v,v(ϕ)∈C(v [Γ])。

这个定义在 C 的闭集合方面有一个等价物:一个抽象逻辑 A=⟨A,C⟩ 是 L 的一个模型,当且仅当对于每个 C-闭集合 X,矩阵 ⟨A,X⟩ 是 L 的一个模型(即 X 是一个 L-滤器)。

这个观察引导我们对抽象逻辑作为逻辑系统模型的另一种观点。它将它们转化为同一个代数上的一组逻辑矩阵(由闭集合给出),或者更简单地说,转化为一个对偶 ⟨A,B⟩,其中 B 是 A 的子集的集合。这种类型的结构在文献中被称为广义矩阵(Wójcicki 1973),最近被称为地图册(atlas)(Dunn&Hardegree 2001)。如果对于每个 X∈B,⟨A,X⟩ 是 L 的一个矩阵模型,则称其为逻辑系统 L 的一个模型。

逻辑系统 L=⟨L,⊢L⟩ 直接为我们提供了一个等价的抽象逻辑 ⟨FmL,C⊢L⟩ 和一个等价的广义矩阵 ⟨FmL,Th(L)⟩,其中 Th(L)是 C⊢L-闭公式集合(即 L-理论)。我们将自由地在两者之间转换。

对应于抽象逻辑的广义矩阵 ⟨A,B⟩ 具有以下两个特性:A∈B 且 B 在任意非空族的交集下是封闭的。具有这两个特性的子集族 B 被称为闭集系统,也被称为闭包系统。在集合 A 上,抽象推论操作与闭集系统之间存在对偶对应关系。给定集合 A 上的抽象推论操作 C,C-闭集的集合 CC 是一个闭集系统;给定闭集系统 C,对于每个 X⊆A,由 CC(X)=⋂{Y∈C:X⊆Y}定义的操作 CC 是一个抽象推论操作。一般来说,通过将 B∪{A}与任意非空子族的交集添加到一般化矩阵 ⟨A,B⟩ 中,可以将其转化为闭集系统,从而成为一个抽象逻辑,我们用 ⟨A,CB⟩ 表示。在这种情况下,我们说 B 是 CB 的一个基。显然,一个抽象逻辑可以有多个基。具有每个闭集是族中元素的交集的性质的闭集族是一个基。研究逻辑理论的闭集系统的基通常在其研究中起重要作用。例如,在经典逻辑中,其理论的一个重要基是最大一致理论的族,在直觉逻辑中,是素理论的族。类似地,对于逻辑的广义矩阵模型的基的系统研究变得重要。

为了使阐述流畅,我们现在将从抽象逻辑转向广义矩阵。设 A=⟨A,B⟩ 是一个广义矩阵。存在与 B 中所有集合兼容的最大同余关系;它被称为 A 的 Tarski 同余关系。我们用 Ω∼A(B)表示,并使用 Leibniz 算子对其进行以下刻画

Ω∼A(B)=⋂X∈BΩA(X)。

它还可以通过以下条件来描述:

⟨a,b⟩∈Ω∼A(B) 当且仅当对于每个 ϕ(p,q1,…,qn),每个 c1,…,cn∈A 和所有 X∈B

ϕA [a,c1,…,cn] ∈X⇔ϕA [b,c1,…,cn] ∈X

或等价地通过

⟨a,b⟩∈Ω∼A(B) 当且仅当对于每个 ϕ(p,q1,…,qn) 和每个 c1,…,cn∈A,CB(ϕA [a,c1,…,cn])=CB(ϕA [b,c1,…,cn])。

一个广义矩阵是简化的,如果它的塔斯基同余是恒等关系。每个广义矩阵 ⟨A,B⟩ 可以通过将其塔斯基同余关系相关的元素进行等价识别,转化为一个等价的简化矩阵。结果是商广义矩阵 ⟨A/Ω∼A(B),B/Ω∼A(B)⟩,其中 B/Ω∼A(B)={X/Ω∼A(B):X∈B},对于 X∈B,集合 X/Ω∼A(B) 是 X 元素的等价类的集合。

逻辑 L 的属性通常取决于其理论家族的整体行为,正如我们之前所说的。在某些逻辑中,这种行为体现在其定理集的行为中,例如经典逻辑和直觉主义逻辑由于演绎-分离性质,但这绝不是最一般的情况,正如正常模态逻辑 K 的局部和全局模态逻辑的例子所证明的那样。两者具有相同的定理,但不共享相同的属性。请记住,局部逻辑具有演绎-分离性质,而全局逻辑则没有。类似地,如果我们考虑代数上的 L-滤器家族,逻辑的属性通常在代数设置中更好地编码,而不是在逻辑矩阵模型理论中考虑单个 L-滤器。

在逻辑代数化研究中,自然吸引了最多关注的广义矩阵模型是形式为 ⟨A,FiLA⟩ 的广义矩阵,其中 FiLA 是 A 的所有 L-滤器的集合。在 L-代数的 L-滤器格结构中编码的逻辑属性的一个例子是,对于每个有限原代数逻辑 L,当且仅当对于每个代数 A,由 A 的所有 L-滤器组成的 L-滤器格的上界半格,即由有限生成的 L-滤器组成的上界半格是对偶可残余的;参见 Czelakowski 2001。

形式为 ⟨A,FiLA⟩ 的广义矩阵被称为 L 的基本全 g 模型(字母'g'代表广义矩阵)。对这些模型的兴趣导致了对具有以下特性的广义矩阵模型类的考虑:它们通过它们的塔斯基同余关系的商是一个基本全 g 模型。这些广义矩阵(及其对应的抽象逻辑)被称为全 g 模型。任意逻辑的全 g 模型理论在 Font&Jansana 1996 年得到发展,其中引入了全 g 模型和基本全 g 模型的概念。我们将提及其中的一些主要结果。

设 L 为逻辑系统。

  1. 当且仅当对于每个全 g 模型 ⟨A,C⟩,存在 A 的 L-滤子 F 使得 C={G∈FiLA:F⊆G},L 是原代数的。

  2. 如果 L 是有限的,那么当且仅当对于每个代数 A 和每个 L-滤子 F,广义矩阵 ⟨A,{G∈FiLA:F⊆G}⟩ 是一个完全的 g-模型且 AlgL 是一个拟变种。

  3. 类别 AlgL 既是 L 的简化广义矩阵模型的代数类别,也是{A:⟨A,FiLA⟩ 是简化的}的类别。

  4. 对于每个代数 A,存在一个同构,它将在 A 上的闭集系统 C(满足 ⟨A,C⟩ 是 L 的完全 g-模型)与在 A 上的同余 θ(满足 A/θ∈AlgL)的族相互映射。这个同构由 Tarski 算子给出,它将一个广义矩阵映射到它的 Tarski 同余。

上述的同构定理(4)是我们之前遇到的可代数逻辑的同构定理的一般化。有趣的是,该定理适用于每个逻辑系统。利用上述的(2),定理(4)蕴含了有限和有限可代数逻辑的同构定理。因此,定理(4)可以被看作是数学逻辑现象的最一般的表述,这些现象是同构定理在某个类别的代数的同余和它们的某种子集之间的存在,我们在第 9 节中提到过。

广义矩阵和抽象逻辑作为逻辑系统的模型的使用,对于自扩展逻辑的研究非常有用,特别是对于那些不是原代数的自扩展逻辑,比如在第 12 节中讨论的逻辑。特别是,它们对于具有合取的有限自扩展逻辑类和具有单个项(例如 p→q)的演绎-分离性质的有限自扩展逻辑类的研究非常有用;然而,这个最后一类逻辑仍然是原代数的。如果逻辑 L 有一个合取,那么存在一个双变量公式 ϕ(p,q),使得

ϕ(p,q)⊢Lp,ϕ(p,q)⊢Lq,p,q⊢Lϕ(p,q)。

这两个类中的逻辑具有以下特性:每个完全 g-模型 ⟨A,C⟩ 的 Tarski 关系为{⟨a,b⟩∈A×A:C(a)=C(b)}。一种说法是,对于这些逻辑,定义自扩展性的特性,即相互推导条件是一个同余,可以扩展到每个完全 g-模型。具有这种特性的自扩展逻辑被称为完全自扩展。这个概念是在 Font&Jansana 1996 年的论文中引入的,称为“强自扩展”。到 1996 年为止,所有自然的自扩展逻辑都是完全自扩展的,特别是在第 12 节中讨论的逻辑,但是 Babyonyshev(Babyonyshev 2003 年)展示了一个自扩展逻辑的特例,它不是完全自扩展的。后来发现的一个更自然的例子是只有否定和经典逻辑的常量 ⊤ 的自扩展逻辑,它也不是完全自扩展的。

关于完全自扩展逻辑的有合取或单个项具有演绎-分离性质的有限逻辑的一个有趣结果是它们的代数类 AlgL 总是一个变种。令人惊讶的是,许多有限和有限代数化逻辑的等价代数语义是一个变种,而代数化逻辑的理论通常只能证明有限和有限代数化逻辑的等价代数语义是一个准变种。该结果解释了适用于有限和有限代数化逻辑的这种现象。对于许多其他有限和有限代数化逻辑,找到令人信服的解释仍然是一个研究的开放领域。

每个抽象逻辑 A=⟨A,C⟩ 都确定了一个拟序(一个自反且传递的关系)在 A 上。它是由 a≤Ab 当且仅当 C(b)⊆C(a) 当且仅当 b∈C(a)定义的关系。

因此,当且仅当 b 属于 A 所属的每个 C-闭集合时,a≤Ab。对于一个完全自扩展的逻辑 L 来说,这个准序在简化的全 g-模型中变成了一个偏序,实际上就是简化的基本全 g-模型,即抽象逻辑 ⟨A,FiLA⟩,其中 A∈AlgL。因此,在完全自扩展的逻辑 L 中,每个代数 A∈AlgL 都具有一个可以用 L-滤器族来定义的偏序。如果逻辑是具有合取的完全自扩展的逻辑,那么这个偏序可以用 L-代数语言的方程来定义,因为在这种情况下,对于每个代数 A∈AlgL,我们有:a≤b 当且仅当 C(b)⊆C(a)当且仅当 C(a∧Ab)=C(a)当且仅当 a∧Ab=a,其中 C 是与闭集系统 FiLA 对应的抽象推论操作,∧A 是在 A 上由逻辑 L 的合取公式定义的操作。

对于具有单个项的完全自扩展逻辑(例如 p→q)具有演绎-分离性质,对于每个代数 A∈AlgL,类似的情况也成立。

a≤b 当且仅当 C(b)⊆C(a)当且仅当 C(a→Ab)=C(∅)=C(a→Aa)当且仅当 a→Ab=a→Aa。

这些观察使我们将具有合取的有限自扩展逻辑 L 和具有单个术语的演绎-分离属性的逻辑视为可以通过在 AlgL 中使用 L-代数语言的方程来定义的顺序可定义的逻辑。与此相关的是,已知以下结果。

定理 8。 具有合取的有限逻辑 L 是完全自扩展的,当且仅当存在一个代数类 K,对于每个 A∈K,其约化 ⟨A,∧A⟩ 是一个 meet 半格,如果 ≤ 是半格的顺序,那么

ϕ1,…,ϕn⊢Lϕ 当且仅当对于所有的 A∈K 和每个赋值 v 在 Av(ϕ1)∧A…∧Av(ϕn)≤v(ϕ)成立

并且

⊢Lϕ 当且仅当对于所有的 A∈K 和每个赋值 v 在 Aa≤v(ϕ)成立,对于每个 a∈A。

此外,在这种情况下,代数类 AlgL 是由 K 生成的变种。

类似的结果可以得到对于具有单个术语的推导-分离属性的自扩展逻辑。读者可以参考 Jansana 2006 对带有合取的自扩展逻辑的研究,以及 Jansana 2005 对具有单个术语的推导-分离属性的自扩展逻辑的研究。

具有合取的自扩展逻辑类包括在子结构逻辑和多值逻辑领域研究的所谓保持真实度的逻辑。读者可以参考 Bou et al. 2009 和其中的参考文献。

14. 弗雷格层次

在抽象代数逻辑中,考虑一种基于第 11 节讨论的替换原则而不是莱布尼茨同余行为的逻辑系统层次结构,称为弗雷格层次。它的类别包括自扩展逻辑、完全自扩展逻辑、弗雷格逻辑和完全弗雷格逻辑,我们现在来定义它们。

与完全自扩展逻辑类似,完全弗雷格逻辑是那些在它们的每一个全 g-模型中都满足定义自扩展性的特征性质的弗雷格逻辑。下面可以作为最易理解的定义。

当在逻辑系统 L 的每一个基本的完全 g-模型 ⟨A,FiLA⟩ 中,对于每个 F∈FiLA,Suszko 同余 Ω∼AL(F)与属于扩展 F 的 FiLA 的相同元素的关系相一致时,逻辑系统 L 是完全 Fregean 的。很容易看出,完全 Fregean 逻辑是 Fregean 逻辑,并且它们是完全自扩展的。

完全 Fregean 逻辑的例子包括经典逻辑和直觉主义逻辑,以及 12.1 节中讨论的合取和析取逻辑。之前提到的仅包含否定和真常量的经典逻辑片段是一个不完全 Fregean 的 Fregean 逻辑。

我们将读者引向 Font 2016a 的第 7 章,介绍 Frege 层次结构的主要事实和 Frege 层次结构中逻辑系统的例子。关于断言逻辑相关的 Frege 和 Leibniz 层次结构的讨论可以在 Albuquerque 等人的 2018 年的论文中找到,该论文还讨论和分类了几个逻辑系统的例子。

图。弗雷格层次

读者可以在阿尔布开尔基等人的 2017 年的论文中找到对莱布尼兹和弗雷格层次中分类的几个自然逻辑示例的讨论。

15. 扩展设置

在前几节中描述的逻辑系统研究已经扩展到包括超越命题逻辑的其他结果关系,例如等式逻辑和使用序列演算定义的命题语言的公式构建的序列之间的结果关系。感兴趣的读者可以参考优秀的论文 Raftery 2006a。

这项研究引发了对发展结果关系理论的更抽象方式的需求。它导致了逻辑系统理论的重新表述(在范畴论设置中),如本条目所解释的。这项工作主要由 G. Voutsadakis 在一系列论文中完成,例如 Voutsadakis 2002。Voutsadakis 的方法使用了由 Fiadeiro 和 Sernadas 引入的 pi-机构的概念,作为他范畴论设置中逻辑系统的类比。在 Gil-Férez 2006 中也可以找到一些相关工作。另一种推广逻辑系统和序列演算研究的方法可以在 Galatos&Tsinakis 2009 中找到;Gil-Férez 2011 也属于这一领域。这两篇论文中提出的工作源于 Blok&Jónsson 2006。Galatos-Tsinakis 的方法最近得到了扩展,以包括 Galatos&Gil-Férez 2017 中 Voutsadakis 的设置。

另一条最近的研究线路扩展了本条目中描述的框架,使用计算机科学中的行为等式结果(一种来自计算机科学的概念)代替自然类别的代数的等式结果关系,并且比可代数逻辑更弱:行为代数逻辑。请参阅 Caleiro,Gonçalves&Martins 2009。

Bibliography

  • Albuquerque, Hugo, Josep Maria Font, and Ramon Jansana, 2016, “Compatibility operators in abstract algebraic logic”, The Journal of Symbolic Logic, 81(2): 417–462. doi:10.1017/jsl.2015.39

  • –––, 2017, “The strong version of a sentential logic”, Studia Logica, 105: 703–760. doi: 10.1007/s11225-017-9709-0

  • Albuquerque, Hugo, Josep Maria Font, Ramon Jansana and Tommaso Moraschini, 2018, “Assertional logics, truth-equational logics and the hierarchies of abstract algebraic logic”, in Don Pigozzi on Abstract Algebraic Logic, Universal Algebra, and Computer Science (Outstanding Contributions to Logic: Volume 16), Janusz Czelakowski (ed.), Dordrecht: Springer: 53–79. doi: 10.1007/978-3-319-74772-9

  • Babyonyshev, Sergei V., 2003, “Strongly Fregean logics”, Reports on Mathematical Logic, 37: 59–77. [Babyonyshev 2003 available online]

  • Blackburn, Patrick, Johan van Benthem, and Frank Wolter (eds.), 2006, Handbook of Modal Logic, Amsterdam: Elsevier.

  • Blok, W.J. and Eva Hoogland, 2006, “The Beth property in algebraic logic”, Studia Logica (Special Issue in memory of Willem Johannes Blok), 83: 49–90. doi:10.1007/s11225-006-8298-0

  • Blok, W.J. and Bjarni Jónsson, 2006, “Equivalence of consequence operations”, Studia Logica, 83: 91–110. doi:10.1007/s11225-006-8299-z

  • Blok, W.J. and Don Pigozzi, 1986, “Protoalgebraic logics”, Studia Logica, 45(4): 337–369. doi:10.1007/BF00370269

  • –––, 1989, Algebraizable logics, (Mem. Amer. Math. Soc., Volume 396), Providence: A.M.S.

  • –––, 1991, “Local deduction theorems in algebraic logic”, in Algebraic Logic (Colloquia Mathematica Societatis János Bolyai: Volume 54), H. Andréka, J.D. Monk, and I. Németi (eds.), Amsterdam: North Holland, 75–109.

  • –––, 1992, “Algebraic semantics for universal Horn logic without equality”, in Universal Algebra and Quasigroup Theory, Anna B. Romanowska and Jonathan D.H. Smith (eds.). Berlin: Heldermann, 1–56.

  • Blok, W.J. and Jordi Rebagliato, 2003, “Algebraic semantics for deductive systems, ” Studia Logica, Special Issue on Abstract Algebraic Logic, Part II, 74(5): 153–180. doi:10.1023/A:1024626023417

  • Bloom, Stephen L., 1975, “Some theorems on structural consequence operations”, Studia Logica, 34(1): 1–9. doi:10.1007/BF02314419

  • Bou, Félix, Francesc Esteva, Josep Maria Font, Àngel J. Gil, Lluís Godo, Antoni Torrens, and Ventura Verdú, 2009, “Logics preserving degrees of truth from varieties of residuated lattices”, Journal of Logic and Computation, 19(6): 1031–1069. doi:10.1093/logcom/exp030

  • Brown, Donald J. and Roman Suszko, 1973, “Abstract logics”, Dissertationes Mathematicae: Rozprawy Matematyczne, 102: 9–42.

  • Caleiro, Carlos, Ricardo Gonçalves, and Manuel Martins, 2009, “Behavioral algebraization of logics”, Studia Logica, 91(1): 63–111. doi:10.1007/s11225-009-9163-8

  • Celani, Sergio and Ramon Jansana, 2003, “A closer look at some subintuitionistic logics”, Notre Dame Journal of Formal Logic, 42(4): 225–255. doi:10.1305/ndjfl/1063372244

  • –––, 2005, “Bounded distributive lattices with strict implication”, Mathematical Logic Quarterly, 51: 219–246. doi:10.1002/malq.200410022

  • Cintula, Petr and Carles Noguera, 2010 “Implicational (semilinear) logics I: a new hierarchy”, Archive for Mathematical Logic, 49(4): 417–446. doi:10.1007/s00153-010-0178-7

  • –––, 2016 “Implicational (semilinear) logics II: additional connectives and characterizations of semilinearity”, Archive for Mathematical Logic, 55(3): 353–372. doi:10.1007/s00153-015-0452-9

  • –––, 2021 Logic and Implication. An Introduction to the General Algebraic Study of Non-classical Logics (Trends in Logic: Volume 51), Cham: Springer.

  • Czelakowski, Janusz, 1980, “Reduced products of logical matrices”, Studia Logica, 39(1): 19–43. doi:10.1007/BF00373095

  • –––, 1981, “Equivalential logics, I and II”, Studia Logica, 40(3): 227–236 and 40(4): 355–372. doi:10.1007/BF02584057 and doi:10.1007/BF00401654

  • –––, 2001, Protoalgebraic Logics (Trends in Logic, Studia Logica Library, Volume 10), Dordrecht: Kluwer Academic Publishers.

  • –––, 2003, “The Suszko operator. Part I”, Studia Logica, 74(1): 181–231. doi:10.1023/A:1024678007488

  • Czelakowski, Janusz and Ramon Jansana, 2000, “Weakly algebraizable logics”, The Journal of Symbolic Logic, 65(2): 641–668. doi:10.2307/2586559

  • Czelakowski, Janusz and Don Pigozzi, 2004a, “Fregean logics”, Annals of Pure and Applied Logic, 127: 17–76. doi:10.1016/j.apal.2003.11.008

  • –––, 2004b, “Fregean logics with the multiterm deduction theorem and their algebraization”, Studia Logica, 78: 171–212. doi:10.1007/s11225-005-1212-3

  • Dunn, J. Michael, 1995, “Positive Modal Logic”, Studia Logica, 55(2): 301–317. doi:10.1007/BF01061239

  • Dunn, J. Michael and Gary M. Hardegree, 2001, Algebraic methods in philosophical logic (Oxford Logic Guides, Oxford Science Publications, Volume 41), New York: Oxford University Press.

  • Font, Josep Maria, 1997, “Belnap’s four-valued logic and De Morgan lattices”, Logic Journal of the I.G.P.L, 5: 413–440.

  • –––, 2016, Abstract Algebraic Logic. An Introductory Textbook, volume 60 of Studies in Logic, London: College Publications.

  • –––, 2022, “Abstract Algebraic Logic.”, in Hiroakira Ono on Residuated Lattices and Substructural Logics, Nikolaos Galatos and K. Terui (eds), series Outstanding Contributions to Logic 23, Springer. 72pp. doi: 10.1007/978-3-030-76920-8

  • Font, Josep Maria and Ramon Jansana, 1996, A general algebraic semantics for sentential logics (Lecture Notes in Logic: Volume 7), Dordrecht: Springer; 2nd revised edition, Cambridge: Cambridge University Press, 2016 (for the Association for Symbolic Logic).

  • Font, Josep Maria, Ramon Jansana, and Don Pigozzi 2003, “A Survey of Abstract Algebraic Logic”, Studia Logica, 74 (Special Issue on Abstract Algebraic Logic—Part II): 13–97. doi:10.1023/A:1024621922509

  • Font, Josep Maria and Gonzalo Rodríguez, 1990, “Note on algebraic models for relevance logic”, Mathematical Logic Quarterly, 36(6): 535–540. doi:10.1002/malq.19900360606

  • –––, 1994, “Algebraic study of two deductive systems of relevance logic”, Notre Dame Journal of Formal Logic, 35: 369–397. doi:10.1305/ndjfl/1040511344

  • Font, Josep Maria and V. Verdú, 1991, “Algebraic logic for classical conjunction and disjunction”, Studia Logica, 65 (Special Issue on Abstract Algebraic Logic): 391–419. doi:10.1007/BF01053070

  • Galatos, Nikolaos and Constantine Tsinakis, 2009, “Equivalence of consequence relations: an order-theoretic and categorical perspective”, The Journal of Symbolic Logic, 74(3): 780–810. doi:10.2178/jsl/1245158085

  • Galatos, Nikolaos and José Gil-Férez, 2017, “Modules over quataloids: Applications to the isomorphism problem in algebraic logic and π-institutions”, Journal of Pure and Applied Algebra, 221(1): 1–24. doi:10.1016/j.jpaa.2016.05.012

  • Gil-Férez, José, 2006, “Multi-term π-institutions and their equivalence”, Mathematical Logic Quarterly, 52(5): 505–526. doi:10.1002/malq.200610010

  • –––, 2011, “Representations of structural closure operators”, Archive for Mathematical Logic, 50:45–73. doi:10.1007/s00153-010-0201-z

  • Herrmann, Bughard, 1996, “Equivalential and algebraizable logics”, Studia Logica, 57(2): 419–436. doi:10.1007/BF00370843

  • –––, 1997, “Characterizing equivalential and algebraizable logics by the Leibniz operator”, Studia Logica, 58(2): 305–323. doi:10.1023/A:1004979825733

  • Heyting, Arend, 1930, “Die formalen Reglen der Intuitionionischen Logik” (in 3 parts), Sitzungsberichte der preussischen Akademie von Wissenschaften, 42–56, 57–71, 158–169.

  • Hoogland, Eva, 2000, “Algebraic characterizations of various Beth definability properties”, Studia Logica, 65 (Special Issue on Abstract Algebraic Logic. Part I): 91–112. doi:10.1023/A:1005295109904

  • Humberstone, Lloyd, 2005, “Logical Discrimination”, in J.-Y. Béziau (ed.), Logica Universalis, Basel: Birkhäuser. doi:10.1007/3-7643-7304-0_12

  • Jansana, Ramon, 2002, “Full models for positive modal logic”, Mathematical Logic Quarterly, 48(3): 427–445. doi:10.1002/1521-3870(200204)48:3<427::AID-MALQ427>3.0.CO;2-T

  • –––, 2005, “Selfextensional logics with implication”, in J.-Y. Béziau (ed.), Logica Universalis, Basel: Birkhäuser. doi:10.1007/3-7643-7304-0_4

  • –––, 2006, “Selfextensional logics with conjunction”, Studia Logica, 84(1): 63–104. doi:10.1007/s11225-006-9003-z

  • Jansana, Ramon and Alessandra Palmigiano, 2006, “Referential algebras: duality and applications”, Reports on Mathematical Logic (Special issue in memory of Willem Blok), 41: 63–93. [Jansana and Palmigiano 2006 available online]

  • Koslow, Arnold, 1992, A structuralist theory of logic, Cambridge: Cambridge University Press. doi:10.1017/CBO9780511609206

  • Kracht, Marcus, 2006, “Modal Consequence Relations”, in Blackburn, van Benthem, and Wolter 2006: 497–549.

  • Lávička, Tomáš, Tommaso Moraschini and James Raftery, 2021, “The algebraic significance of weak excluded middle laws”, Mathematical Logic Quarterly, 68(1): 79–94.

  • Lewis, Clarence Irving, 1918, A Survey of Symbolic Logic, Berkeley: University of California Press; second edition, New York Dover Publications, 1960.

  • Lewis, Clarence Irving and Langford, Cooper H., 1932 Symbolic Logic, second edition, New York: Dover Publications, 1959.

  • Łoś, Jerzy, 1949, O matrycach logicznych, Ser. B. Prace Wrocławskiego Towarzystwa Naukowege (Travaux de la Société et des Lettres de Wrocław), Volume 19.

  • Łoś, Jerzy and Roman Suszko, 1958, “Remarks on sentential logics”, Indagationes Mathematicae (Proceedings), 61: 177–183. doi:10.1016/S1385-7258(58)50024-9

  • Łukasiewicz, J. and Alfred Tarski, 1930, “Untersuchungen über den Aussagenkalkül”, Comptes Rendus des Séances de la Société des Sciences et des Lettres de Varsovie, Cl.III 23: 30–50. English translation in Tarski 1983: “Investigations into the sentential calculus”.

  • Malinowski, Jacek, 1990, “The deduction theorem for quantum logic, some negative results”, The Journal of Symbolic Logic, 55(2): 615–625. doi:10.2307/2274651

  • McKinsey, J.C.C., 1941, “A solution of the decision problem for the Lewis systems S2 and S4, with an application to topology”, The Journal of Symbolic Logic, 6(4): 117–134. doi:10.2307/2267105

  • McKinsey, J.C.C. and Alfred Tarski, 1948, “Some theorems about the sentential calculi of Lewis and Heyting”, The Journal of Symbolic Logic, 13(1): 1–15. doi:10.2307/2268135

  • Moraschini, T., forthcoming, “On equational completeness theorems ”, The Journal of Symbolic Logic, first online 13 September 2021. doi:10.1017/jsl.2021.67

  • Pigozzi, Don, 1991, “Fregean algebraic logic”, in H. Andréka, J.D. Monk, and I. Németi (eds.), Algebraic Logic (Colloq. Math. Soc. János Bolyai, Volume 54), Amsterdam: North-Holland, 473-502.

  • Prucnal, Tadeusz and Andrzej Wroński, 1974, “An algebraic characterization of the notion of structural completeness”, Bulletin of the Section of Logic, 3(1): 30–33.

  • Raftery, James G., 2006a, “Correspondence between Gentzen and Hilbert systems”, The Journal of Symbolic Logic, 71(3): 903–957. doi:10.2178/jsl/1154698583

  • –––, 2006b, “On the equational definability of truth predicates”, Reports on Mathematical Logic (Special issue in memory of Willem Blok), 41: 95–149. [Raftery 2006b available online]

  • –––, 2011, “Contextual deduction theorems”, Studia Logica (Special issue in honor of Ryszard Wójcicki), 99: 279–319. doi:10.1007/s11225-011-9353-z

  • –––, 2013, “Inconsistency lemmas in algebraic logic”, Mathematical Logic Quarterly, 59(6): 393–406. doi:10.1002/malq.201200020

  • –––, 2016, “Admissible rules and the Leibniz Hierarchy”, Notre Dame Journal of Formal Logic, 57: 569–606.

  • Rasiowa, H., 1974, An algebraic approach to non-classical logics (Studies in Logic and the Foundations of Mathematics, Volume 78), Amsterdam: North-Holland.

  • Schroeder-Heister, Peter and Kosta Dośen (eds), 1993, Substructural Logics (Studies in Logic and Computation: Volume 2), Oxford: Oxford University Press.

  • Suszko, Roman, 1977, “Congruences in sentential calculus”, in A report from the Autumn School of Logic (Miedzygorze, Poland, November 21–29, 1977). Mimeographed notes, edited and compiled by J. Zygmunt and G. Malinowski. Restricted distribution.

  • Tarski, Alfred, 1930a, “Über einige fundamentale Begriffe der Metamathematik”, C. R. Soc. Sci. Lettr. Varsovie, Cl. III 23: 22–29. English translation in Tarski 1983: “On some fundamental concepts of metamathematics”, 30–37.

  • –––, 1930b, “Fundamentale Begriffe der Methodologie der deduktiven Wissenschaften I”, Monatfshefte für Mathematik und Physik, 37: 361–404. English translation in Tarski 1983: “Fundamental concepts of the methodology of the deductive sciences”, 60–109.

  • –––, 1935, “Grundzüge der Systemenkalküls. Erster Teil”, Fundamenta Mathematicae, 25: 503–526, 1935. English translation in Tarski 1983: “Foundations of the calculus of systems”, 342–383.

  • –––, 1936, “Grundzüge der Systemenkalküls. Zweiter Teil”, Fundamenta Mathematicae, 26: 283–301, 1936. English translation in Tarski 1983: “Foundations of the calculus of systems”, 342–383.

  • –––, 1983, Logic, Semantics, Metamathematics. Papers from 1923 to 1938, J. Corcoran (ed.), Indianapolis: Hackett, second edition.

  • Torrens, Antoni, 2008, “An Approach to Glivenko’s Theorems in Algebraizable Logics”, Studia Logica, 88(3): 349–383. doi:10.1007/s11225-008-9109-6

  • Troelstra, A.S., 1992, Lectures on Linear Logic (CSLI Lecture Notes 29), Stanford, CA: CSLI Publications.

  • Visser, Albert, 1981, “A Propositional Logic with Explicit Fixed Points”, Studia Logica, 40(2): 155–175. A Propositional Logic with Explicit Fixed Points

  • Voutsadakis, George, 2002, “Categorical Abstract Algebraic Logic: Algebraizable Institutions”, Applied Categorical Structures, 10: 531–568. doi:10.1023/A:1020990419514

  • Wójcicki, Ryszard, 1969, “Logical matrices strongly adequate for structural sentential calculi”, Bulletin de l’Académie Polonaise des Sciences, Classe III XVII: 333–335.

  • –––, 1973, “Matrix approach in the methodology of sentential calculi”, Studia Logica, 32(1): 7–37. doi:10.1007/BF02123806

  • –––, 1988, Theory of logical calculi. Basic theory of consequence operations (Synthese Library, Volum 199), Dordrecht: D. Reidel.

Academic Tools

Other Internet Resources

algebra | Boole, George | Boolean algebra: the mathematics of | logic: classical | logic: intuitionistic | logic: linear | logic: many-valued | logic: modal | logic: relevance | logical consequence | model theory: first-order | Tarski, Alfred

Copyright © 2022 by Ramon Jansana <jansana@ub.edu>

最后更新于

Logo

道长哲学研讨会 2024