这是阅读Pfenning的亚结构逻辑讲义所做的笔记. 这个课程之前的版本叫做线性逻辑. 线性逻辑是亚结构逻辑的一种. 虽然我之前学过一些线性逻辑, 但仍然对于线性逻辑和亚结构逻辑不甚了解.
implication一般翻译为推出? 不过我保留了原文, 因为翻译了之后容易和其他一些概念引起混淆. valid我没有翻译, 通行的翻译有效
也往往招致误解, 实际上在逻辑学中它具有特定的意义.
在入门课程里学习逻辑, 我们习惯于将真性当作一种数学概念, 某种客观且就像物理定律那样不可改变的东西. 真性是某种我们可以揭示和理解的东西, 但并不是我们可以创造的东西. 在这门课程里我将试图说服你其实存在着别的不同观念.
首先, 真性是瞬态的. 在讲座的这个时间点我拿着一支粉笔. 直接的证据可以确认: Frank拿着一支粉笔.
在我将这粉笔置于我面前的桌子上之后, 这个命题就不再为真了. 因此, 显然, 真性是瞬态的. 亚结构逻辑捕获并分析这种现象, 其在计算机科学中具有根本的重要性. 例如, 当在某个命令式语言中执行着一个程序时某个变量或者存放着值. 这就是一个瞬态的真性, 因为在给赋值之后其就不再为真了——转而, 的值会是.
其次, 特定的真性是永恒的. 例如, 对于过剩的证明而言, 很难否定Pythagoras定理. 抑或是, 根据implication的本性, 对于任意的命题, 总是可以推出. 亚结构逻辑既考虑到了瞬态也考虑到了永恒, 因此其是为了泛化而非取代研究永恒真性的传统逻辑. 在这门课程的上下文里, 我们将这样的逻辑称为亚结构的. 术语结构和亚结构的起源将在这次讲座的之后得到澄清.
逻辑是对于valid推理的法则的研究, 所以说我们将以同样的方式开始我们的课程. 今天的讲座我们将会全然避免逻辑联结词, 只使用推理规则. 实际上, 我们可以使用推理规则描述一些算法, 它们可以视为执行逻辑推理, 这是逻辑和计算机科学的诸多联系之一.
考虑有向图中顶点和之间的关系. 我们想要定义何时从到存在着一条路径. 从数学上来说, 我们可以称路径 (path) 关系是边 (edge) 关系的传递闭包. 我们以两条推理规则定义这个概念: 一些术语:
{译注: 最早Pfenning使用的术语是cut归约和identity展开, 但意思完全相同.}
到目前为止我们已经为有序逻辑, 线性逻辑, 以及亚结构逻辑划定了严格的界限. 为了使得线性逻辑更富表现力, 我们使用了递归, 因为从编程角度而言递归是相当自然的. 在讲座2里我们简要提及了指数模态以及它的规则, 其服从于弱化和收缩.
本次讲座里我们将会进行解释, 实际上是某种更为一般的构造的结果, 而这种构造也可以对于其他逻辑施行. 例如, 在结构逻辑中, 其通常记作, 表达了必然为真或者在所有的可能世界中为真. 从这个角度来看的证明论在某种意义上是更加令人愉快的, 但最终也并不全然令人满意. 下次讲座我们将会回到这里进行改进, 甚至进一步将其泛化.
Girard [1987]的指数模态, 在直觉主义情形下 [Girard and Lafont, 1987], 可以在相继式演算中以如下规则定义. 这里的意思是中的每个前件都具有形式. 以这些规则, 我们可以从中得到任意多份想要的的复制.