报告人：陈至诚

题目：Lyndon interpolation theorem in R-restricted fragment of 1st-order logic

时间：2021/11/2 15:10-18:00

摘要:  Lyndon 插值定理说的是在关系型语言的一阶逻辑中，任给语句间的有效蕴含式，存在插值，其中所有正（负）出现的关系符都同时在前、后件中正（负）出现。对于关系型语言，Lyndon 插值定理强于Craig 插值定理。

给定二元关系符R，称形如"任意（存在）xRy"的量词为"R-受限"的，所含量词皆是R-受限量词的公式称为"R-受限公式"。

[S.Feferman,1968]证明了一个 many-sorted 无穷逻辑的考虑受限量词的插值定理，使用的是证明论方法。作为其推论，Craig 插值定理在R-受限公式上成立。

利用 back-and-forth 证明一阶逻辑插值定理的做法可见于[J.Flum,1975]、[M.Otto,2000]。取道于此，我们引入一种对应R-受限量词的 back-and-forth 概念，并利用之证明：Lyndon 插值定理在R-受限公式上成立。证明的思路主要借鉴了[M.Otto,2000]。