We study abstract versions of Goedel’s second incompleteness theorem and formulate generalizations of Loeb’s derivability conditions that work for logics weaker than the classical one. We isolate the role of the contraction and weakening rules in Goedel’s theorem and give a (toy) example of a system based on modal logic without contraction invalidating Goedel’s argument. On the other hand, Goedel’s theorem is established for a version of Peano arithmetic without contraction. (Joint work with Daniyar Shamkanov)

Intuitionistic epistemic logic, IEL, introduces to intuitionistic logic an epistemic operator which reflects the intended BHK semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the Logic of Proofs, LP, and its arithmetical semantics. We show here that the Gödel embedding, realization, and an arithmetical interpretation can all be extended to S4 and LP extended with a verification modality, thereby providing intuitionistic epistemic logic with an arithmetical semantics too.

In this series of talks, I will provide an analysis of definable sets in models of linear arithmetics. Here, for a cardinal k, the k-linear arithmetic (LA_k) is a full-induction arithmetical theory extending Presburger arithmetic by k non-standard scalars (= unary functions of multiplication by distinguished elements). Note that each model of a linear arithmetic naturally corresponds to a discretely ordered module over the ordered ring generated by the scalars.

I will prove a quantifier elimination result (QE up to disjunctions of bounded pp-formulas) for LA_1 and give a complete characterisation of definable sets in its models. On the other hand, I will construct an example of a model of LA_2 (or any LA_k with k at least 2) where multiplication is definable on a non-standard initial segment (and thus no pp-elimination is possible). Finally, I will show that all the theories LA_k satisfy quantifier elimination (at least) up to bounded formulas.

I will mention several applications and corollaries of these results including a construction of a non-NIP ordered module, or a result on automorphisms in saturated models of PA.

In this series of talks, I will provide an analysis of definable sets in models of linear arithmetics. Here, for a cardinal k, the k-linear arithmetic (LA_k) is a full-induction arithmetical theory extending Presburger arithmetic by k non-standard scalars (= unary functions of multiplication by distinguished elements). Note that each model of a linear arithmetic naturally corresponds to a discretely ordered module over the ordered ring generated by the scalars.

I will prove a quantifier elimination result (QE up to disjunctions of bounded pp-formulas) for LA_1 and give a complete characterisation of definable sets in its models. On the other hand, I will construct an example of a model of LA_2 (or any LA_k with k at least 2) where multiplication is definable on a non-standard initial segment (and thus no pp-elimination is possible). Finally, I will show that all the theories LA_k satisfy quantifier elimination (at least) up to bounded formulas.

I will mention several applications and corollaries of these results including a construction of a non-NIP ordered module, or a result on automorphisms in saturated models of PA.

In this series of talks, I will provide an analysis of definable sets in models of linear arithmetics. Here, for a cardinal k, the k-linear arithmetic (LA_k) is a full-induction arithmetical theory extending Presburger arithmetic by k non-standard scalars (= unary functions of multiplication by distinguished elements). Note that each model of a linear arithmetic naturally corresponds to a discretely ordered module over the ordered ring generated by the scalars.

I will prove a quantifier elimination result (QE up to disjunctions of bounded pp-formulas) for LA_1 and give a complete characterisation of definable sets in its models. On the other hand, I will construct an example of a model of LA_2 (or any LA_k with k at least 2) where multiplication is definable on a non-standard initial segment (and thus no pp-elimination is possible). Finally, I will show that all the theories LA_k satisfy quantifier elimination (at least) up to bounded formulas.

I will mention several applications and corollaries of these results including a construction of a non-NIP ordered module, or a result on automorphisms in saturated models of PA.

A model M of PA has the omega-property if it has an elementary end extension coding a subset
of M of order type omega. The countable short recursively saturated models are a proper subclass
of the countable models with the omega-property, and both classes share many common
model theoretic properties. For example, they all have automorphism groups of size continuum. I will give a brief survey of what is known about models with the omega-property and I will discuss some open problems.

In this talk, I will give an overview of recent results on linear arithmetics with main focus on definability in their models. Here, for a cardinal k, the k-linear arithmetic (LA_k) is a full-induction arithmetical theory extending Presburger arithmetic by k non-standard scalars (= unary functions of multiplication by distinguished elements). The hierarchy of linear arithmetics lies between Presburger and Peano arithmetics and stretches from tame to wild.

I will present a quantifier elimination result for LA₁ and give a complete characterisation of definable sets in its models. On the other hand, I will construct an example of a model of LA₂ (or any LA_k with k at least 2) where multiplication is definable on a non-standard initial segment (and thus no similar quantifier elimination is possible).

There is a close connection between models of linear arithmetics and certain discretely ordered modules (as each model of a linear arithmetic naturally corresponds to a discretely ordered module over the ordered ring generated by the scalars) which allows to construct wild (e.g. non-NIP) ordered modules. On the other hand, the quantifier elimination result for LA₁ implies interesting properties of the structure of saturated models of Peano arithmetic.

Slides from this talk.

Much work in the model theory of Peano Arithmetic is based on constructions of elementary end extensions. Let N be an elementary end extension of M. An important isomorphism invariant of the pair (N,M), is Cod(N/M)—the set of intersections with M of the definable subsets of N. For a given model M, one wants to characterize those subsets X of M for which there is an elementary end extension of N of M such that X is in Cod(N/M), and those subsets A of the power set of M for which there is an N, such that A=Cod(N/M). Such characterizations involve properties of subsets of M, but also, a bit surprisingly, properties of M itself. I will talk about some old and some new results in this area.

The longstanding problem of representing Scott sets as standard systems of models of Peano Arithmetic is one of the most vexing in the subject. We show that the analogous question has a positive solution for real closed fields and Presburger arithmetic. This is joint work with Alf Dolich, Julia Knight and Karen Lange.

In 1936, only a few years after the incompleteness theorems were proved, Gentzen proved the consistency of Peano arithmetic by using transfinite induction up to the ordinal epsilon_0. I will give a short proof of the result, based on on the simplification introduced by Schutte, and discuss some of the consequences.

Let M be countable recursively saturated model of Peano Arithmetic. In the talk I will discuss ongoing research on recognizing standard system of M in the automorphism group of M.

We discuss two results relating ideas in Reverse Mathematics to the properties of models of first order arithmetic. The first shows that we can extend second order arithmetic by the existence of a non-principal ultrafilter — a third order property — while remaining conservative. The second result shows that we can extend models of RCA so that any particular set is definable; this allows us to recover some properties of models of Peano arithmetic for models of RCA.