代数命题逻辑

George Boole是第一个在代数风格中作为数学理论呈现逻辑。 在他的工作中，在十九世纪逻辑的代数传统中，正式语言与数学上严谨的语义之间的区别仍未绘制。 这种传统中的代数所做的是建立代数理论（布尔代数和关系代数），其中在其他解释中是一个逻辑的理论。

Frege和Russell的作品在接近逻辑的路上引入了不同的视角。 在这些作品中，逻辑系统由正式语言和演绎微积分给出，即一组公理和一组推理规则。 让我们（对于此条目）呼叫这样的一对逻辑扣除系统，并且在其定理中衍生的公式（如今，代数逻辑中的常见做法是指Hilbert风格和证明的这种类型的计算复杂性理论作为弗赖特系统）。 在Frege和Russell的方法中，缺乏他们使用的正式语言的形式（数学）语义（代数，模型等）。 目前唯一的语义是一种直观的，非正式的。

由Frege和Russell引入的系统是古典逻辑系统，但在其他逻辑学家考虑了非古典逻辑系统后不久。 引入不同于经典逻辑的逻辑的第一个有影响力的尝试仍然是在没有任何形式语义的情况下呈现逻辑扣除系统的弗雷克罗塞尔传统。 这些尝试导致C.I的第一个模态系统。 Lewis（1918,1932）通过Heyting（1930）和直觉逻辑的公理化。

弗雷格和罗素的逻辑推导系统设计的潜在的想法是定理应该是（直观）到逻辑真理或逻辑有效性的公式。 逻辑后果的概念并不是发展的核心，这也是在C.I的第一个模态系统的脚步之后设计的许多非古典逻辑系统。 刘易斯。 这种情况影响了通常呈现了对某些非古典逻辑的研究的方式，有时也是它的真实演变。 然而，逻辑后果的概念是逻辑传统上处理的概念。 Tarski将其再次进入现代逻辑的中心，两种语义和句法。 如今，逻辑逻辑概念的逻辑代数的一般理论从上世纪中获得的不同逻辑的不同代数治疗生长。

逻辑后果的概念已经证明比定理和发展这种一般理论的发展的逻辑有效性更加富有成效。 建立逻辑代数的一般理论过程中的第一次尝试可以在Rasiowa（1974）的潜在逻辑研究中找到，并在Wójcicki（1988）的系统演示中找到在二十世纪的第一部分研究Tarski，Lindenbaum，Łukasiewicz和其他人之后，主要由波兰逻辑学家为主要是波兰逻辑学家进行了致命性逻辑的研究。

它仅在20世纪20年代，代数和逻辑矩阵（与一组指定元素一起的代数）开始被视为逻辑推导系统的模型，即提供正式语言的正式语言。 此外，它们还用于定义具有与已知逻辑推导系统的定理的相似性质的相似性，特别是在替换实例下关闭的性质; 在逻辑矩阵之后也很快用来将逻辑定义为后果关系。

可以以非常一般的术语描述代数逻辑作为研究逻辑通过将它们的代数，逻辑矩阵类和其他代数相关数学结构相关的逻辑以及与逻辑可能具有属性的属性来研究逻辑相关代数（或代数相关的结构），目的是对这些代数的理解可用于更好地理解手头的逻辑。

从特定逻辑的代数研究，在上个世纪慢慢出现了逻辑的代数的一般理论，目的是在过程中或多或少明确说明，获取与逻辑的属性相关的一般和信息结果可能具有代数属性与它可能享受的代数（或与代数相关结构）的类别。 这些代数研究假定了一个隐含的概念，该过程是将与任何给定的逻辑一类代数作为其天然代数对应的过程相关联的过程。 在20世纪80年代初开始发展该一般理论随着代数宗旨的概念而巩固，并在此时的概念也是关于作为自然的代数类别的假设给定的逻辑开始越来越明确。

在此进入中，我们专注于作为后果关系所采取命题逻辑的代数的一般理论。 该理论已经进化到称为抽象代数逻辑（AAL）的领域。 该条目可以作为对此字段的温和介绍。

抽象关系

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 visser的子管逻辑

12.4本地模态逻辑LK的严格含义片段

13.抽象逻辑和广义矩阵

14.弗雷格层次结构

15.延长设置

参考书目

学术工具

