证明理论语义（三）
在他关于逻辑基础的早期论文中，Popper（1947a; 1947b; 1947b; Binder等，编辑，2022年）在证明理论术语中给出了逻辑常数的推论性特征。他使用序列的演算，并通过此类序列的某些衍生性条件来表征逻辑常数。他的术语清楚地表明，他打算对逻辑常数的证据理论语义，因为他谈到了“推论定义”和通过以描述方式定义常数实现的“数学逻辑的琐事”。尽管他的演讲并非没有概念上的不精确和错误，但他预计现在有许多在证明理论语义中常见的想法，例如通过某些最小值或最大程度的条件在引言或消除规则方面通过某些最小值或最大条件来描述逻辑常数。
Kneale（1956）和Hacking（1979）对逻辑性辩论的重要贡献是，根据序列序列规则的逻辑常数是逻辑常数。 Došen（1980; 1989）在其逻辑常数为“标点符号”的理论中提出了对逻辑性的彻底说明，并在逻辑层面表达了结构特征。他将逻辑常数理解为遵循序列的某些双行规则，可以在两个方向上读取。例如，连词和脱节服从（在经典逻辑中，具有多种形式的成功）双行规则
=
γ
⊢
�
∧
�
,
Δ
γ
⊢
�
,
Δ
γ
⊢
�
,
Δ
=
γ
,
�
∨
�
⊢
Δ
γ
,
�
⊢
Δ
γ
,
�
⊢
Δ
Došen能够提供包括模态逻辑系统的特征。他明确将自己的作品视为对逻辑性辩论的贡献，而不是对证明理论语义的任何概念。 Sambin等人的基本逻辑（Sambin，Battilotti和Faggian，2000年）明确地理解Došen所说的双线规则是基本的意思，赋予规则。连词和析取的双行规则被理解为这些常数的隐式定义，通过某些过程可以将其转变为我们习惯的明确序列规则。因此Sambin等。使用与Došen相同的起点，而是将其解释为对常数行为的结构描述，而是语义上是其隐式定义。
还有其他几种方法可以对逻辑常数进行统一的证明理论表征，所有这些方法至少都触及了证明理论语义的问题。这样的理论是Belnap的显示逻辑（Belnap，1982），Wansing的信息结构逻辑（Wansing，1993b），通用的证明编辑系统及其实现，例如爱丁堡逻辑框架（Harper，Honsell，Honsell和Plotkin，1987）以及许多继任者以及许多继承者，这些框架是其中的许多继任者允许各种逻辑系统的规范。由于线性逻辑的兴起，而且更一般而言，有各种方法与逻辑有关，这些方法在限制其结构规则方面有所不同（请参见第3.10节）。最近的动作从将特定逻辑列为真正的逻辑上，转向更多元化的立场（例如，参见Beall and Restall，2006年），这对不同逻辑的共同点感兴趣，而无需任何对特定逻辑的偏爱，可以被视为从语义依据转向结构表征的转变。
进一步阅读：
对于Popper的逻辑常数理论，请参见Binder等。 （2022），Piecha（2023）。
有关逻辑常数及其逻辑性，请参阅逻辑常数的条目。
有关线性和下结构逻辑，请参见线性逻辑上的条目以及子结构逻辑上的条目。
有关逻辑中的多元化，请参见有关逻辑多元化的条目。
2.5类别证明理论
关于证明理论的类别理论有大量文献，在律师，兰贝克和其他人的开创性工作之后（参见Lambek和Scott，1986），类别理论本身可以被视为一种抽象证明理论。如果看箭头
�
→
�
在一个类别中，作为b的一种抽象证明，我们有一个表示，它超出了b的纯衍生性（因为箭头具有其个性），但并不涉及该证明的特定句法结构。对于直觉系统，类别形式的证明理论语义可能最接近经典案例中的典型语义。
分类理论的最高度发达的方法之一是由于došen造成的。他不仅在证明理论中推动了分类方法的应用（例如Došen和Petrić，2004年），而且还展示了如何在类别理论本身中使用证明理论方法（Došen，2000年）。与证明理论语义有关的分类逻辑最重要的是，在分类逻辑中，箭头总是与身份关系在一起，在证明理论中，箭头与证明的身份相对应。这样，分类证明理论的思想和结果与可能所谓的强化证明理论语义有关（请参阅第3.7节），即将证明作为实体本身的研究，而不仅仅是建立后果的工具（ Došen，2006年；
由于分类意义上的箭头之间存在着牢固的关系，而在演绎推理的意义上，有类似的类似物可以在演绎领域中处理所有概念，通常都以新颖的方法，思想和结果来补充一种在某种程度上补充演绎方法非常有生产力的方式。类别证明理论语义是一个非常广泛的研究领域，与本条目中采用的演绎视角平行运行 - 演绎视角在哲学中更为普遍。在直觉逻辑领域中，分类逻辑涵盖了高度高级的主题：超出标准量词逻辑类型的类型理论，其中包括Martin-Löf的传统（请参阅第2.2.3节），包括同型类型理论。对于许多其他逻辑系统，已经开发了类别语义，包括经典逻辑和各种子结构逻辑，例如线性逻辑。
分类理论的哲学上一般重要的一般特征是其固有的假设特征。这是由于它从假设的陈述开始的事实
�
→
�
（箭头）而不是分类陈述A（“分类”而不是“假设”，而不是“分类”，而不是“类别”，而不是“类别理论”）。这样，它就会克服标准范式，特别是基于有效性的证明理论语义（请参阅第3.6节）。
进一步阅读：
对于一般的类别方法，请参见类别理论的条目和数学哲学中的结构主义的条目。
有关类别的证明理论语义，请参见PYM，RITTER和ROBINSON（2023，其他互联网资源）。
2.6原子系统
证明理论语义主要与逻辑常数有关。即使人们同意这种方向 - 定义反思理论（请参见第2.3.2节）是一个例外 - 我们仍然必须修复原子句子的状态及其证明的状态。在模型理论语义中，逻辑上复杂的句子的真实是根据结构定义的，该结构称为该句子的“模型”。该结构决定了哪些原子句子是真实的，哪些是不正确的。一个复杂的句子是否真正取决于其原子成分。这在证明理论语义上是相似的。复杂句子的证明是否有效取决于正在考虑的系统的原子基础。在这里，原子基碱通常被视为生成原子句子的微积分：原子基碱中原子句的证据本身是有效的。类似于对所有结构的逻辑真理的模型理论定义，在证明理论语义中，人们将在逻辑上定义有效的证据为与所有原子基础有关的证明。
有多种选择原子系统应被视为原子基础的候选者。 （1）最简单的是逻辑编程理论中使用的Herbrand模型，这些模型只是原子句子的集合。从理论上讲，这些将仅由公理组成，而没有适当的推理规则。 （2）在洛伦岑（Lorenzen
�
1
,
……
,
�
�
⇒
�
允许一个人从中产生b
�
1
,
……
,
�
�
。 （3）更多涉及的系统可能包含原子规则，可以使一个假设解除假设，这与逻辑规则（例如暗示介绍）相似。 （4）概括这个想法的人可能会允许原子本身的原子规则，即更高级别的规则（请参阅第2.1.3节）。 （5）甚至进一步的先进将是包含定义反射规则的原子系统（请参阅第2.3.2节）。 - 可以想象许多其他构成原子系统的原子规则。
对于证明理论语义，这里的关键点是某些形式结果取决于接受哪种原子系统的类型。这特别是对于语义完整性问题（请参阅第2.8节）。当被视为证明理论语义的原子基础时，对哪种原子系统的调查导致逻辑层面的正式系统刚刚开始（请参阅Sandqvist 2015b； Piecha和Schroeder-Heister，2016a; Stafford; Stafford 2023，其他Internet资源）。应该注意的是，这是证明理论语义的强度特征：我们不仅对各种原子系统产生的原子产生的原子感兴趣，而且是如何完成的，也就是说，通过哪种规则类型实现了。这与模型理论语义是一个至关重要的差异，这在这方面纯粹是扩展的。有关证明理论语义的进一步强度特征，请参见第3.7节。
2.7基于句子的语义
人们可以直接定义句子的证明理论有效性，而不是定义句子证明的有效性。在逻辑上复杂句子的有效性的定义中，人们将丢弃对这些句子的证明的引用。这并不意味着一个人正在放弃证据理论的方法，因为人们仍然指原子基础中的证明。证明在原子层有，但不在逻辑层面上。从技术上讲，这种方法比基于证明的有效性的方法要简单得多（请参阅第2.2.2节），但仍然足以讨论基本主题，例如语义完整性（请参阅第2.8节）。实际上，从从第2.2.2节的意义上有效的句子a的证明，可以推断出基于句子的语义的有效性；相反，可以构建基于句子的语义A（尽管退化）A（尽管退化）A的有效性。从某种意义上说，基于句子的语义与Martin-Löf系统中固有的证明理论语义有关（请参阅第2.2.3节），在基本逻辑中（在其中依赖类型不起任何角色），证明判决的信息
�
：
�
可以丢弃以简化的判断
�
真的
。
关于原子系统的最小命题逻辑中句子有效性的一个可能定义，因为其在命题逻辑中的原子基础是：以下是：
如果原子公式A为S Valid，则是在S中衍生的。
连词
�
∧
�
如果a和b都是s-valid，则为s-valid。
一个脱节
�
∨
�
如果A或B为S瓦利德，则为S-VALID。
含义
�
→
�
有效，如果每次扩展
�
′
s，如果是
�
′
- valid然后b是
�
′
-有效的。
请注意，在假设有效性的陈述中，提到了所考虑的原子基碱的任意扩展。与证明有效性的正式定义一样，考虑基础扩展是为了确保单调性并避免空虚的有效性。在文献中，遵循SandQvist（2015a），通常以更具体的含义使用“基本扩展语义”一词：即基于句子的语义的特殊形式，在该语义上，脱节会得到一种偏差的解释。
基于句子的语义中的有效性取决于原子系统的选择。这种选择是使基于句子的语义理论的方法。如第2.6节所示，原子系统的类型计数，以及有关含义和后果陈述所考虑的扩展关系。
2.8语义完整性
证明理论的语义在精神上是直觉的，至少是其起源。相应地，Prawitz（1971）猜想这些后果陈述
γ
⊨
�
这是有效的任何原子基础的证明是合理的
γ
⊢
�
正式的直觉逻辑系统。在句子语义的框架内，对于语义完整性的有效性问题，它比有效证明的框架更容易处理，因此这种猜想被证明是错误的。哈罗普的规则
Ø
�
→
（
�
∨
�
）
（
Ø
�
→
�
）
∨
（
Ø
�
→
�
）
可以在本框架中验证直觉逻辑中的（但仅是可接受的）（Piecha和Schroeder-Heister，2019年）。但是，当原子碱基的扩展结构超出设置的理论超集关系之外，图片发生变化，而Kripke的直觉逻辑证明完整性证明将适用于证明理论框架（Goldfarb 2016； Stafford和Nascimento 2023）。避免不完整的另一种方法是给出一个非标准的解释，例如，要求次要的前提和结论
∨
- 灭绝可以始终被视为原子质（参见Sandqvist，2015a）。
进一步阅读：
有关Prawitz的完整性猜想，请参见证明理论有效性的例子的补充。
有关Harrop规则在直觉逻辑的可接受性陈述中的作用，请参见Intuitionistic逻辑的条目。
3。标准证明理论语义的扩展和替代方案
3.1消除规则作为基本
证明理论语义的大多数方法都将简介规则视为基本，含义给予或自我辩护，而消除推论对于给定的简介规则有效。这个概念至少具有三个根源：第一个是意义上的验证主义理论，句子的确定性条件构成其含义。第二个想法是，我们必须区分赋予含义的因素以及这种含义的后果，因为并非所有推论知识都可以由定义的应用组成。第三个是主张与其他语音行为（例如假设或拒绝）的首要地位，这在到目前为止所考虑的所有方法中都是隐含的。
人们可能会通过考虑消除规则而不是引入规则作为证明理论语义的基础来研究多远。 Dummett（1991，第13章）概述了一些基于消除而不是简介规则的证明理论语义的想法，尽管以一种非常基本的形式。基于消除推论的有效性的更精确的定义是由于Prawitz（1971; 2007;另见Schroeder-Heister 2015）。它的必要想法是，如果将淘汰规则应用于其最终公式是有效的证明或减少到一个公式的结果，则封闭的证据被认为是有效的。例如，封闭证明暗示
�
→
�
有效，如果对于任何给定的闭合有效证明A，则使用Modus Ponens
�
→
�
�
�
对于这两个证明，是B的有效证明，或者减少了这样的证明。该概念使Prawitz风格的证明理论语义的三种基本要素中有两种（请参阅第2.2.2节）：减少证明的作用和假设的替代观点。只有以介绍结尾的证据的规范性才变成以消除结尾的证据的规范。
3.2否定和否认
标准证明理论语义是以主张为中心的，因为确定性条件决定了逻辑常数的含义。对应于诉讼的直觉方式，否定方式
Ø
�
公式A通常被理解为意味着荒谬
�
→
⊥
， 在哪里
⊥
是一个无法断言的常数，即没有确定的确定性条件。这是理解否定的“间接”方式。在文献中，人们讨论了冯·库施拉（Von Kutschera，1969）之后，可能被称为“直接”否定。这样一来，人们就会理解一个单位原始的否定操作员，或者至少不能沦为暗示荒谬的。这也不是经典的否定。它遵守规则，将逻辑常数的通常规则双重化。有时，它被称为句子的“否认”，有时也称为“强烈否定”（参见Odintsov，2008年）。否认的典型规则
～
�
一个是
～
�
～
�
～
（
�
∨
�
）
～
�
～
（
�
∧
�
）
～
�
～
（
�
∧
�
）
本质上，操作员的拒绝规则对应于双重操作员的主张规则。已经研究了几种否认逻辑，尤其是纳尔逊（1949年）的“可构造虚假”逻辑，纳尔逊在某种可实现的语义方面所激发。主要的重点是他后来称为N3和N4的系统，该系统在矛盾的处理方面有所不同（N4是N3没有矛盾的Quodlibet）。通过拒绝任何方法来证明理论语义的方法可以通过交换断言和否认并从逻辑常数转向其双重偶数双重。这样，一个人获得了基于反驳的系统
（
=
否认证明）而不是证明。它可以理解为通过保持其直觉精神将Popperian观点应用于证明理论语义。正式地，它通过给它们提供了证明理论语义，从而导致诸如双重直觉逻辑之类的系统。
另一种方法是，不仅是以断言为中心的证明理论语义对否定为中心的反驳理论语义，而且要查看主张规则之间的关系和由定义反向重新定义的原则或原则所支配的拒绝之间的关系它自己的。这将是所谓的“断言 - 士兵”的原则。尽管在标准的证明理论语义中，反演原则控制主张与假设（或后果）之间的关系，现在这样的原则将调节主张与拒绝之间的关系。鉴于A的某些定义条件，它将说对每个定义条件的否定会导致拒绝自身。为了结合和分离，这导致了普遍的断言和否认规则
�
�
∨
�
�
�
∨
�
～
�
～
�
～
（
�
∨
�
）
�
�
�
∧
�
～
�
～
（
�
∧
�
）
～
�
～
（
�
∧
�
）
这个想法可以很容易地推广到定义反射，从而产生了一个交织在一起的推理系统。它与传统反对派广场所研究的审判形式之间的演绎关系有相似之处（Schroeder-Heister，2012a； Zeilberger，2008）。应该强调的是，拒绝操作员在这里是一个表明判断形式而不是逻辑操作员的外部标志。这特别意味着它不能迭代。
主张和否认条件都赋予句子的意义，从而对逻辑行动的意义也为“双边主义”一词，这一想法也是由Rumfitt创造的术语。
进一步阅读
有关否定和否认的证明理论语义，请参见Tranchini（2012b），Wansing（2001; 2017），以及Carrara，Chiffi和de Florio（2017年）和《否定条目》，关于断言和拒绝的特殊问题，有关连接逻辑的条目和矛盾的条目。
