Recursive logic frames

探究性一阶逻辑既不紧凑也不可递归地公理化

Inquisitive first-order logic is neither compact nor recursively axiomatizable

本文研究了探究性一阶逻辑（InqBQ）的元理论性质，证明其蕴含关系不满足紧凑性，且有效式集不可递归枚举。

二元谓词经典理论与一元谓词非经典逻辑的递归不可分性

Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate

本文通过骨牌问题提取递归不可分性，间接证明了有界语言中经典与非经典一阶逻辑各种片段的不可判定性，涵盖二元谓词经典逻辑、模态及超直觉主义谓词逻辑的单调片段。

Recursive enumerability and elementary frame definability in predicate modal logic

We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplet…

The provably total recursive functions and the MRDP theorem in Basic Arithmetic and its extensions

We study Basic Arithmetic, BA introduced by W. Ruitenburg. BA is an arithmetical theory based on basic logic which is weaker than intuitionistic logic. We show that the class of the provably total recursive functions of BA is a proper sub-class of the primitive recursive functions. Three extensions of BA, called BA+U, BA_c and EBA are investigated with relation to their provably total recursive functions. It is shown that the provably total recursive functions of these three extensions of BA are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-…

Team Semantics and Recursive Enumerability

It is well known that dependence logic captures the complexity class NP, and it has recently been shown that inclusion logic captures P on ordered models. These results demonstrate that team semantics offers interesting new possibilities for descriptive complexity theory. In order to properly understand the connection between team semantics and descriptive complexity, we introduce an extension D* of dependence logic that can define exactly all recursively enumerable classes of finite models. Thus D* provides an approach to computation alternative to Turing machines. The essential novel feature…

Recursive axiomatisations from separation properties

We define a fragment of monadic infinitary second-order logic corresponding to an abstract separation property. We use this to define the concept of a separation subclass. We use model theoretic techniques and games to show that separation subclasses whose axiomatisations are recursively enumerable in our second-order fragment can also be recursively axiomatised in their original first-order language. We pin down the expressive power of this formalism with respect to first-order logic, and investigate some questions relating to decidability and computational complexity. As applications of thes…