其他互联网资源

相关条目

抽象关系

Tarski的工作（1930A，1930B，1935,1936）关于20世纪20年代和20世纪30年代的演绎科学的方法，抽象地研究了公理方法，并首次引入了后果操作的抽象概念。 Tarski主要考虑到不同的数学公理理论。 在这些理论上，从公理证明的句子是它们的后果，但（当然）几乎所有这些都不是逻辑的真理; 在这些理论的适当形式化下，可以使用像Frege或Russell等逻辑计算来导出公理的后果。 tarski设置了框架来研究分配给一组公理的操作的最通用属性。

给定逻辑扣除系统H和任意一组甲型x，如果存在有限的公式序列属于x或是H的序列的公理，则在X中测定公式A.或者是从序列中的先前公式中获得的公式H的推理规则是X. X. X的扣除（或证据）在X中的房地或假设中的扣除（或证据）。Let CN（x）是从X中的X中的公式中推动的一组公式，作为场所或假设。 此集被称为X的后果集（相对于逻辑扣除系统H）。 然后，CN是应用于一组公式以获得新的公式的操作。 它具有以下属性：对于每组公式x

x⊆cn（x）

CN（CN（x））= CN（x）

CN（x）=⋃{cn（y）：y⊆x，y有限}

第三个条件规定CN（x）等于从X. Tarski的有限子集那种可衍生的公式组的联盟，这属于这些属性来定义后果操作的概念。 事实上，他补充说，有一个公式X，使得CN（{X}）是所有公式的集合A，并且该组必须是自然数的集合的有限或基数。 条件（3）意味着单调性的弱点和重要条件

如果x⊆y⊆a，则cn（x）⊆cn（y）。

为了包含整类逻辑系统，在文献中找到一个发现，需要比Tarski更略微的一般定义。 我们会说，任意集合A上的抽象后果操作C是应用于A和所有X的给出子集的子集的操作，满足上述条件（1），（2）和（4）。 如果另外，C满足（3）我们说这是一个合理的后果运作。

结果业务不仅存在于逻辑中，而且在数学的许多领域存在。 例如，摘要后果操作被称为通用代数和格子理论中的闭合运算符。 在拓扑中，将拓扑空间子集到其拓扑封闭的操作是闭合操作员。 实际上，设置A上的拓扑可以用封闭算子在满足C（∅）=∅和c（x∪y）= c（x）∪c（y）的附加条件的封闭运算符来识别，所述X，y⊆a。

给定一个组A上的后果操作C，据说A的子集X被称为C闭，或者如果c（x）= x，则闭合的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的抽象结果关系（不一定是某种形式的一组形式的商品）是满足上述条件（1） - （3）的A和元素的子集之间的关系。 如果它还满足（4），则据说是合理的。 如果⊢是一种抽象的结果和x∈A，那么我们可以说x是一组房屋或假设，得出根据⊢的结论，并且从x下面遵循x（根据⊢）。 抽象后果关系对应于Koslow的含义结构; 参见Koslow 1992为密切相关但不同的逻辑方法（广义）作为该作者引入的后果关系。

集合A上的后果操作与A的抽象后果关系一对一的对应关系。从后果操作C到后果关系⊢c，相反，从后果关系⊢到后果操作c⊢很容易和给出定义：

xīcaiffa∈c（x）和a∈c⊢（x）iffx⊢a。

而且，如果C是合法的，那么⊢c，如果⊢是合法的，则c⊢。

有关逻辑后果的一般讨论，请参阅进入逻辑后果。

2.逻辑作为后果关系

在本节中，我们定义了什么命题逻辑并解释与它们有关的基本概念。 我们将呼叫命题逻辑（如下所定义）简单逻辑系统。

我们在逻辑中研究的后果关系的主要特征之一是他们的正式性格。 这大致意味着，如果句子a从一组句子x下面，我们都有另一个句子b和另一组句子y分别与a和x共享相同的形式，然后b也从y遵循。在命题逻辑中，如果我们统一替换基本子通过其他句子获取y和b的x∪{a}的句子，然后b从y开始。（读者可以在进入逻辑后果中找到有关形式的想法的更多信息。）

将逻辑正式特征的想法变成严格的定义，我们需要介绍命题语言的概念和替代的概念。

