1. 抽象后果关系
2. 作为结果关系的逻辑
3. 一些逻辑示例
3.1 经典命题逻辑
3.2 直觉命题逻辑
3.3 局部正规模态逻辑
3.4 全局正态模态逻辑
3.5 没有指数的直觉线性逻辑
3.6 关联逻辑系统R
4.代数
4.1 泛代数和模型论的一些概念
4.2 品种和准品种
5. 代数语义
6. 逻辑矩阵
7. 证明代数完备性定理的 Lindenbaum-Tarski 方法
8.逻辑系统的代数自然类
9. 当一个逻辑是可代数的时,这意味着什么?
10.逻辑的分类
11. 更换原则
12. 超越原代数逻辑
12.1 合取与析取的逻辑
12.2 正模态逻辑
12.3 维瑟的亚直觉逻辑
12.4 局部模态逻辑lK的严格蕴涵片段
13.抽象逻辑和广义矩阵
14.弗雷格层次结构
15. 扩展设置
参考书目
学术工具
其他互联网资源
相关条目
1. 抽象后果关系
塔斯基关于20世纪20年代和1930年代演绎科学方法论的著作(1930a、1930b、1935、1936)对公理化方法进行了抽象研究,并首次引入了结果运算的抽象概念。塔斯基主要考虑的是不同的数学公理理论。在这些理论中,从公理证明的句子是它们的结果,但(当然)几乎所有的句子都不是逻辑真理;在这些理论的适当形式化下,可以使用像弗雷格或罗素这样的逻辑演算来推导公理的结果。塔斯基设置了一个框架来研究将其结果分配给一组公理的运算的最一般属性。
给定逻辑演绎系统H和任意一组公式X,如果存在有限公式序列,其中任何一个属于X或是H的公理或从先前的公式获得,则公式a可以在H中从X推出在序列中通过 H 的推理规则之一。这样的序列是 H 中对 X 中的前提或假设的 a 的演绎(或证明)。设 Cn(X) 是 H 中可从公式推导的公式集以 X 为前提或假设。这个集合称为X的后果集合(相对于逻辑演绎系统H)。 Cn 是一种应用于公式集以获得新公式集的运算。它具有以下性质: 对于每组公式 X
X⊆Cn(X)
Cn(Cn(X))=Cn(X)
Cn(X)=⋃{Cn(Y):Y⊆X,Y 有限}
第三个条件规定 Cn(X) 等于可从 X 的有限子集导出的公式集的并集。塔斯基利用这些性质以公理方式定义了结果运算的概念。事实上,他补充说,存在一个公式 x,使得 Cn({x}) 是所有公式的集合 A,并且该集合必须是有限的或者是自然数集合的基数。条件 (3) 意味着较弱但重要的单调性条件
如果 X⊆Y⊆A,则 Cn(X)⊆Cn(Y)。
为了涵盖文献中发现的一整类逻辑系统,需要一个比塔斯基的定义稍微更一般的定义。我们可以说,对任意集合 A 的抽象结果运算 C 是应用于 A 的子集的运算,给出 A 的子集,并且对于所有 X,Y⊆A 满足上述条件 (1)、(2) 和 (4) 。另外,如果 C 满足 (3),我们就说它是有限结果运算。
结果运算不仅存在于逻辑中,而且存在于数学的许多领域。例如,抽象结果运算在普适代数和格论中被称为闭包算子。在拓扑中,将拓扑空间的子集发送到其拓扑闭包的操作是闭包算子。事实上,集合 A 上的拓扑可以用 A 上的闭包算子来标识,满足附加条件:对于所有 X,C(∅)=∅ 和 C(X∪Y)=C(X)∪C(Y) ,Y⊆A。
给定集合 A 上的结果运算 C,如果 C(X)=X,则 A 的子集 X 被称为 C 闭集,或 C 的闭集。
一种不同但在数学上等效的(形式)方法是考虑一组公式的结果关系而不是结果运算。形式语言的公式集上的 A(n)(抽象)结果关系是满足以下条件的公式集和公式之间的关系 ⊢:
如果 a∈X,则 X⊢a
如果 X⊢a 且 X⊆Y,则 Y⊢a
如果 X⊢a 并且对于每个 b∈X,Y⊢b,则 Y⊢a。
它是有限的,如果此外还满足
如果 X⊢a,则存在有限集 Y⊆X,使得 Y⊢a。
给定一个逻辑演绎系统 H,如果 a 可从 H 中的 X 推出,则由 X⊢a 定义的关系 ⊢ 是(根据我们已经看到的)有限结果关系。尽管如此,我们不仅习惯于结果关系的句法定义,而且还习惯于语义定义。例如,我们使用真值评估来定义经典命题推论,使用结构来定义一阶推论关系,使用克里普克模型来定义直觉推论关系等。有时,这些推论关系的模型理论定义定义了非有限推论关系,例如,推论无限形式语言的关系以及二阶逻辑与所谓标准语义的结果关系。
一般来说,集合 A(不一定是某种形式语言的公式集)上的抽象结果关系是 A 的子集与 A 的元素之间满足上述条件 (1)–(3) 的关系 ⊢ 。如果它也满足(4),则称其是有限的。如果 ⊢ 是一个抽象结果关系,并且 X⊢a,那么我们可以说 X 是一组前提或假设,根据 ⊢ 有结论 a,并且 a 由 X 推出,或者被 X 蕴涵(根据 ⊢)。抽象的后果关系对应于科斯洛的蕴涵结构;请参阅 Koslow 1992,了解该作者引入的密切相关但不同的逻辑方法(广义上)作为结果关系。
集合 A 上的结果操作与 A 上的抽象结果关系一一对应。从结果操作 C 到结果关系 ⊢C 的移动,反之,从结果关系 ⊢ 到结果操作 C ⊢ 很简单,由定义给出:
X⊢Ca 当且仅当 a∈C(X) 且 a∈C⊢(X) 当且仅当 X⊢a。
此外,如果 C 是有限的,则 ⊢C 也是有限的,如果 ⊢ 是有限的,那么 C⊢ 也是有限的。
有关逻辑结果的一般讨论,请参阅逻辑结果条目。
2. 作为结果关系的逻辑
在本节中,我们定义什么是命题逻辑并解释与其相关的基本概念。我们将命题逻辑(如下定义)简称为逻辑系统。
我们在逻辑中研究的结果关系的主要特征之一是它们的形式特征。这大致意味着,如果一个句子 a 来自一组句子 X,并且我们有另一个句子 b 和另一组句子 Y 分别与 a 和 X 共享相同的形式,那么 b 也来自 Y。在命题逻辑中,这就是沸腾可以说,如果我们将 X∪{a} 中句子的基本子句统一替换为其他句子,得到 Y 和 b,则从 Y 得出 b。(读者可以在条目中找到更多关于形式化思想的信息)逻辑后果。)
为了将逻辑的形式特征的想法转化为严格的定义,我们需要引入命题语言的概念和替代的概念。
命题语言(简称语言)L是一组连接词,即一组符号,每个符号都有一个元数n,它告诉我们在n=0的情况下该符号是一个命题常数,并且如果 n>0 连接词是一元、二元、三元等。例如 {∧,∨,→,⊥,⊤} 是(或可以是)多种逻辑的语言,例如经典逻辑和直觉的,(⊥和⊤是0元,其他连接词是二元),{Ø,∧,∨→,◻,◊}是几种模态逻辑的语言,(Ø,◻,◊是一元,其他连接词二进制)和 {∧,∨,→,*,⊤,⊥,1,0} 是多值逻辑的语言,也是线性逻辑片段(⊥、⊤、1 和 0 是命题常数,其他符号是二元连接词)。
给定语言 L 和一组命题变量 V(与 L 不相交),L 的公式或 L 公式归纳定义如下:
每个变量都是一个公式。
每个 0 元符号都是一个公式。
如果 ∗ 是一个联结词,并且 n>0 是它的元数,那么对于所有公式 ψ1,…,ψn,∗ψ1…ψn 也是一个公式。
L 的替换 σ 是从变量集 V 到 L 的公式集的映射。它告诉我们在执行替换时哪个公式必须替换哪个变量。如果 p 是变量,则 σ(p) 表示代入 σ 赋予 p 的公式。将 σ 应用于公式 phi 的结果是通过同时分别用公式 σ(p1),...,σ 替换 phi 中的变量(例如 p1,...,pk),从 phi 获得公式 σ(phi) (PK)。这样,替换 σ 给出了从公式集到自身的唯一映射 σ,满足
σ(p)=σ(p),对于每个变量 p,
σ(†)=†,对于每个 0 元连接词 †,
σ(*φ1…φn)=*σ(φ1)…σ(φn),对于每个元数 n>0 的连接词 * 和公式 φ1,…,φn。
如果存在替换 σ,使得当应用于 ψ 时给出 ψ,即如果 σ(ψ)=ψ,则公式 ψ 是公式 ψ 的替换实例。
为了避免不必要的复杂化,我们在下文中假设所有逻辑都使用相同的变量可数集V,因此L的公式的定义仅取决于L。逻辑系统(或简称逻辑)由下式给出语言 L 和 L 的公式集上的结果关系 ⊢ 是形式化的,即对于每个替换 σ,每组公式 Γ 和每个公式 phi,
若 Г⊢ , 则 σ[Т]⊢σ(Г)
其中 σ[Г] 是通过将 σ 代入 Г 中的公式而获得的公式集。满足该属性的语言公式集上的结果关系在文献中被称为结构性的并且也是替换不变的。 1958 年,Łoś & Suszko 首次考虑了它们。Tarski 仅明确考虑闭集在某些结果关系的替换实例下也是封闭的;他从未考虑过(至少明确地)后果关系的替代不变性条件。
我们将用字母 L 和可能的子索引来指代逻辑系统,并且我们设置 L=⟨L,⊢L⟩ 和 Ln=⟨Ln,⊢Ln⟩,并理解 L(Ln) 是 L(Ln) 的语言和 ⊢L(⊢Ln) 其后果关系。如果 ⊢L 是有限结果关系,则逻辑系统 L 是有限的。
逻辑系统的结果关系可以通过多种方式给出,一些使用证明理论工具,另一些使用语义手段。替代不变结果关系可以使用希尔伯特式公理系统、Gentzen 式序列演算或自然演绎式演算等证明系统来定义。人们还可以使用类在语义上定义替代不变结果关系数学对象(代数、克里普克模型、拓扑模型等)和满足关系。
如果 L1=⟨L,⊢L1⟩ 是一个逻辑系统,⊢L1 由证明系统定义,并且 L2=⟨L,⊢L2⟩ 是同一语言上的逻辑系统,⊢L2 在语义上定义,我们说证明- 用于定义 ⊢L1 的系统对于用于定义 ⊢L2 的语义是合理的,如果 ⊢L1 包含在⊢L2,即如果 Т⊢L1 蕴含 Т⊢L2 Ф。如果另一个包含成立,则证明系统就定义 ⊢L2 的语义而言被认为是完整的,即当 Γ⊢L2phi 蕴含 Γ⊢L1phi 时。
一组 L-公式 Γ 被称为逻辑系统 L 的理论,或 L-理论,如果它在关系 ⊢L 下是闭的,也就是说,如果每当 Γ⊢L phi 时它也满足 phi ∈ Γ。换句话说,L 的理论是 L 公式集上结果运算 C⊢L 的闭集。为了简化符号,我们用 CL 来表示这个结果运算。公式 phi 是 L if ∅⊢Lphi 的定理(或有效性)。那么CL(∅)是L的定理集合,是L的最小理论。L的所有理论的集合用Th(L)表示。
给定一个逻辑系统 L,结果运算 CL 是替换不变的,这意味着对于每组 L-公式 Γ 和每个替换 σ,σ[CL(Γ)]⊆CL(σ[Γ])。此外,对于 L 的每个理论 T,我们都有一个新的结果 C
时间
L
操作定义如下:
C
时间
L
( ) = CL(T ∪ )
即C
时间
L
(Г) 是根据 L 从 Г 和 T 得出的公式集。事实证明,T 在替换下是封闭的当且仅当 C
时间
L
是替换不变的。
如果 L 是一个逻辑系统,并且 Γ,Δ 是 L 公式的集合,我们将使用符号 Γ⊢LΔ 来表示对于每个 ψ∈Δ,Γ⊢Lψ。因此 Γ⊢LΔ 当且仅当 Δ⊆CL(Γ)。
如果 L=⟨L,⊢L⟩ 且 L′=⟨L′,⊢L′⟩ 是逻辑系统,其语言满足 L′⊆L(因此所有 L′-公式都是 L-公式)并且
Г⊢L′phi 当且仅当 Г⊢Lψ,
对于每组 L'-公式 Γ 和每个 L'-公式 ψ,我们说 L' 是片段 L(实际上是 L'-片段),并且 L 是 L' 的扩展。
3. 一些逻辑示例
我们提供了一些逻辑系统的例子,我们将在本文中提到这些例子,为了方便读者,我们将这些例子聚集在这里。只要有可能,我们都会参考相应的条目。
对于二元连接词,我们使用标准约定写作 (ψ*ψ) 而不是 *ψψ,并省略公式中的外括号。
3.1 经典命题逻辑
我们将经典命题逻辑CPL的语言视为集合Lc={∧,∨,→,⊤,⊥},其中∧,∨,→是二元联结词,⊤,⊥命题常数。我们假设结果关系由通常的真值表方法定义(⊤ 解释为 true,⊥ 解释为 false)如下,
Γ⊢CPLphi 当且仅当为所有 ψ ε 分配 true 的每个真值评估都将 true 分配给 phi。
满足 ∅⊢CPLphi 的公式 phi 是同义反复。请注意,使用语言 Lc,公式 ψ 的否定被定义为 ψ→⊥。有关更多信息,请参阅经典逻辑条目。
3.2 直觉命题逻辑
我们将直觉命题逻辑的语言与经典命题逻辑的语言相同,即集合{∧,∨,→,⊤,⊥}。结果关系由以下希尔伯特式演算定义。
公理:
所有表格的公式
C0。
⊤C1. Φ→(ψ→Φ)C2。
ψ→(ψ→(ψ∧ψ))C3。
(ψ∧ψ)→ψC4。
(ψ∧ψ)→ψ
C5。
ψ→(ψ∨ψ)C6。
ψ→(ψ∨ψ)C7。
(ψ∨ψ)→((ψ→δ)→((ψ→δ)→δ))C8。
(ψ→ψ)→((ψ→(ψ→δ))→(ψ→δ))C9。
⊥→Φ
推理规则
ψ,ψ→ψ/ψ
有关更多信息,请参阅直觉逻辑条目。
3.3 局部正规模态逻辑
我们这里考虑的模态逻辑语言是集合 Lm={∧,∨,→,Ø,◻,⊤,⊥},它通过添加一元连接词 ◻ 来扩展 Lc。在模态逻辑的标准文献中,正规模态逻辑不是被定义为结果关系,而是被定义为具有某些属性的一组公式。正规模态逻辑是 Lm 公式的集合 Λ,其中包含经典逻辑语言的所有同义反复,形式为
◻(ψ→ψ)→(◻ψ→◻ψ)
并根据规则关闭
ψ,ψ→ψ/ψ
φ/◻φ
ψ/σ(ψ),对于每个替换 σ
请注意,集合 Λ 在替换实例下是封闭的,即对于每个替换 σ,如果 ψ ∈ Lm,则 σ(ψ) ∈ Lm。
最不正规的模态逻辑称为 K,可以通过希尔伯特式微积分公理化,其中包含公理、经典逻辑的同义反复和公式 ◻(ψ→ψ)→(◻ψ→◻ψ),以及推理规则 Modus Ponens和模态泛化。请注意,由于我们在公理的表示中使用模式,因此可导公式集在替换规则下是封闭的。
与正常模态逻辑 Λ 相关联的是由微积分定义的结果关系,该微积分将 Λ 中的所有公式作为公理,并作为推理 Modus Ponens 的唯一规则。这种结果关系给出的逻辑系统称为Λ的局部结果。我们用 lΛ 表示它。它的定理是 Λ 的元素并且它认为
Γ⊢lΛphi 当且仅当 phi∈Λ 或存在 phi1,…,phin∈Γ 使得 (phi1∧…∧phin)→phi∈Λ。
3.4 全局正态模态逻辑
另一个结果关系自然地与每个正常模态逻辑 Λ 相关联,由具有 Λ 公式作为公理和推理 Modus Ponens 和模态概括规则的微积分定义。这种结果关系给出的逻辑系统称为Λ的全局结果,用gΛ表示。它与局部 lΛ 有相同的定理,即 Λ 的元素。 lΛ 和 gΛ 之间的区别在于它们允许从非空前提集中得出的结果。例如,我们有 p⊢gK◻p 但 p⊬lK◻p。这种差异对它们的代数行为有巨大影响。
有关模态逻辑的更多信息,请参阅模态逻辑条目。读者可以在 Kracht 2006 中找到关于作为结果关系的模态逻辑的具体信息。
数学联邦政治世界观提示您:看后求收藏(笔尖小说网http://www.bjxsw.cc),接着再看更方便。