Interpretability degrees of finitely axiomatized sequential theories (Q2436609)

Before explaining Albert Visser's main achievement in his article under review, we need to introduce some definitions and notation. -- A \textit{finitely axiomatized theory} is a theory presented to us by giving a finite list of axioms. -- The \textit{adjunctive set theory}~\(\mathsf{AS}\) is the theory with a binary relation~\(\in\), the axiom~\(\exists x \, \forall y \, \neg \, y \in x\) saying that there is the empty set, and the axiom~\(\forall u,v \, \exists x \, \forall y \, (y \in x \leftrightarrow y \in u \vee y = v)\) saying that, given sets~\(u\) and \(v\), there is the set~\(u \cup \{v\}\). -- A \textit{direct interpretation} is an interpretation that is unrelativized (has the trivial domain) and identity-preserving (translates identity to identity). -- A \textit{sequential theory} is a theory that directly interprets \(\mathsf{AS}\). -- We fix a finitely axiomatized theory~\(A\) that interprets Robison's arithmetic~\(\mathsf Q\). -- We denote by \(\mathbb V'_A\) the set of all finite extensions of \(A\) in the same language as \(A\). -- We denote by \(\vartriangleleft'_A\) the binary relation on \(\mathbb V'_A\) defined by: \(U \vartriangleleft'_A V\) if and only if \(V\) interprets \(U\). -- We denote by \(\equiv_A\) the equivalence relation on \(\mathbb V'_A\) defined by: \(U \equiv_A V\) if and only if \(U \vartriangleleft'_A V\) and \(V \vartriangleleft'_A U\). -- We denote by \(\mathbb V_A\) the quotient \(\mathbb V'_A / {\equiv_A}\) and call its elements \textit{degrees of interpretability}. -- We denote by \(\vartriangleleft_A\) the binary relation on \(\mathbb V_A\) induced by \(\vartriangleleft'_A\). Now that we introduced the definitions and notation, we can explain Albert Visser's main achievement in his article. Vítězslav Švejdar asked if \((\mathbb V_A,\vartriangleleft_A)\) is a lattice. Albert Visser answers affirmatively when \(A\) is a sequential theory. He achieves this answer by proving a stronger convexity result: If \(A\) is sequential, \(B\) is a sequential and finitely axiomatized theory, and \(A \vartriangleleft_A B\), then there is a finitely axiomatized extension~\(C\) of \(A\) in the same language as \(A\) such that \(B \equiv C\).