一个命题语言（简称语言）l是一组连接，即，一组符号中的一组符号，其中一个符号都有一个arity n，它告诉我们n = 0，符号是一个命题常数，并且在n＞0的情况下，n＞0是否圆润是联合的例如，二进制，三元等。例如，{∧，∨，→，⊥，⊤}是（或可以）几种逻辑的语言，如经典和直觉，（⊥和⊤是0-ary，另一个连接是二进制的），{¬，∧，∨→，◻，◊}是几种模态逻辑的语言，（¬，◻，◊un是一元，另一个连接二进制）和{∧，∨，→，*，⊤，⊥，1,0}是许多值逻辑的语言，也是线性逻辑的片段（⊥，⊤，1和0是命题常数和其他符号二进制连接）。

给定语言L和一组命题变量v（从l不相交），L或L-Formulas的公式如下定义如下：

每个变量都是公式。

每个0-ary符号都是公式。

如果*是一个连接，并且n＞0是它的arity，那么对于所有公式φ1，...，φn，*φ1...φn也是一个公式。

L的替换σ是来自该组变量v到L的集成型的映射。它告诉我们，当我们执行替换时，哪个公式必须替换哪种变量。 如果p是变量，则σ（p）表示替换σ分配给p的公式。 将替换σ施加到公式φ的结果是通过同时替换φ中的变量，例如分别替换φ，...，pk，by型公式σ（p1），...，σ（PK）。 以这种方式，替换σ从一组公式中给出一个唯一的映射σ，以其自身满足

Σ（p）=σ（p），每个变量p，

Σ（†）=†，每一个0- ary连接†，

σ（*φ1...φn）= *σ（φ1）...σ（φn），对于ARIINY n＞0的每个连接*和公式φ1，...，φn。

公式ψ是公式φ的替换实例，如果存在替换σ，使得当施加到φ时，即，如果σ（φ）=ψ。

为了避免不必要的并发症，我们将在续集中假设所有逻辑使用相同的可降解集V变量，因此L的公式定义仅取决于L.语言L给出逻辑系统（或短的逻辑）和后果关系⊢在L的正式中，是正式的，对于每个替换σ，每组公式γ和每个配方φ，

如果γ⊢φ，则σ[γ]⊢σ（φ）

其中σ[γ]是通过将取代σ施加到γ中的式中获得的公式的组。 满足此属性的语言集合的后果关系称为结构中的结构，也是替代文献中的不变性。 他们在Łoō和苏斯科1958年首次考虑。Tarski仅明确考虑了封闭式套件，也在替代实例下关闭了一些后果关系; 他从未考虑过（至少明确）后果关系的替代不变条件。

我们将通过可能的子曲线引用字母L的逻辑系统，并且我们设置L =⟨l，⊢l⟩和ln =⟨ln，⊢ln⟩，⊢ln⟩是理解L（ln）是l（ln）和⊢l的语言（⊢ln）其后果关系。 逻辑系统L是有限的，如果⊢l是一个合理的后果关系。

可以通过多种方式给出逻辑系统的后果关系，一些使用校样工具，其他语义方式。 可以使用像Hilbert风格的公理系统，绅士型序列微积分或自然扣除风格微积分等校正系统来定义替代不变后果关系。人们还可以使用语义使用替代不变后果关系一类数学对象（代数，克里普克模型，拓扑模型等）和满意关系。

如果L1 =⟨l，则⊢l1⟩是由鼠标系统定义的⊢l1的逻辑系统，并且l2 =⟨l，⊢l2⟩是用语义定义的⊢l2的相同语言的逻辑系统，我们说验证系统用于定义⊢l1是用于定义⊢l2的语义的声音，如果⊢l1包含在⊢l2中，则如果γ⊢l1φ意味着γ12φ。 如果另一个包含保持验证系统，则据说是关于定义⊢l2的语义的任务，即，当γ⊢l2φ意味着γ11φ时。

一组L-公式γ称为逻辑系统L或L-理论的理论，如果它在关系⊢l下闭合，即，如果每当γ⊢lφ它也保持该φίγ。 换句话说，L的理论是L-公式组上的后果操作c⊢l的封闭组。 为了简化符号，我们表示CL的后果操作。 公式φ是L如果∅⊢lφ的定理（或有效性）。 然后Cl（∅）是L的定义集，是L的最小理论。L的一组L）将由L）表示。

