Interpreting the monadic second order theory of one successor in expansions of the real line

Interpreting the weak monadic second order theory of the ordered rationals

We show that the weak monadic second order theory of the structure $({\mathbb Q}, <)$ is first order interpretable in its automorphism group.

分形与单一后继的单子二阶理论

Fractals and the monadic second order theory of one successor

本文证明了几乎任意经典分形子集的结构均能解释单一后继的单子二阶理论，并指出该结果在特定维数与光滑性条件下是尖锐的。

实数序可加群的两个离散子群展开

Expansions of the ordered additive group of real numbers by two discrete subgroups

如果$a$是二次的，则$(\mathbb{R},<,+,\mathbb{Z},\mathbb{Z} a)$的理论是可判定的。如果$a$是黄金比例，则$(\mathbb{R},<,+,\mathbb{Z},\mathbb{Z} a)$定义乘以$a$。利用基于$a$的连分数展开的Ostrowski计数系统定义一个后继的一元二阶逻辑中的上述结构，建立了这些结果.逆命题$(\mathbb{R},<,+,\mathbb{Z},\mathbb{Z} a)$定义了一个后继的一元二阶逻辑。

带后继函数的完全n分支序数树的初等理论

The elementary theory of full $n$-branching ordinal trees with successor functions

该论文研究带后继函数的完全n分支序数树的初等理论，对标准树按初等等价分类，建立量词消去与可判定性结果，还发展可实现性理论并澄清树与一元二阶逻辑的关系。

A model-theoretic characterization of monadic second order logic on infinite words

Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols. Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in $\mathcal{P}(ω)$, the power set Boolean algebra of the natural numbers, equipped with modal operators for 'initial', 'next' and 'future' states. We prove that the first-order theory of this structure is the model companion…

作为有状态程序的证明：一种带抽象 Hoare 三元组的一阶逻辑及其到命令式语言的解释

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language

本文提出一种扩展一阶逻辑，以 Hoare 三元组风格对抽象状态进行推理，并通过可实现性解释将证明提取为混合函数式/命令式程序，同时给出基于状态单子的语义解释及 Heyting 算术单子扩展。