考虑到逻辑系统L，后果操作CL是替代不变的，这意味着对于每组L-公式γ和每组替换σ，σ[Cl（γ）]⊆cl（σ[γ]）。 此外，对于我们的每个理论T，我们都有一个新的后果c

t

l

操作定义如下：

c

t

l

（γ）= cl（t∪γ）

那是，c

t

l

（γ）是根据L的γ和T遵循的一组公式。事实证明，如果才能在替换时关闭，如果c

t

l

是替代不变的。

如果L是逻辑系统和γ，Δ是L-公式的一组，我们将使用符号γ⊢lδ表示每个ψ∈δ，γ⊢lψ的状态。 因此，如果δ⊆cl（γ），则γ⊢lδ。

如果l =⟨l，⊢l⟩和l'=⟨l'，则⊢l'⟩是逻辑系统，其语言满足L'11（因此所有L'-Formulas是L-公式）和

γ⊢l'φ，

对于每组L'-公式γ和每个L'-甲术φ，我们说L'是一个片段L（实际上，L'-碎片），L是L'的扩展。

3.一些逻辑示例

我们展示了我们将在本文过程中提到的一些逻辑系统的示例，这些逻辑系统将在此处为读者提供方便。 只要有可能，我们会引用相应的条目。

我们使用写作的标准惯例（φ*ψ）而不是*φψ进行二进制连接，并省略公式中的外部括号。

3.1古典命题逻辑

我们将古典命题逻辑CPL的语言成为集合LC = {∧，∨，→，⊤，⊥}，其中∧，∨，→是二进制连接和⊤，⊥命题常数。 我们假设后果关系由通常的真实表方法（⊤被解释为真实和⊥为false），如下所述，

γ⊢cplφ为所有ψ∈γ分配的每个真实估值都会为φ分配true。

公式φ使得∅⊢cplφ是tautologies。 注意，使用语言LC，公式φ的否定被定义为φ→⊥。 有关更多信息，请参阅古典逻辑的条目。

3.2直觉的命题逻辑

我们采用直觉命题逻辑的语言与经典命题逻辑的语言相同，即集合{∧，∨，→，⊤，⊥}。 后果关系由以下Hilbert风格的微积分定义。

公理：

表格的所有公式

c0。

⊤c1.φ→（ψ→φ）c2的。

φ→（ψ→（φ∧ψ））的c3。

（φ∧ψ）→φc4。

（φ∧ψ）→ψ

c5。

φ→（φ∨ψ）c6。

ψ→（φ∨ψ）的c7。

（φ∨ψ）→（（φ→δ）→（（ψ→δ）→δ））c8。

（φ→ψ）→（（φ→（ψ→δ））→（φ→δ））c9。

⊥→φ

推理规则

φ，φ→ψ/ψ

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

3.3本地正常模态逻辑

我们考虑的模态逻辑的语言是通过添加一元连接◻来扩展LC的集合LM = {∧，∨，→，¬，◻，→}。 在模态逻辑上的标准文献中，常规模态逻辑不作为后果关系定义，而是作为具有某些属性的一组公式。 常规模态逻辑是LM的框架，包含古典逻辑语言的所有Tautologies，表单的公式

◻（φ→ψ）→（◻φ→◻ψ）

并在规则下关闭

φ，φ→ψ/ψ

φ/◻φ

φ/σ（φ），用于每个替换σ

注意，设定λ在替换实例下关闭，即每种替换σ，如果φ∈lm，则σ（φ）∈lm。

最小常规模态逻辑被称为k，可以通过Hilbert-Sique微积分和公理性的古典逻辑的TaItologies和公式◻（φ→ψ）→（◻φ→◻ψ），以及推理调制规则庞永和模态泛化。 注意，由于我们在演示中使用模式，因此可以在替换规则下关闭该组衍生式公式。

具有正常的模态逻辑λ，它与计算的后果关系相关联，该结石所定义为公理λ中的所有公式，并且作为推理模式的唯一规则。 由此后果关系给出的逻辑系统称为λ的局部后果。 我们用lλ表示。 它的定理是λ的元素，它坚持这一点

γ⊢lλφ或有φ1，...，φn∈γ，使得（φ1∧...∧φn）→φόλ。