\begin{document}

	
	\title{Universal properties of truth}
	
	\section{Introduction}
	
	Many types of arguments in mathematical logic (especially in foundations) make an important use of a truth predicate of some form. For example, when one wants to prove a consistency of one theory in its extension, one often proceeds by defining a truth predicate for a class of formulae and then inductively shows that each sentence from this class which is provable in the weaker theory is true. Similarly, if one wants to deduce finite axiomatizability of an infinite theory, one often makes use of a definable truth predicate. Last but not least, the existence of a truth predicate for some language $\mathcal{L}$ is often used to show that a given model of an $\mathcal{L}$-theory is $\mathcal{L}$-recursively saturated.
	
	\rem{In most general terms, the current paper investigates whether the use of the truth predicate in such arguments is \textit{essential}}.
	More concretely, we focus on model-theoretic properties and ask whether for a given property $P$, the existence of a definable truth predicate is necessary to uniformly impose this property. One of the clearest illustrations here is provided by the property of \textit{imposing recursive saturation}: it is a very basic fact that every nonstandard model $\mathcal{M}\models \textnormal{PA}$ which has a partial inductive nonstandard satisfaction class (i.e. a satisfaction predicate for all formulae of some nonstandard complexity which satisfy full induction) is recursively saturated (a very simple overspill argument is presented in \cite{kaye}). Since the theory of partial inductive nonstandard satisfaction classes is axiomatizable, we have an example of a theory, call it $\textnormal{UTB}$, which \textit{imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation}. In general, we say that a theory $U$ imposes $\mathcal{L}$-recursive saturation iff the $\mathcal{L}$-reduct of an arbitrary nonstandard model of $U$ is recursively saturated. Quite surprisingly there is a good sense in which the use of the $\textnormal{UTB}$-truth predicate is essential in this context. More precisely, we have the following theorem due to Roman Kossak \cite[Theorem 2.4]{kossak_cztery_problematy}:
	
	\begin{tw}\label{tw_kossak}
		Suppose that $U$ is a theory in a language $\mathcal{L}$ which extends $\textnormal{PA}$ and proves all instantiations of the induction scheme with $\mathcal{L}$-formulae. If $U$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, then in every $\mathcal{M}\models U$ there exists a definable partial satisfaction class.
	\end{tw}  
	
	Thus Kossak's theorem shows that, for a reasonable class of theories, having a definable satisfaction predicate is necessary to impose recursive saturation.
	
	Another example of a property that seems even more directly connected with the definability of the notion of truth is \textit{imposing elementary equivalence}. Consider the weak truth theory $\textnormal{TB}^-$: it is obtained by  adding $\textnormal{PA}$ all the axioms of the form $T(\qcr{\phi}) \equiv \phi$ (where $T$ is a fresh predicate). Then $\textnormal{TB}^-$ has the following property: whenever $\mathcal{M} \models \textnormal{TB}^-$, $\mathcal{N}\models \textnormal{TB}^-$ and $\mathcal{M}$ is a submodel of $\mathcal{N}$, then $\mathcal{M}$ and $\mathcal{N}$ satisfy the same sentences of $\mathcal{L}_{\textnormal{PA}}$. This can be abstracted into a property of a general theory: we say that a theory $U$ imposes $\mathcal{L}$-elementary equivalence iff whenever $\mathcal{M},\mathcal{N}\models U$ and $\mathcal{M}\subseteq \mathcal{N}$, then $\mathcal{M}$ and $\mathcal{N}$ satisfy the same $\mathcal{L}$-sentences. Then we can ask whether having a definable truth predicate for $\mathcal{L}$-sentences is necessary for a (sufficiently strong) theory $U$ to impose $\mathcal{L}$-elementary equivalence. It turns out that $\textnormal{TB}^-$ is indeed essential to ensure this property (Theorem \ref{tw_impos_elem}, point 3).

	When we start investigating the main question, one quickly encounters a number of semantic properties imposed by certain natural truth theories over $\textnormal{PA}$ for which those truth predicates are not essential. However there seem to be quite natural candidates for axiomatic theories of truth-related notions which do provide such exact characterisations. One example of such a phenomenon is the notion of definability: whenever $\mathcal{M}, \mathcal{N}$ are models of $\textnormal{UTB}^-$  (the theory of the uniform Tarski biconditionals without induction) and $\mathcal{M}$ is a submodel of $\mathcal{N}$, they have the same arithmetically definable elements. This can be again defined as an abstract property of a theory. However, in order for that property to hold it is not essential that we have a truth predicate to our disposal. Nevertheless, we can introduce an axiomatic theory of definability, $\textnormal{DEF}^-$, which indeed corresponds to that semantic property. So we can expand our initial question as follows: given a truth-related semantic property, find an axiomatic theory whose use is essential in ensuring that property. 
	
	As we already mentioned, imposing definability is in general not enough to define a predicate satisfying $\textnormal{UTB}^-$. This can be in fact rephrased by saying that in $\textnormal{DEF}^-$ one cannot define a predicate satisfying $\textnormal{UTB}^-$ (while preserving the arithmetical part of the language). Therefore, it becomes natural to ask about definability relations between theories corresponding to truth-like semantic properties. 
	
	The definability notions which we analyse, come in many flavours: we can consider them with or without parametres. Similarly, we can require that one theory defines another over every model, possibly with different formulae or we can require the definability to hold uniformly in the theory. Finally, we can require that the definability is non-uniform between models, but uniformly bounded in complexity. Those distinctions apply to both types of questions we discussed above: we can consider various definability notions of a theory corresponding to a semantic property or analyse distinct reductions between those theories. 
	
	Finally, it sometimes happen that the answer to an analysed question depends on the base theories. In a similar manner, the choice of the base theory may vastly simplify the arguments. In general, we will try to work in a general framework of arbitrary sequential theories, but in some cases we can get a clearer picture or more elegant proofs, when we accept some additional natural assumptions on the base theories (notably, we can choose $\textnormal{PA}$). This adds another dimension to our investigations.
	
The plan of the paper is as follows.
	In section 2 we introduce all the relevant notions, including the axiomatic theories of truth ($\textnormal{TB}$), \rem{definability ($\textnormal{DEF}$)} and satisfaction ($\textnormal{USB}$ or $\textnormal{UTB}$) in the general context of an arbitrary sequential theory. The theory $\textnormal{DEF}$ is introduced in this paper for the first time. Moreover, we state the definitions of two definability relations between theories, which we call syntactical and semantical definability. Finally we introduce abstract model-theoretical properties of general theories that will be used to characterize axiomatic theories of semantical notions. Each of the properties is introduced in two variants: uniform and non-uniform. 
	
	In section 3 each of the axiomatic theories is paired with the appropriate model-theoretical notion: we show that, up to syntactical definability, axiomatic theories of truth, definability
	and satisfaction can be characterized via the notions of imposing elementary equivalence, preserving definability and imposing elementarity, respectively (Theorem \ref{tw_impos_elem}). The theorems account for coordinate-free characterizations of these axiomatic theories, in the sense of \cite{VisserR}. In Theorems \ref{tw_nonuniform_def_tb} and \ref{tw_nonuniform_impos_elem_utb} we prove that the above characterization holds also for semantical definability and the non-uniform analogues of the model-theoretical properties.  
	
	Section 4 explores definability relations between various axiomatic theories of semantic notions. These results can be also viewed as  generalisations of some previously known non-definability results between the axiomatic theories of truth and satisfaction (see \cite[Corollary 3.8]{wcislyk_models_weak} and \cite[Theorem 5.9]{viss19enayat}). 

	We show that satisfaction is not definable from truth over any sequential base theory (Theorem \ref{tw_nondef_sat_in_def_tb}). This solves problem 5.10 in \cite{viss19enayat}. Then this picture is enriched with an axiomatic theory of definability ($\textnormal{DEF}$): we show that, except for some degenerate cases\footnote{We classify as \rem{"degenerate"} the examples of sequential theories which, roughly speaking, are inconsistent with the theory of extensional adjunctive sets.}, the theory situates itself strictly between $\textnormal{TB}$ and $\textnormal{USB}$ (Theorems \ref{tw_nondef_sat_in_def_tb} and \ref{tw_nondef_def_in_tb}). It is shown that each of the separations ($\textnormal{DEF}$ from $\textnormal{TB}$ and $\textnormal{USB}$ from $\textnormal{DEF}$) hold in the strict sense: each (non-degenerate) sequential theory has a model which can be expanded to a model of $\textnormal{TB}$ ($\textnormal{DEF}$) such that in the expanded model $\textnormal{DEF}$ ($\textnormal{USB}$, resp.) is not definable. The proof for $\textnormal{TB}$ vs. $\textnormal{DEF}$ case uses a construction of a model in which the definability hierarchy does not collapse. The construction works uniformly for any (non-degenerate) sequential theory $U$, and to our best knowledge this is an original result in the model theory of sequential theories (Lemma \ref{lem_hierarchical_model}).  As a corollary we conclude that, unless $U$ is degenerate, $\textnormal{DEF}$ does not have a restricted axiomatization modulo $U$. A similar argument shows that for every sequential $U$, $\textnormal{TB}$ does not have a restricted axiomatization modulo $U$, which solves a problem posed in \cite[Open Question 5.7]{viss19enayat}. In the final two subsections we study the definability relations between the above mentioned theories and two axiomatic theories of Skolem functions (uniform and non-uniform; Subsection \ref{subsect_skolem}) and the special

	 situation with $\textnormal{PA}$ as the base theory (Subsection \ref{subsect_PA}). In the former, we use Kaye-Kossak style results (from \cite{kossak_1990}, \cite{kossak_cor_to_1990} and \cite{kaye_model_char_PA}) about models of fragments of $\textnormal{PA}$ to construct models of $\textnormal{USB}$ in which there is no definable witness-picking function for arithmetical formulae (Theorems \ref{stw_nondef_H_usb} and \ref{tw_nondef_US_in_UTB}). In the latter, we show that various structural results about models of $\textnormal{PA}$ provide simpler and stronger (Subsection \ref{subsect_PA_def_inno}) separability arguments for $\textnormal{TB}$, $\textnormal{DEF}$ and $\textnormal{USB}$.
	
	In section 5 we study the property of imposing recursive saturation and  possible strengthenings of Kossak's theorem (Theorem \ref{tw_kossak}). Using a recursion-theoretic argument (involving an arithmetisation of a construction of an $\omega$-generic set intertwined with the Jump Inversion Theorem) we show that there is a theory in a finite language which imposes recursive saturation but does not syntactically define $\textnormal{UTB}$ (Theorem \ref{th_theory_finlang_with_rec_sat_without_utb}). To our best knowledge this is the first example of a theory in a finite language which defines $\textnormal{UTB}$ semantically but not syntactically. Secondly, we show that Kossak's Theorem does generalise to theories without full induction (but extending $\textnormal{PA}$): we prove that each sequential theory in a countable language which extends $\textnormal{PA}$ and imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation semantically defines $\textnormal{UTB}$ for $\mathcal{L}_{\textnormal{PA}}$ (Theorem \ref{th_recursive_saturation_implies_truth}).\footnote{Here in $\textnormal{UTB}$ we do not assume the induction scheme for formulae with the satisfaction predicate.} The proof is very different from the original Kossak's reasoning and uses iterated omitting types theorem in the spirit of \cite{casanovas_farre}. As a corollary we define a theory $\textnormal{RSAT}$ which is universal for imposing $\mathcal{L}_{\textnormal{PA}}$-recursive saturation in the following sense: a sequential theory $U$ in a countable language and extending $\textnormal{PA}$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation if and only if $U$ semantically defines $\textnormal{RSAT}$.
	
	\rem{Section 6 contains a list of open problems. Most of them are connected either to some questions in model theory of fragments of $\textnormal{PA}$ or interpretability and definability in finitely axiomatized theories.}
	

	\section{Preliminaries}\label{sect_prelim}
	
	\subsection{Model-theoretical properties}
	
	For general first-order theories the arithmetical $\Sigma_n\setminus\Pi_n$ hierarchy need not make much sense. In what follows we shall employ the quantifier alternation depth hierarchy, introduced in \cite{Buss2015} and in a similar context used in \cite{viss_sivs}.
	
	\begin{definicja}[Depth of quantifier alternation]\label{def_complexity}
		Let $\mathcal{L}$ be any first-order language and let $\textsc{AT}$ denote the set of atomic formulae of $\mathcal{L}$. $\Sigma_n^*(\mathcal{L})$ and $\Pi_n^*(\mathcal{L})$ are defined by simultaneous induction as follows  (below, and whenever it is clear from the context, we omit the reference to $\mathcal{L}$):
		\begin{align*}
			\Sigma^*_0 &= \Pi_0^* := \emptyset\\
			\Sigma_{n+1}^*&:= \textsc{AT}\ \ | \ \ \exists v \Sigma_{n+1}^* \ \ | \ \ \Sigma^*_{n+1}\wedge \Sigma^*_{n+1} \ \ | \ \ \Sigma^*_{n+1}\vee \Sigma^*_{n+1} \ \ | \ \ \neg\Pi^*_{n+1} \ \ | \forall v \Pi^*_n | \\
			\Pi_{n+1}^*&:= \textsc{AT}\ \ | \ \ \forall v \Pi_{n+1}^* \ \ | \ \ \Pi^*_{n+1}\wedge \Pi^*_{n+1} \ \ | \ \ \Pi^*_{n+1}\vee \Pi^*_{n+1} \ \ | \ \ \neg\Sigma^*_{n+1} \ \ | \exists v \Sigma^*_n | \\
        \Delta_{n+1}^*&:= \Sigma_{n+1}^*\cap \Pi_{n+1}^*
		\end{align*}
		For a formula $\phi$, $\Sigma^*(\phi)$ $(\Pi^*(\phi), \Delta^*(\phi))$  denotes the $\Sigma^*_n$ ($\Pi^*_n, \Delta_n^*$) complexity of $\phi$.

        We will need two more fine-grained measures of complexity of formulae. We call the first one \emph{depth} ($\textnormal{dp}$) and the second \emph{pure depth} ($\textnormal{pdp}$). In short, the depth of $\phi$ is the maximal number of connectives and quantifiers on a branch in the syntactic tree of $\phi$. The pure depth of $\phi$ is the maximal length of a branch in the syntactic tree of $\phi$, where terms occuring in $\phi$ are unravelled. Formally, we define $\textnormal{dp}$ and $\textnormal{pdp}$ recursively:
        \begin{align*}
        \textnormal{dp}(\phi) &= 0, \textnormal{ if } \phi\in \textsc{AT}\\
        \textnormal{dp}(\neg\phi)&= \textnormal{dp}(\exists x \phi) = \textnormal{dp}(\forall x \phi) = \textnormal{dp}(\phi)+1\\
        \textnormal{dp}(\phi\wedge\psi) &= \textnormal{dp}(\phi\vee\psi) = \max\{\textnormal{dp}(\phi),\textnormal{dp}(\psi)\}+1 
        \end{align*}
        Pure depth is defined first for terms: $\textnormal{pdp}(t)=0$, if  $t$ is a constant or a variable and $\textnormal{pdp}(f(t_1,\ldots,t_n)) = \max\{\textnormal{pdp}(t_1),\ldots,\textnormal{pdp}(t_n)\}+1.$ Then $\textnormal{pdp}(\phi)$ is defined as $\textnormal{dp}(\phi)$, except for the case of atomic formulae, where we put $\textnormal{pdp}(R(t_1,\ldots,t_n)) = \max\{\textnormal{pdp}(t_1),\ldots,\textnormal{pdp}(t_n)\}$.
	\end{definicja}
	
	In the paper we only consider first-order languages. If $\mathcal{M}$ is any model of a language $\mathcal{L}$, $A\subseteq M$, then $\mathcal{L}_A$ denotes the extension of $\mathcal{L}$ with constants naming every element of $A$. If $U$ is any first order theory, then $\mathcal{L}_U$ denotes its language. If $\mathcal{M}$ is any model and $\mathcal{L}$ any language, then $\mathcal{M}\restr{\mathcal{L}}$ denotes the $\mathcal{L}$-reduct of $\mathcal{M}$.
	
	
	
	\begin{definicja}
		Let $\mathcal{L}$ an arbitrary language.
		\begin{enumerate}
			\item $n\mhyphen \textnormal{Diag}(\mathcal{M})$ denotes the set of $\Sigma^*_n(\mathcal{L}_M)$ sentences, that are true in $\mathcal{M}$. We put $\textnormal{ElDiag}(\mathcal{M}) = \bigcup_{n\in\mathbb{N}}n\mhyphen \textnormal{Diag}(\mathcal{M})$. We write $\mathcal{M}\preceq_{n} \mathcal{N}$ as an abbreviation of $n\mhyphen\textnormal{Diag}(\mathcal{M})\subseteq n\mhyphen\textnormal{Diag}(\mathcal{N})$ and $\mathcal{M}\preceq \mathcal{N}$ for $\textnormal{ElDiag}(\mathcal{M})\subseteq \textnormal{ElDiag}(\mathcal{N})$.
			\item $n\mhyphen \textnormal{Th}(\mathcal{M})$ denotes the set of $\Sigma^*_n(\mathcal{L})$ that are true in $\mathcal{M}$.  We put $\textnormal{Th}(\mathcal{M}) = \bigcup_{n\in\mathbb{N}}n\mhyphen \textnormal{Th}(\mathcal{M})$. We write $\mathcal{M}\equiv_{n} \mathcal{N}$ as an abbreviation of $n\mhyphen\textnormal{Th}(\mathcal{M})= n\mhyphen\textnormal{Th}(\mathcal{N})$ and $\mathcal{M}\equiv \mathcal{N}$ for $\textnormal{Th}(\mathcal{M})= \textnormal{Th}(\mathcal{N})$.
			\item $n\mhyphen \textnormal{Def}(\mathcal{M})$ denotes the set of $\Sigma^*_n(\mathcal{L})$ definable elements of $\mathcal{M}$. We put $\textnormal{Def}(\mathcal{M}) = \bigcup_n n\mhyphen\textnormal{Def}(\mathcal{M})$.
			\item  $n\mhyphen \textnormal{DEF}(\mathcal{M})$ denotes the set $\set{\pair{\theta(x)}{a}}{\mathcal{M}\models \theta(a)\wedge \exists!x\theta(x)}$.  We put $\textnormal{DEF}(\mathcal{M}) = \bigcup_n n\mhyphen\textnormal{DEF}(\mathcal{M})$.
		\end{enumerate}   
	\end{definicja}
	
	\begin{definicja}
		Let $U$ be any theory and $\mathcal{L}$ be an arbitrary language.
		\begin{enumerate}
			\item We say that $U$ \emph{imposes $\mathcal{L}$-elementarity} (\emph{$\mathcal{L}$-elementary equivalence}) if for every $\mathcal{M}\models U$ there exists $n\in\mathbb{N}$ such that for all $\mathcal{N}\models U$, 
			\begin{align}\label{impos_elem_def}\tag{E$^{\mathcal{M}, \mathcal{N}}_n$}
				\mathcal{M}\preceq_{n}\mathcal{N} &\Rightarrow \mathcal{M}\restr{\mathcal{L}}\preceq\mathcal{N}\restr{\mathcal{L}}\\
				(\mathcal{M}\equiv_{n}\mathcal{N}&\Rightarrow \mathcal{M}\restr{\mathcal{L}} \equiv \mathcal{N}\restr{\mathcal{L}}). \label{impos_elem_equiv_def}\tag{EE$^{\mathcal{M},\mathcal{N}}_n$}
			\end{align}
			
			\item We say that $U$ \textit{uniformly imposes $\mathcal{L}$-elementarity} (\textit{$\mathcal{L}$-elementary equivalence}) if there is an $n$ such that for every $\mathcal{M},\mathcal{N}\models U$, \eqref{impos_elem_def} holds (\eqref{impos_elem_equiv_def} holds, respectively).
			
			\rem{	\item We say that $U$ \textit{imposes equality of $\mathcal{L}$-definables} (\textit{preserves $\mathcal{L}$-definability}) if for every $\mathcal{M}\models U$ there is $n\in\mathbb{N}$ such that for every $\mathcal{N}\models U$
				\begin{align}
					n\mhyphen\textnormal{Def}(\mathcal{M})= n\mhyphen\textnormal{Def}(\mathcal{N}) &\Rightarrow \textnormal{Def}(\mathcal{M}\restr{\mathcal{L}}) = \textnormal{Def}(\mathcal{N}\restr{\mathcal{L}}).\label{impos_equal_def}\tag{ED$^{\mathcal{M},\mathcal{N}}_n$}\\
					\bigl(n\mhyphen \textnormal{DEF}(\mathcal{M})= n\mhyphen\textnormal{DEF}(\mathcal{N}) &\Rightarrow \textnormal{DEF}(\mathcal{M}\restr{\mathcal{L}}) = \textnormal{DEF}(\mathcal{N}\restr{\mathcal{L}})\bigr) \label{preserv_def}\tag{PD$^{\mathcal{M},\mathcal{N}}_n$}
				\end{align}
			}	
			\item We say that $U$ \textit{uniformly imposes equality of $\mathcal{L}$-definables} (\textit{preserves $\mathcal{L}$-definability}) if there is an $n$ such that for every $\mathcal{M},\mathcal{N}\models U$, \eqref{impos_equal_def} holds (\eqref{preserv_def} holds, respectively).
			
			\item We say that $U$ \textit{imposes recursive $\mathcal{L}$-saturation} if for every $\mathcal{M}\models U$, $\mathcal{M}\restr{\mathcal{L}}$ is recursively saturated.
		\end{enumerate}
	\end{definicja}
	
	\subsection{Various grades of definability}
	
	In what follows the definitions of translation and interpretation are borrowed from \cite{viss_sivs}. We use $K: U\lhd V$ to denote the fact that $K$ is a relative interpretation of $U$ in $V$. $id_U$ denotes the identity interpretation $U\lhd U$ and we omit the reference to $U$ if it is clear from context. Let $\textnormal{Th}eta_0$, $\textnormal{Th}eta_1$ be two signatures and $\mathcal{L}$ a language. We say that the translation $\tau:\textnormal{Th}eta_0 \rightarrow \textnormal{Th}eta_1$ is $\mathcal{L}$-conservative if for every formula $\phi\in\mathcal{L}$, $\phi^{\tau}=\phi$ and we say that $\tau$ is direct if it is one-dimensional, unrelativized and it translates identity to identity.
	
	\begin{definicja}
		We say that $U$ \emph{syntactically defines} $V$ \textit{modulo} $\mathcal{L}$, $V\leq_{\mathcal{L}} U$, if $U$ interprets $V$ via a direct, parameter-free and $\mathcal{L}$-conservative interpretation.
		
		We say that $U$ \rem{\emph{semantically defines} $V$ \textit{modulo} $\mathcal{L}$, $V\leq_{\mathcal{L}}^m U$} if for every $\mathcal{M}\models U$, $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $V$ modulo $\mathcal{L}_{M}$.
	
		
		We say that $U$ \emph{semantically parameter-free defines $V$ modulo} $\mathcal{L}$ if every consistent and complete extension of $U$ syntactically defines $V$ modulo $\mathcal{L}$. 
	\end{definicja}
	
	All the definability results in this paper consider the situation in which the defined-modulo-$\mathcal{L}$ theory is formulated in a language extending $\mathcal{L}$ with a single (at most binary) predicate $R$. In such a context it is easy to see that $U$ \textit{syntactically defines} $V$ \textit{modulo $\mathcal{L}$} if and only if there is a formula $\phi_R(\bar{x})\in\mathcal{L}_U$ such that for every $\Phi$-axiom of $V$
	\[U\vdash \Phi[\phi_R(\bar{t})/R(\bar{t})],\]
	where $\Phi[\phi_R(\bar{t})/R(\bar{t})]$ denotes the result of substituting $\phi_R(\bar{t})$ for each occurrence of $R(\bar{t})$, perhaps preceded by renaming of the bounded variables in $\phi_R(\bar{t})$ so as to avoid unwanted variable capture. 
	
	\begin{uwaga}
		It is very easy to observe that if $U$ syntactically defines $V$, then $U$ semantically defines $V$ and that this reverses if $V$ is finite. However, in a general context, it is possible for $U$ to semantically, but not syntactically define $V$. In such a scenario, in every model $\mathcal{M}$ of $U$ one can define intepretations for the predicates in $\mathcal{L}_V$ so as to turn $\mathcal{M}$ into a model of $V$, but there is no single fixed interpretation that works across all models. Our paper provides many examples of this phenomenon in the realm of axiomatic theories of semantical notions.
	\end{uwaga}
	
	

	
	\subsection{Axiomatic theories of semantical notions}\label{sect_prelim_truth}
	
	An axiomatic theory of truth (satisfaction, definability,...) splits into two parts: the base theory and some axioms specific for the notion of truth. An important restriction is that the syntax is encoded uniquely by the base theory. For the very basic theories of truth studied in this paper to make sense already very moderate syntax theory is sufficient: as shown in \cite{viss19enayat}, theories of truth make sense already for theories which are able to interpret the basic theory of successor and theories of satisfaction make sense over Vaught theories. We shall start from a stronger assumption that the base theory is sequential, which already covers a wide range of important first-order theories.   
	
	\subsubsection{Sequential theories}
	
	A theory is sequential if it admits a reasonably well-behaved notion of a finite sequence. More precisely: a sequential theory needs to prove that there exists an empty sequence and that every sequence $s$ can be extended by appending a given element from the universe at the end of $s$. Here comes the formal definition:
	
	\begin{definicja}[Adjunctive sets, sequentiality]\label{defi_sekwencyjność}
		The theory $\textsc{AS}$ is formulated in the language with one binary relational symbol $\in$ and has as axioms
		\begin{itemize}
			\item[AS1] $\exists x \forall y \bigl(y\notin x\bigr)$.
			\item[AS2] $\forall x \forall y \exists z \forall w \bigl(w\in z \equiv w\in x \vee w = y\bigr)$.
		\end{itemize}
		A theory $U$ is \emph{sequential} if there is a direct interpretation of $\textsc{AS}$ in $U$. The translation of $\in$ under this interpretation will be denoted $\in_U$. A model $\mathcal{M}$ is \emph{sequential} if $\textnormal{ElDiag}(\mathcal{M})$ is sequential. We write $\in_{\mathcal{M}}$ instead of $\in_{\textnormal{ElDiag}(\mathcal{M})}$. If $\mathcal{M}$ is sequential and $c\in M$, then $c^{\mathcal{M}}$ denotes the set $\set{a\in M}{\mathcal{M}\models a\in_{\mathcal{M}} c}$.
		
		For later purposes let us introduce also the theory of \textit{adjunctive sets with extensionality}, ASE, which is an extension of AS with the axiom $\forall x\forall y \bigl(\forall z (z\in x\equiv z\in y)\rightarrow x=y\bigr)$.
	\end{definicja}
	
	In this paper we shall restrict ourselves to sequential theories which directly interpret $\textsc{AS}$ via a parameter-free interpretation.
	We leave the problem of adding parameters for further investigations.
	
	Let us recall some prominent sequential theories: $\textnormal{PA}$ denotes Peano Arithmetic which we take to be formulated in the language $\mathcal{L}_{\textnormal{PA}}$ of ordered rings $\was{0,1,+,\times, <}$. I$\Sigma_n$ denotes the fragment of $\textnormal{PA}$ consisting of axioms of induction uniquely for formulae in $\Sigma_n$ form (according to the standard definition in which $\Sigma_0$ ($\Delta_0$) consists of all formulae in which all quantifiers are bounded) and B$\Sigma_n$ extends I$\Delta_0$ with collection axioms for $\Sigma_n$ formulae. Abusing the notation, we use $\textnormal{EA}$ to denote the theory in the language $\mathcal{L}_{\textnormal{PA}}$ extending $I\Delta_0$ with the axiom $\exp$ saying that the exponential function is total. All the details and basic facts about these theories can be found in \cite{kaye} and \cite{hapu98}. Finally, $S^1_2$ is the Buss's weak arithmetic of P-Time computability (consult \cite[Chapter V.4.b, Definition 4.4]{hapu98} for details).
	
	The notion of sequentiality is extensively discussed e.g. in \cite{viss_sivs}. Two most important for the current project features of sequential theories are summarized in the following two facts (Fact \ref{sequentiality_arithmetic} and Fact \ref{fakt_partial_truth}). 
	
	\begin{fakt}\label{sequentiality_arithmetic}
		If $U$ is sequential, then $U$ relatively interprets $S^1_2$ via a one-dimensional, parameter-free interpretation (but we allow the equality to be re-defined).
	\end{fakt} 
	
	To see how this is possible, observe that in AS one can first interpret ASE (by introducing new identity relation which glues together sets with the same elements). Then inside this interpretation one can define von Neumann ordinal numbers in the standard way. By restricting the domain to those ordinals on which multiplication and addition behaves nicely, one obtains a relative interpretation of Robinson's arithmetic $Q$. The fact that $Q$ interprets $S^1_2$ is well-known (see e.g. \cite{FerrQ}). 
	
	\begin{konwencja}\label{konwencja_arytmetyka_w sekwencji}
		We make use of the following abbreviations:
		\begin{itemize}
			\item We assume fixed G\"odel coding of languages in consideration. For a fixed formula $\phi$, $\qcr{\phi}$ denotes the G\"odel code of $\phi$.
			\item $\num{n}$ denotes the binary numeral naming $n$, to wit, the expression:
			\[\num{a_0} + \num{2}\cdot (\num{a_1} + \num{2}\cdot (\num{a_2} + \ldots(\num{a_{k-1}} + \num{2}\cdot \num{a_{k}})\ldots)),\] 
			where $a_i\in\was{0,1}$, $\num{0} = 0$, $\num{1} = 1$ and $\num{2} = (1+1)$ and $(a_i)_{i\leq k}$ is a binary expansion of $n$.
			\item Throughout the paper, when working in a sequential theory $U$ with a fixed interpretation $N$ of $S^1_2$, $E$ shall always denote the definable  equivalence relation  which is used by $N$ to translate the identity relation from the arithmetical signature. For any $n\in\omega$, we  write $n(x)$ for the $N$-translation of the formula $x = \num{n}$. We stress that, in the context of a general sequential theory, $\phi(\num{n})$ should be understood contextually as $\exists x \bigl(n(x) \wedge \phi(x)\bigr)$, where $n(x)$ is a predicate expressing the property of "being the $n$-th ordinal". We stress that $n(x)$ need not define any particular object, although it uniquely determines an $E$-equivalence class. Putting together this and the previous conventions, $\num{\qcr{\phi}}$ will denote a predicate corresponding to the G\"odel code of a formula $\phi$.
			\item Similarly, in the context of a sequential theory $U$ and $N: S^1_2\lhd U$, we shall use arithmetical predicates such as the ordering ($<$), "$x$ is a sentence of a language $\mathcal{L}$" ($\textnormal{Sent}_{\mathcal{L}}$), "$x$ is a formula of a language $\mathcal{L}$" ($\form_{\mathcal{L}}$), "$x$ is a proof of $y$ in pure first order logic" ($\textnormal{Proof}_{\emptyset}(x,y)$), "$x$ is a $\Sigma^*_n$ complexity of $\phi$" ($x=\Sigma_n^*(\phi)$), ''$\alpha$ is an assignment'' ($\alpha\in\textnormal{Asn}$) having in mind their $N$-translations to the language $\mathcal{L}_U$. We also assume that these predicates apply uniquely to members of the domain of $N$.
			\item To keep the good balance between precision and readability, we often abbreviate the use of a syntactic operation by using $\qcr{\cdot}$ (stretching the notation introduced above). For example if $\phi$ is understood to be a sentence, then $\qcr{\exists x \phi}$ will denote the result of prefixing $\phi$ with an existential quantifier and then variable $x$. 	 For substitutions of binary numeral we use the dot notation: $\qcr{\phi(\dot{x}/v)}$ denotes the result of substituting the binary numeral naming $x$ for the variable $v$ in $\phi$. We stress that we often treat $\qcr{\phi(\dot{x}/v)}$ as a function in three variables, $x$, $v$ and $\phi$ and skip the reference to $v$ if it is clear from context.
		\end{itemize}	
		
	\end{konwencja}
	
	
	
	
	
	\begin{fakt}\label{fakt_partial_truth}
		If $U$ is a sequential theory, then for each $n$ there is a formula $\textnormal{Sat}_n(x,y)$ which, provably in $U$ satisfies the Tarskian compositional clauses for formulae of complexity $\Delta^*_n$ whose pure depth belong to a certain $U$-provable cut $J$.
	\end{fakt}
    More precisely, for a fixed sequential theory $U$ in a finite language $\mathcal{L}$, $\textnormal{CS}^-(\mathcal{L})(\phi)$ denotes the following formula of $\mathcal{L}\cup S$, where $S$ is a fresh binary predicate (the initial disjunction $\bigvee_{R\in \mathcal{L}}$ and $\bigvee_{f\in\mathcal{L}}$ range over all relational symbols and all function symbols from $\mathcal{L}$, respectively (we treat constants as $0$-ary function symbols)):
    \begin{align*}
    \forall \alpha\in\textnormal{Asn}\bigl[S(\phi,\alpha) \equiv& \bigl[\bigvee_{R\in \mathcal{L}}\exists v_0,\ldots, v_n \bigl(\phi = \qcr{R(v_0,\ldots,v_n)}\wedge R(\alpha(v_0),\ldots,\alpha(v_n)\bigr)  \\
    &\vee \bigvee_{f\in \mathcal{L}}\exists v_0,\ldots, v_n \bigl(\phi = \qcr{v_{0} = f(v_1,\ldots,v_n)}\wedge \alpha(v_0) = f(\alpha(v_1),\ldots,\alpha(v_n))\bigr)\\
    &\vee \exists \phi_0,\phi_1\bigl(\phi = \qcr{\phi_0\wedge\phi_1}\wedge (S(\phi_0,\alpha)\wedge S(\phi_1,\alpha))\bigr)\\
    &\vee \exists \phi_0,\phi_1\bigl(\phi = \qcr{\phi_0\vee\phi_1}\wedge (S(\phi_0,\alpha)\vee S(\phi_1,\alpha))\bigr)\\
    &\vee \exists \phi_0 \bigl(\phi = \qcr{\neg\phi_0}\wedge \neg S(\phi_0,\alpha)\bigr)\\
    &\vee \exists \phi_0\exists v_0\bigl(\phi = \qcr{\forall v_0}\wedge \forall\beta \bigl(\beta\sim_{v_0}\alpha \rightarrow S(\phi_0,\beta)\bigr)\\
    &\vee \exists \phi_0\exists v_0\bigl(\phi = \qcr{\exists v_0}\wedge \exists\beta \bigl(\beta\sim_{v_0}\alpha \wedge S(\phi_0,\beta)\bigr)\bigr]\bigr].
    \end{align*}
	The results of \cite{viss_sivs}[Section 2] show that for every $n$ there exists a $U$-provable cut $J_n$ and a formula $\textnormal{Sat}_n(x,y)$ such that
   \[U\vdash \forall \phi\bigl(J_n(\textnormal{pdp}(\phi))\wedge \Delta^*_n(\phi)\rightarrow \textnormal{CS}^-(\mathcal{L})(\phi^{te})[\textnormal{Sat}_n(x,y)/S(x,y)]\bigr),\]
	where $\phi^{te}$ is the canonical formula equivalent to $\phi$, in which term symbols occur uniquely in the context $y=f(x)$, where $y$ and $x$ are variables. In what follows, $\textnormal{SAT}^{x,y}_n[\psi]$ denotes the formula 
 \[\forall \phi\bigl(J_n(\textnormal{pdp}(\phi))\wedge \Delta^*_n(\phi)\rightarrow \textnormal{CS}^-(\mathcal{L})(\phi^{te})[\psi(x,y)/S(x,y)]\bigr)\]
	We note that $\textnormal{SAT}_n^{x,y}[\psi]$ might contain free variables, if $\psi$ has some free variables other that $x$ and $y$. The last definition generalizes the notion of a coded set from the context of fragments of $\textnormal{PA}$ to arbitrary sequential theories.
	\begin{definicja}\label{defi_kodowanie}
		Let $\mathcal{M}$ be a sequential model and $K:S^1_2\lhd \textnormal{ElDiag}(\mathcal{M})$. We say that a set $A\subseteq \omega$ is \emph{coded} in $\mathcal{M}$ if for some $c\in M$ and every $n\in\omega$, $\mathcal{M}\models \exists x \bigl(n(x)\wedge x\in_{\mathcal{M}} c\bigr)$ if and only if $n\in A$.
	\end{definicja}
	
	
	\subsubsection{Truth, satisfaction, definability}
	
	In this section we have a sequential theory $U$ in the background, together with the distinguished one-dimensional parameter-free interpretation $K:S^1_2\lhd U$. We assume that the language of $U$ is r.e. and the codes of formulae are given by this interpretation. Hence $\qcr{\phi}$ denotes the natural number coding $\phi$ and $\num{\qcr{\phi}}$ is the predicate picking the $E$-equivalence class corresponding to $\qcr{\phi}$:
	
	\paragraph{Truth} $\textnormal{TB}_K(\mathcal{L})$ extends $U$ with all axioms of the form
	\[T(\num{\qcr{\phi}})\equiv \phi,\]
	where $\phi$ is a $\mathcal{L}$-sentence and $T$ is a fresh unary predicate.	
	
	\paragraph{Definability}
	
	$\textnormal{DEF}_K(\mathcal{L})$ extends $U$ with all axioms of the form:
	\[\forall y \bigl(D(\num{\qcr{\phi(x)}}, y)\equiv \exists! x \phi(x)\wedge \phi(y)\bigr),\]
	for $\phi\in\mathcal{L}$ and $D$- a fresh binary predicate.
	
	\paragraph{Satisfaction}  $\textnormal{USB}_K(\mathcal{L})$ extends $U$ with all axioms of the form
	\[\forall x \bigl(S(\num{\qcr{\phi}}, x)\equiv \phi(x)\bigr),\]
	where $\phi$ is a $\mathcal{L}$-formula and $S$ is a fresh binary predicate.
	
	\begin{uwaga}
		The reference to $U$ in $\textnormal{TB}_K$, $\textnormal{DEF}_K$ and $\textnormal{USB}_K$ is hidden in the interpretation $K$: as in \cite{viss_sivs} we take both the interpreting and the interpreted theory to be parts of data needed to specify the interpretation.
	\end{uwaga}
	
	\begin{uwaga}\label{uwaga_twarze_utb}
		For sequential theories $\textnormal{USB}_K$ is inter-definable with the following theory $\textnormal{USB}_K^{<\infty}$, which extends $U$ with all axioms of the form:
		
		\[\forall \alpha \bigl(\textnormal{Asn}(\phi,\alpha)\rightarrow S(\num{\qcr{\phi}}, \alpha)\equiv \phi[\alpha]\bigr),\]
		where $\textnormal{Asn}(\phi,\alpha)$ means that $\alpha$ is an assignment for $\phi$ and $\phi[\alpha]$ denote a formula
		\[\exists x_1,\ldots,x_n (\bigwedge_{i\leq n}\alpha(v_i) = x_i \wedge \phi[x_1/v_1,\ldots, x_n/v_n]),\]
		where $v_0,\ldots,v_n$ are all free variables of $\phi$. 
		
		Moreover, if $\mathcal{L}$ extends the language of arithmetic and $K = id$, then $\textnormal{USB}_K(\mathcal{L})$ mutually syntactically definable modulo $\mathcal{L}$ with the theory $\textnormal{UTB}_K(\mathcal{L})$, which extends $U$ with all axioms of the form $\forall x \bigl(T(\qcr{\phi(\dot{x})})\equiv \phi(x)\bigr),$ for $\phi(x)\in \mathcal{L}$. 
		
	\end{uwaga}
	

	
	\begin{uwaga}
		Theories $\textnormal{TB}$ and $\textnormal{UTB}$ have been studied in the literature, mostly in the context of Peano Arithmetic, $\textnormal{PA}$. For such a base theory, normally $\textnormal{TB}$ and $\textnormal{UTB}$ denote extensions of $\textnormal{TB}_{id}$ and $\textnormal{UTB}_{id}$ with the induction scheme extended to all formulae of $\mathcal{L}_{\textnormal{TB}}$ (see e.g. \cite{hal11}). Theories which are based only on the T-biconditionals are often called $\textnormal{TB}^-$ ($\textnormal{UTB}^-$) or $\textnormal{TB}\restr{}$ ($\textnormal{UTB}\restr{}$).
	\end{uwaga}

	\begin{uwaga}
		The term "definability" is used in three different contexts in the current paper. First of all, given a model $\mathcal{M}$, an element $a\in M$, or a subset $A\subseteq M$ can be definable in $\mathcal{M}$. In such contexts "definability" has its standard meaning known from basic model-theory. Secondly, a theory $U$ can be syntactically or semantically definable in another theory $V$. For the sake of precision we always speak of theories (and not models) and qualify the definability to be either semantic or syntactic. Thirdly, we consider the axiomatic theory of definability, $\textnormal{DEF}$.
	\end{uwaga}
	
	\section{Model-theoretical characterizations of semantical predicates}
	
	It is very easy to check the following properties of our target axiomatic theories:
	
	\begin{stwierdzenie}
		Let $U$ be any sequential $\mathcal{L}$-theory and $N: S^1_2\lhd U$.
		\begin{enumerate}
			\item $\textnormal{TB}_N$ uniformly imposes $\mathcal{L}$-elementary equivalence.
			\item $\textnormal{DEF}_N$ uniformly preserves $\mathcal{L}$-definability.
			\item $\textnormal{USB}_N$ uniformly imposes $\mathcal{L}$-elementarity.
		\end{enumerate}
	\end{stwierdzenie}
	
	The next theorem says that each of the above model-theoretical properties characterizes the respective theory up to syntactical definability.
	
	\begin{tw}\label{tw_impos_elem}
		Suppose that $U$ is an r.e. sequential theory in a finite language and let $N: S^1_2\lhd U$. Then
		\begin{enumerate}
			\item if $U$ uniformly imposes $\mathcal{L}$-elementarity, then $U$ syntactically defines $\textnormal{USB}_N(\mathcal{L})$ modulo $\mathcal{L}$.
			\item if $U$ uniformly preserves $\mathcal{L}$-definability, then $U$ syntactically defines $\textnormal{DEF}_N(\mathcal{L}$) modulo $\mathcal{L}$.
			\item if $U$ uniformly imposes $\mathcal{L}$-elementary equivalence, then $U$ syntactically defines $\textnormal{TB}_N(\mathcal{L}$) modulo $\mathcal{L}$.
		\end{enumerate}
	\end{tw}
	
	We start with a lemma which is purely model-theoretical. We say that a formula $\phi(x)\in\mathcal{L}$ is an $\mathcal{L}$-definition if for some formula $\psi(x)$, $\phi(x):= \psi(x)\wedge \forall y\neq x \neg\psi(y)$.
	
	\begin{lemat}\label{lem_main_impos_elem}
		Let $U$ be any theory.
		\begin{enumerate}
			\item If $n\in\omega$ witnesses that $U$ uniformly  imposes $\mathcal{L}$-elementarity , then for every $\mathcal{L}$-formula $\phi(\bar{x})$ there exists a $\Sigma^*_n(\mathcal{L}_U)$ formula $\theta_{\phi}(\bar{x})$ such that $U\vdash \forall x\bigl(\theta_{\phi}(\bar{x})\equiv \phi(\bar{x})\bigr).$
			\item If $n\in\omega$ witnesses that $U$ uniformly preserves $\mathcal{L}$-definability, then for every $\mathcal{L}$-definition $\phi(x)$ there exists a $\Sigma^*_n(\mathcal{L}_U)$ formula $\theta_{\phi}(x)$ such that $U\vdash \forall x\bigl(\theta_{\phi}(x)\equiv \phi(x)\bigr).$
			\item If $n\in\omega$ witnesses that $U$ uniformly imposes $\mathcal{L}$-elementary equivalence, then for every $\mathcal{L}$-sentence $\phi$ there exists a $\Sigma^*_n(\mathcal{L}_U)$-sentence $\theta_{\phi}$ such that $U\vdash \theta_{\phi}\equiv \phi.$
		\end{enumerate} 
	\end{lemat}
	\begin{proof}
		We show the argument for $\mathcal{L}$-elementarity, the rest of them being analogous. Fix $U$, $n$ and $\phi(x)$ (without loss of generality we can assume that $\phi$ has a single free variable). If $\phi(x)$ is inconsistent with $U$, then we know what to do. Otherwise, let $\mathcal{M}\models U$ be such that for some $a$, $\mathcal{M}\models \phi(a)$. Since $n$ witnesses that $U$ imposes $\mathcal{L}$-elementarity, then
		\[U + n\mhyphen \textnormal{Diag}(\mathcal{M})\vdash \phi(a).\]
		Consequently, there exists a $\Sigma^*_n(\mathcal{L}_U)$ sentence $\theta''_{\phi}(a,\bar{b})\in n\mhyphen \textnormal{Diag}(\mathcal{M})$ with parameters $a,\bar{b}\in M$ such that (we assume that $a$ and $\bar{b}$ are disjoint)
		\[U\vdash \theta''_{\phi}(a,\bar{b})\rightarrow \phi(a).\]
		We may safely assume that $a,\bar{b}$ do not belong to the language of $U$. It follows that for $\theta'_{\phi}(x):= \exists \bar{y}\theta''_{\phi}(x,\bar{y})$ we have
		\[U\vdash \forall x \bigl(\theta'_{\phi}(x)\rightarrow \phi(x)\bigr).\]
	

		Let $A:= \set{\psi(x)\in\Sigma^*_n(\mathcal{L}_U)}{U\vdash \forall x(\psi(x)\rightarrow \phi(x))}$. We claim that for some $\psi_0,\ldots,\psi_k\in A$ we have
		\[U\vdash \phi(x)\rightarrow \bigvee_{i\leq k}\psi_i(x).\]
		Suppose not. Then $U+\phi(b) + \set{\neg\psi(b)}{\psi(x)\in A}$ is consistent ($b$ is a fresh constant). Let $\mathcal{M}$ be any model of this theory. We claim that $U+n\mhyphen \textnormal{Diag}(\mathcal{M})+\neg\phi(b)$ is consistent as well. Indeed, for if not, then for some $\theta(x,\bar{y})$ such that $\theta(b,\bar{c})\in n\mhyphen \textnormal{Diag}(\mathcal{M})$
		\[U\vdash \forall x\bigl(\exists \bar{y} \theta(x,\bar{y})\rightarrow \phi(x)\bigr).\]
		However, then $\exists\bar{y}\theta(x,\bar{y})\in A$, hence $\mathcal{M}\models \neg\exists \bar{y}\theta(b,\bar{y})$. This contradicts the fact that $\theta(b,\bar{c})\in n\mhyphen \textnormal{Diag}(\mathcal{M})$. Hence $U+n\mhyphen \textnormal{Diag}(\mathcal{M})+\neg\phi(b)$ is consistent, which in turn contradicts the fact that $U$ uniformly imposes $\mathcal{L}$-elementarity.
	\end{proof}
	\begin{proof}[Proof of Theorem \ref{tw_impos_elem}]
		Similarly to the case of the above lemma, we focus on $\textnormal{USB}_N$. Let us define the following function $\sigma:\form_{\mathcal{L}}\rightarrow \textnormal{Proof}_U$:\footnote{$\textnormal{Proof}_U$ denotes the set of G\"odel codes of proofs from the axioms of $U$.}
		\begin{equation*}
			\sigma(\phi(x))= \min\set{p}{\exists \theta(x)\in\Sigma^*_n(\mathcal{L}_U)\textnormal{Proof}_U\bigl(p, \qcr{\forall x\bigl(\theta(x)\equiv \phi(x)\bigr)}\bigr)}.
		\end{equation*}
		In the above, $\textnormal{Proof}_U(x,y)$ is the canonical $\Sigma_1$-provability predicate for $U$. Lemma \ref{lem_main_impos_elem} makes it obvious that this function is total and recursive. For a formula $\phi(x)\in\mathcal{L}$, let $\theta_{\phi}(x)$ be the unique $\Sigma^*_n(\mathcal{L}_U)$-formula such that $\sigma(\phi(x))$ is a proof of $\forall x\bigl(\theta_{\phi}(x)\equiv \phi(x)\bigr).$ 
		The mapping $\phi\mapsto \theta_{\phi}$ is clearly total and recursive and we take $\rho(x,y)$ to be the formula which strongly represents this function in $U$. Clearly we may assume that $U$ proves that $\rho(x,y)$ is a partial function. As we have already discussed in Fact \ref{fakt_partial_truth}, there are a cut $J$ of $N$ and a satisfaction predicate $\textnormal{Sat}_n(s,x)$ such that $U$ proves that $\textnormal{Sat}_n(s,x)$ satisfies compositional clauses for all assignments (in the sense of $N$) $s$ and all $\Sigma^*_n(\mathcal{L}_U)$ formulae from $J$. Let us put:
		\begin{equation*}
			S_U(x,y):= \textnormal{Form}_{\mathcal{L}}(x) \wedge \exists z \bigl(\rho(x,z) \wedge \textnormal{Sat}_n(z,y)\bigr). 
		\end{equation*}

		Within $U$ we prove that for every $\phi(v)\in\mathcal{L}$ 
		\[U\vdash \forall x \bigl(S_U(\num{\qcr{\phi(v)}},x)\equiv \phi(x)\bigr).\]
		Fix $\phi(v)$ and let $\rho(\qcr{\phi(v)})=\qcr{\theta(v)}$. Working in $U$ observe that the following equivalences hold for an arbitrary $a$
		\begin{align*}
			S_U(\qcr{\phi(v)},a) &\iff \exists z \bigl(\rho(\num{\qcr{\phi(v)}},z) \wedge \textnormal{Sat}_n(z,a)\bigr) \\
			&\iff \textnormal{Sat}_n(\num{\qcr{\theta_{\phi}(v)}}, a)\\
			&\iff \theta_{\phi}(a)\\
			&\iff \phi(a)
		\end{align*}   

		The first one follows from the definition, the fact that $\phi(v)$ is an $\mathcal{L}$-formula and the representability of the set of G\"odel codes of formulae. The second one is obtained by the representability of $\rho$. The third one holds by the appropriate version of ''"It's snowing"-It's snowing'' lemma from \cite{viss_sivs}. The last one follows, since  $\phi(v)$ is equivalent to $\theta_{\phi}(v)$ in $U$.

	\end{proof}
	
	\begin{uwaga}
		The last argument was used for the first time by Albert Visser's in the proof of \cite[Theorem 3.11]{viss19enayat}.
	\end{uwaga}
	\begin{stwierdzenie}
		There is a theory $U\supseteq \textnormal{PA}$ in a countable language which uniformly imposes arithmetical elementarity but does not semantically define $\textnormal{TB}_{id}$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{stwierdzenie}
	\begin{proof}
		We define $U$. Apart from the axioms of $\textnormal{PA}$, for every formula $\phi(x)$, $U$ has a binary predicate $S_{\phi(x)}$ and an axiom
		\[\forall y \bigl(S_{\phi(x)}(\num{\qcr{\phi(x)}},y)\equiv \phi(y)\bigr).\]
		To see that $U$ does not semantically define $\textnormal{TB}_{id}$ observe first that each model $\mathcal{M}\models\textnormal{PA}$ expands to a model of $U$ in which for every $\phi$, $S_{\phi}$ is arithmetically definable without parameters. Indeed, fixing $\mathcal{M}$ and  $\phi(x)\in\mathcal{L}$, one can put $S_{\phi(x)}^{\mathcal{M}} = \set{\pair{\qcr{\phi(x)}}{a}}{a\in M\wedge \mathcal{M}\models \phi(a)}$. Hence if one starts with the standard model $\mathbb{N}\models \textnormal{PA}$ and let $\mathbb{N}^*$ be the above defined expansion of $\mathbb{N}$ to a model of $U$, there can be no definition of $\textnormal{TB}_{id}$ in $\mathbb{N}^*$.
	\end{proof}
	
	Now we pass to semantical definability. The following notion will come in handy:
	
	\begin{definicja}\label{def_definable_theories}
		Let $\mathcal{M}$ be a sequential model for a language $\mathcal{L}$ and $N: S^1_2\lhd \textnormal{ElDiag}(\mathcal{M})$. We say that an $\mathcal{L}_{\mathcal{M}}$-theory $V$ \emph{is representable in $\mathcal{M}$ w.r.t. $N$} (or \emph{representable in $(\mathcal{M},N)$ for short})  with a formula $\theta(x,y)\in\mathcal{L}_{\mathcal{M}}$ iff for every $\mathcal{L}$-formula $\phi(v)$ and every $a$
		\[\phi(a)\in V \iff \mathcal{M}\models \theta(\num{\qcr{\phi}},a).\]
		If $V$ is representable in $\mathcal{M}$ with $\theta$, then we put
		\[\textnormal{Proof}_{\theta}(y,x,z):= \exists \psi \bigl(\theta(\psi, z)\wedge \textnormal{Proof}_{\emptyset}(y,\qcr{\psi\rightarrow x})).\]
		We recall that $\textnormal{Proof}_{\emptyset}(y,x)$ is the ($N$-translation of the) standard decidable predicate strongly representing the relation "$y$ is a proof of $x$ in pure first-order-logic". Intuitively, $\textnormal{Proof}_{\theta}(y,x,z)$ expresses that $y$ is a proof of $x$ which may use as an axiom any formula $\phi(x)$, such that $\phi(z)\in V$, where $V$ is the theory represented by $\theta$. 
	\end{definicja}
	
	\begin{tw}\label{tw_nonuniform_def_tb}
		If $U$ is a sequential, r.e. theory in a finite language which imposes elementary equivalence (preserves $\mathcal{L}$-definability) and $N: S^1_2\lhd U$, then $U$ parameter-free semantically defines $\textnormal{TB}_N$ ($\textnormal{DEF}_N$) modulo $\mathcal{L}$.
	\end{tw}
	\begin{proof}
		We do the case for $\textnormal{DEF}_N$, the proof for $\textnormal{TB}_N$ being fully analogous. Suppose $U$ preserves $\mathcal{L}$-definability and fix $\mathcal{M}$ and a suitable $n$. Then $U + n\mhyphen \textnormal{Diag}(\mathcal{M})$ uniformly preserves $\mathcal{L}$-definability. Hence, by Lemma \ref{lem_main_impos_elem}, for every $\mathcal{L}$-definition $\phi(x)$ there is a $\Sigma^*_n(\mathcal{L}_{\mathcal{M}})$-formula $\theta_{\phi}(x,b)$ such that
		\[U + n\mhyphen \textnormal{Diag}(\mathcal{M})\vdash \forall x(\theta_{\phi}(x,b)\equiv \phi(x)),\]
		So for every $\phi$ there are formulae $\psi(b)\in n\mhyphen \textnormal{Diag}(\mathcal{M}), \chi\in U$ such that
		\begin{equation*}\label{U_prov_DEF_sem}
			\emptyset\vdash  \forall y (\chi\wedge\psi(y)\rightarrow \forall x(\theta_{\phi}(x,y)\equiv \phi(x))).
		\end{equation*}
		Observe that $n\mhyphen\textnormal{Diag}(\mathcal{M}) \cup U$ is (parameter-free) representable in $(\mathcal{M}, N)$, thanks to the existence of partial satisfaction predicates.
		Let $\zeta$ be the representing formula. 
		For an arbitrary formula $\phi$, let $\phi^d(x):= \phi(x)\wedge \forall y\neq x \ \phi(y)$. We write the definition $D_{\mathcal{M}}(\phi, a)$ in $\mathcal{M}$:
			\begin{multline*}
				\exists \theta(x,y)\exists p\exists b\bigl[\textnormal{Sat}_n^*(\theta,\pair{a}{b})\wedge  \forall y \neq a \neg \textnormal{Sat}_{n}^*(\theta,\pair{y}{b})\wedge  \textnormal{Proof}_{\zeta}(p, \qcr{\forall x (\theta(x,y)\equiv \phi^d(x))}, b) \wedge \\ \wedge \forall p'<p\forall \theta'<p\bigl(\theta'\in\Sigma_n^*(\mathcal{L}_U)\rightarrow \forall b\neg\textnormal{Proof}_{\zeta}(p', \qcr{\forall x (\theta'(x,y)\equiv \phi^d(x))},b)\bigr) \bigr].
			\end{multline*}	
		We prove that $D_{\mathcal{M}}(x,y)$ defines $\textnormal{DEF}_N$ in $\mathcal{M}$. Fix $\phi(x)$ and fix the least proof $p$ with the following property
			\begin{center}
				There are $b\in M$, $\chi\in U$ and $\psi(y),\theta(x,y)\in \Sigma^*_n(\mathcal{L}_U)$ such that $M\models \psi(b)$ and it holds that 
				$\textnormal{Proof}_{\emptyset}(p, \qcr{\forall y (\chi\wedge\psi(y)\rightarrow \forall x(\theta(x,y)\equiv \phi^d(x)))}).$
			\end{center}
		$p$ is well-defined by the well-foundedness of natural numbers. Let $\qcr{p}$ denote the G\"odel code of $p$. By definition
		\begin{multline*}
			\mathcal{M}\models \exists b\exists \theta \in\Sigma_n^*(\mathcal{L}_U)\textnormal{Proof}_{\zeta}(\num{\qcr{p}}, \qcr{\forall x (\theta(x,y)\equiv \phi^d(x))}, b) \wedge \\ \wedge \forall p'<\num{\qcr{p}}\forall \theta'<\num{\qcr{p}}\bigl(\theta'\in\Sigma_n^*(\mathcal{L}_U)\rightarrow \forall b\neg\textnormal{Proof}_{\zeta}(p', \qcr{\forall x (\theta'(x,y)\equiv \phi^d(x))},b)\bigr).
		\end{multline*}
		Moreover $\num{\qcr{p}}\in M$ is the unique, up to the $E$-equivalence relation, element of the domain of $\mathcal{M}$ for which the above holds. Assume now $\mathcal{M}\models D_{\mathcal{M}}(\num{\qcr{\phi}},a)$. Then clearly for some $b$ and standard $\theta\in\Sigma_n^*(\mathcal{L}_U)$, $\mathcal{M}\models \textnormal{Sat}_n^*(\theta,\pair{a}{b})\wedge  \forall y \neq a \neg \textnormal{Sat}_{n}^*(\theta,\pair{y}{b})$. Moreover, for the same $b$, $\theta$, $U+n\mhyphen\textnormal{Diag}(\mathcal{M})\vdash  \forall x (\theta(x,b)\equiv \phi^d(x))$, hence in $\mathcal{M}$, $\phi(x)$ defines $a$. Now assume that $\phi(x)$ defines $a$ in $\mathcal{M}$. Then obviously $\phi^d(x)$ defines $a$. Fix any $b$ and $\theta$ such that $\mathcal{M}\models \textnormal{Proof}_{\zeta}(\qcr{p}, \qcr{\forall x (\theta(x,y)\equiv \phi^d(x))}, b)$. By definition and the fact that both $p$ and $\theta(x,y)$ are standard,
		it follows that $\mathcal{M}\models \forall x (\theta(x,b)\equiv \phi^d(x))$. Hence $\theta(x,b)$ defines $a$ in $\mathcal{M}$ and $D_{\mathcal{M}}(\num{\qcr{\phi}},a)$ follows by ""It's snowing"-It's snowing" lemma for $\textnormal{Sat}_n$. 
	\end{proof}
	
	
	The lemma below provides a criterion for definability of $\textnormal{USB}_N$ in a sequential model. It will be used to characterize the satisfaction predicate up to semantical definability and, in the next section, separate satisfaction from truth and definability.
	
	
	\begin{lemat}\label{lem_main_model_theor_def}
		Let $\mathcal{M}$ be a model of a sequential theory
		for some finite language $\mathcal{L}'$ and $N: S^1_2\lhd \textnormal{ElDiag}(\mathcal{M})$. Then $\textnormal{USB}_N(\mathcal{L})$ is syntactically definable in $\textnormal{ElDiag}(\mathcal{M})$ modulo $\mathcal{L}$ iff for some $(\mathcal{M},N)$-representable, sequential $\mathcal{L}'_{\mathcal{M}}$-theory $V$ consistent with $\textnormal{ElDiag}(\mathcal{M})$, $V\vdash \textnormal{ElDiag}(\mathcal{M}\restr{\mathcal{L}})$.
	\end{lemat}
	\begin{proof}
		Assume that $\textnormal{ElDiag}(\mathcal{M})$ defines $\textnormal{USB}_N(\mathcal{L})$ via a formula $S'(\bar{x})$ and let $n$ be the complexity of $S'$. Let $V$ be the theory $\textnormal{USB}_N(\mathcal{L})[S'/S] + n\mhyphen \textnormal{Diag}(\mathcal{M})$. This theory is representable in $(\mathcal{M},N)$, by the existence of partial satisfaction predicates. Then clearly, for every $\phi(x)\in\mathcal{L}$ and all $a\in M$ we have 
		\begin{align*}
			\mathcal{M}\models\phi(a)&\iff \mathcal{M}\models S'(\num{\qcr{\phi(x)}}, a)\\
			&\iff S'(\num{\qcr{\phi(x)}}, a)\in n\mhyphen\textnormal{Diag}(\mathcal{M})\\
			&\iff V\vdash \phi(a).
		\end{align*}
		
		
		Assume now, $V\vdash \textnormal{ElDiag}(\mathcal{M}\restr{\mathcal{L}})$. It follows from this, the consistency of $V$ and the completeness of $\textnormal{ElDiag}(\mathcal{M})$ that for every $\phi(a)\in\mathcal{L}_{\mathcal{M}}$, $\phi(a)\in\textnormal{ElDiag}(\mathcal{M})$ iff there is $\psi(x)\in \mathcal{L}'$ such that $\psi(a)\in V$ and
		\[\emptyset\vdash \psi(x)\rightarrow \phi(x).\]
		Let $\theta$ represent $V$ in $\mathcal{M}$. Now, we can define $S_{\mathcal{M}}(x, c)$ as
		\[\exists y\bigl(\textnormal{Proof}_{\theta}(y,x,c) \wedge \forall z \bigl(z< y \rightarrow \neg \textnormal{Proof}_{\theta}(z,x,c)\bigr)\bigr) \]
		We check that this definition works, following the lines of the standard Rosser-style argument. Fix $\phi(v)\in\mathcal{L}$ and any  $a\in M$. First assume that $\phi(a)$ holds in $\mathcal{M}$. As above for some $\mathcal{L}'$-formula $\psi(v)$ such that $\psi(a)\in V$ 
		\[\emptyset\vdash \psi(v)\rightarrow \phi(v).\]
		Let $l\in \omega$ code this proof. Clearly then $\mathcal{M}\models \textnormal{Proof}_{\theta}(\num{l}, \num{\qcr{\phi(v)}}, a)$. We claim that for no $l'<l$ and for no $\xi$ such that $\mathcal{M}\models\textnormal{Sat}_{n}^*(\xi,a)$ we have $\mathcal{M}\models\textnormal{Proof}_{\theta}(\num{l'},\qcr{\xi\rightarrow\neg\phi(v)}, a)$.	
		Indeed, if this were the case, then $\xi$ would be a standard formula. Since $\mathcal{M}\models V$, we would have $\mathcal{M}\models \xi(a)$. However, obviously also $\xi(a)\rightarrow\neg\phi(a)$ is true in $\mathcal{M}$. This contradicts $\phi(a)$ being true in $\mathcal{M}$. Assume now that $\neg\phi(a)$ holds in $\mathcal{M}$. Then, arguing as previously we have that for some $l\in\omega$, $\mathcal{M}\models \textnormal{Proof}_{\theta}(\num{l}, \num{\qcr{\neg\phi(v)}}, a)$ and for all $l'<l$, $\mathcal{M}\models\neg \textnormal{Proof}_{\theta}(\num{l'}, \num{\qcr{\phi(v)}}, a)$. Hence, 
		\[\mathcal{M}\models \forall y\bigl(\textnormal{Proof}_{\theta}(y,(\num{\qcr{\phi(v)}},c) \rightarrow \exists z \bigl(z< y \wedge \textnormal{Proof}_{\theta}(z,(\num{\qcr{\neg\phi(v)}},c)\bigr).\]
		Hence $\mathcal{M}\models \neg S_{\mathcal{M}}(\num{\qcr{\phi}},a)$.
	\end{proof}
	
	The theorem below is a semantical variant of Theorem \ref{tw_impos_elem} (for $\textnormal{USB}$). We stress that neither of the theorems directly implies the other one. 
	\begin{tw}\label{tw_nonuniform_impos_elem_utb}
			If $U$ is an r.e. sequential theory in a finite language $\mathcal{L}'$ which imposes $\mathcal{L}$-elementarity, then $U$ semantically defines $\textnormal{USB}_N(\mathcal{L})$ modulo $\mathcal{L}$ for each interpretation $N:S^1_2\lhd U$.
	\end{tw}
	\begin{proof}
		Fix $U$, $N$ and let $\mathcal{M}\models U$. Since $U$ imposes $\mathcal{L}$-elementarity, there is an $n$ such that $U+n\mhyphen\textnormal{Diag}(\mathcal{M})\vdash\textnormal{ElDiag}(\mathcal{M}\restr{\mathcal{L}})$. Since $U$ is r.e., sequential and in a finite language, $U+ n\mhyphen\textnormal{Diag}(\mathcal{M})$ is representable in $(\mathcal{M},N)$. Hence by Lemma \ref{lem_main_model_theor_def}, $\mathcal{M}$ defines $\textnormal{USB}_N({\mathcal{L}})$.
	\end{proof}
	
	\section{Definability between axiomatic theories of truth, definability and satisfaction}
	
	\label{sec_definability_between_theories}
	
	Now, we turn to the definability relations between the theories of semantical notions in study. We say that $U$ has a definable element, if for some formula $\phi(x)$, $U\vdash \exists ! x \phi(x)$.
	
	\begin{stwierdzenie}\label{stw_latwa_definiowalnosc}
		For every sequential theory $U$ and interpretation $N: S^1_2\lhd U$, $\textnormal{TB}_N \leq_{\mathcal{L}_U} \textnormal{USB}_N$ and  $\textnormal{DEF}_N \leq_{\mathcal{L}_U}\textnormal{USB}_N$. Moreover, if $U$ has a definable element, then $\textnormal{TB}_N\leq_{\mathcal{L}_U}\textnormal{DEF}_N$.
	\end{stwierdzenie}
	\begin{proof}
		The definability $\textnormal{TB}_N \leq_{\mathcal{L}_U} \textnormal{USB}_N$ is trivial. Moreover, clearly
		\[D(\phi(x), y):= \exists! z S(\phi(x), z)\wedge S(\phi(x),y)\]
		witnesses the definability of $\textnormal{DEF}_N$ in $\textnormal{USB}_N$. For the remaining case, let $\theta(x)$ be a $U$-provable definition. Then, the formula
		\[T(\phi):= \exists y D(\qcr{\theta(x) \wedge \phi}, y),\]
		witnesses the definability of $\textnormal{TB}_N$ in $\textnormal{DEF}_N$. In the above, $\qcr{\theta(x)\wedge \phi}$ denotes the ($S^1_2$-representation of the) function with one free variable $\phi$ which, given a (G\"odel code of a) sentence $\phi$ returns the (G\"odel code of the) sentence $\theta(x)\wedge \phi$. This function need not be provably total in $U$, however for every standard sentence $\phi$ the value of the function exists and this all we need for the definability of $\textnormal{TB}_N$.
	\end{proof}
	
	In general, it is not true that $\textnormal{DEF}_N$ syntactically defines $\textnormal{TB}_N$ modulo $U$. This is due to the following simple observation:
	
	\begin{stwierdzenie}\label{stw_def_no_tb}
		If $U$ has a model in which no element is parameter-free definable, then $\textnormal{DEF}_N$ does not semantically define $\textnormal{TB}_N$ modulo $\mathcal{L}_U$.
	\end{stwierdzenie}
	\begin{proof}
		If $\mathcal{M}\models U$ and has no parameter-free definable elements, then $\textnormal{DEF}_N$ is definable in $\mathcal{M}$ via a parameter-free formula $\phi(x,y):= x\neq x \wedge y\neq y$. Clearly, $\textnormal{TB}_N$ cannot be parameter-free definable in $\mathcal{M}$, by Tarski undefinability theorem for $\textnormal{Th}(\mathcal{M})$.
	\end{proof}
	
	A concrete example of a sequential theory with a model with no parameter-free definable elements is AS. In particular,  $(V_{\omega}, \in)\sqcup (V_{\omega}, \in)$  is a model of AS in which no element is definable (for models $\mathcal{M}$ and $\mathcal{N}$, $\mathcal{M}\sqcup\mathcal{N}$ denotes their disjoint union), because every element can be moved by an automorphism.
	
	
	
	We proceed to separations between $\textnormal{TB}_N$, $\textnormal{USB}_N$ and $\textnormal{DEF}_N$. In the specific context where $U$ is a theory in an arithmetical language consistent with $\textnormal{PA}$ and $N$ is the identity interpretation, the separation between $\textnormal{TB}_N$ and $\textnormal{USB}_N$ was first shown in \cite{wcislyk_models_weak}. Below we prove that
	$\textnormal{USB}_N$ is not semantically definable in $\textnormal{DEF}_N$ which obviously generalizes also to the case of $\textnormal{TB}_N$.
	

	
	\begin{tw}\label{tw_nondef_sat_in_def_tb}
		Suppose $U$ is a consistent, sequential r.e. $\mathcal{L}$-theory and $N: S^1_2\lhd U$. Then neither $\textnormal{DEF}_N(\mathcal{L})$ nor $\textnormal{TB}_N(\mathcal{L})$ semantically defines $\textnormal{USB}_N(\mathcal{L})$ modulo $\mathcal{L}$.
	\end{tw}
	\begin{proof}
		We do the case of $\textnormal{DEF}_N(\mathcal{L})$, the argument for $\textnormal{TB}_N(\mathcal{L})$ being analogous. Fix $U,N$. Let $\mathcal{M}\models U$ be any $\mathcal{L}$-recursively saturated model. 
		
		
		
		By recursive saturation there is $c\in M$ such that for any $\phi(x)$ and any $a\in M$
		\[\mathcal{M}\models \pair{\num{\qcr{\phi(x)}}}{a}\in_{\mathcal{M}} c \equiv \exists!x\phi(x)\wedge \phi(a).\]
		In the above $\pair{\cdot}{\cdot}$ denotes the pairing function given by the direct interpretation of AS. Let $D^{\mathcal{M}}:= \set{\pair{a}{b}}{\mathcal{M}\models \pair{a}{b}\in_{\mathcal{M}} c}$. Then $(\mathcal{M},D^{\mathcal{M}})\models \textnormal{DEF}_N(\mathcal{L})$ and $D^{\mathcal{M}}$ is definable with a parameter in $\mathcal{M}$. Hence there cannot be any definition of $\textnormal{USB}_N(\mathcal{L})$ in $(\mathcal{M}, D^{\mathcal{M}})$ by Tarski's undefinability of truth theorem (applied to $\textnormal{ElDiag}(\mathcal{M})$). 
	\end{proof}
	
	Now, we shall separate $\textnormal{DEF}_N$ from $\textnormal{TB}_N$. Unlike in the case of $\textnormal{DEF}_N$ and $\textnormal{USB}_N$,

	 we cannot count for the undefinability result over all sequential theories, since some of them trivialize the behaviour of $\textnormal{DEF}_N$.
	\begin{przyklad}
		Define $\textsc{AS}_f$ to be the extension of AS with a sentence "$f$ is an automorphism which moves every element". Then, by the remark following Proposition \ref{stw_def_no_tb}, $\textsc{AS}_f$ is consistent. Clearly in every model $\mathcal{M}\models \textsc{AS}_f$, $f^{\mathcal{M}}$ is an automorphism of $\mathcal{M}$ which moves every element. Hence $\textnormal{DEF}_N$ is syntactically definable in $\textsc{AS}_f$ via any formula $\phi(x,y)$ with provably empty extension.
	\end{przyklad} 
	

As we already noted in Proposition \ref{stw_latwa_definiowalnosc},
in the case when $U$ admits a provably definable element, $\textnormal{TB}_N$ is contained in $\textnormal{DEF}_N$. We will shortly see, in Theorem \ref{tw_nondef_def_in_tb}, that under relatively mild assumptions this containment is in fact strict.  However, if $U$ has provably finitely many definable elements, then $\textnormal{DEF}_N$ does not exceed $\textnormal{TB}_N$:
	
	\begin{stwierdzenie}
		If for finitely many formulae $\theta_0,\ldots, \theta_n$, $U$ proves $\bigwedge_{i\leq n}\exists ! \theta_i(x)$ and for an arbitrary formula $\phi(x)$
		\[U\vdash \exists ! \phi(x)\rightarrow \forall x \bigl(\phi(x)\rightarrow \bigvee_{i\leq n}\theta_i(x)\bigr),\]
		then $\textnormal{TB}_N$ syntactically defines $\textnormal{DEF}_N$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $\was{\theta_i}$ as above and working in $\textnormal{TB}_N$, put
		\[D(\psi(x),y):= \form_U(\psi(x)) \wedge \bigvee_{i\leq n} \bigl[T(\qcr{\forall x (\psi(x)\equiv \theta_i(x))})\wedge \theta_i(y)\bigr].\]
		In the above, as in the proof of Proposition \ref{stw_latwa_definiowalnosc},  $\qcr{\forall x (\psi(x)\equiv \theta_i(x))}$ denotes the ($S^1_2$-representation of the) function which, given a (G\"odel code of a) formula $\psi(x)$ with a single free variable returns the (G\"odel code of the) sentence $\forall x (\psi(x)\equiv \theta_i(x))$.
	\end{proof}
	
	Also, it is fairly easy to convince oneself that for each $n$ there is a sequential theory which admits exactly $n$ definable elements. We shall show that if $U$ is a sequential, r.e. theory in a finite language $\mathcal{L}$ which for some $n$ has a model with infinitely many $\Sigma^*_n(\mathcal{L})$-definable elements then $\textnormal{TB}_N$ does not semantically define $\textnormal{DEF}_N$ modulo $\mathcal{L}$. Let us observe that each theory $U$ that admits a consistent extension which directly interprets ASE via a one-dimensional and parameter-free interpretation is of this form. 
	
	The idea of the proof is to construct a model $\mathcal{M}\models U$  with $c\in M$ such that 
	
	\begin{enumerate}
		\item $c$ codes the theory of $\mathcal{M}$,
		\item there is a partition $\was{M_i}_{i\in \omega}$ of $\mathcal{M}$ such that for every $n$ there exists an element $d_n\in \textnormal{Def}(\mathcal{M})$ which is not $\Sigma_n^*(\mathcal{L}_{M_n})$-algebraic in $\mathcal{M}$.
	\end{enumerate}
	This will ensure that for any $n$, the $\mathcal{L}_T$ model $(\mathcal{M},c^{\mathcal{M}})$ has an $\mathcal{L}_T$-elementarily equivalent, $\Sigma_n^*(\mathcal{L}_T)$-elementary extension which differs from $\mathcal{M}$ on definable elements. Moreover, $\textnormal{ElDiag}(\mathcal{M})$ does not syntactically define $\textnormal{DEF}_N$. In our construction we shall make use of flexible formulae.
	
	\begin{definicja}
		Let $U$ be any theory in a language $\mathcal{L}$. A formula $\theta(x)$ is $(n,k)$-flexible for $U$ iff for every $\mathcal{M}\models U$ and every $\Sigma^*_k(\mathcal{L})$ formula $\delta(x)$ there exists $\mathcal{M}\preceq_{n}\mathcal{N}$ such that $\mathcal{N}\models \theta(x)\equiv \delta(x)$. 
	\end{definicja}
	
	The following is a variation of \cite[Theorem 11, Section 2.3]{lindstrom_aspects}.
	
	\begin{stwierdzenie}\label{prop_flexible}
		If $U$ is a sequential, r.e. theory in a finite language, then for every $n,k$ there exists an $(n,k)$-flexible formula for $U$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $U$ and $n,k\in\omega$. Let $\textnormal{Proof}_{\theta}(y,x,z)$ be the provability predicate defined as in Definition \ref{def_definable_theories} for $\theta(x,z):= \textnormal{Sat}_{n+1}(x,z)\vee U(x)$ (where $U(x)$ is any decidable predicate which represents an axiom set of $U$ and $\textnormal{Sat}_{n+1}$ is a partial truth predicate for $\mathcal{L}_U$). Let $\rho'(y, \phi,\psi)$ be the formula
		\[\psi \in\Sigma^*_k(\mathcal{L}_U)\wedge\exists z\textnormal{Proof}_{\theta}(y, \qcr{\neg \forall x \bigl(\phi\equiv \psi\bigr)}, z),\]
		In the above, $\qcr{\neg \forall x \bigl(\phi\equiv \psi\bigr)}$ denotes the ($S^1_2$-representation of the) function which, given  (G\"odel codes of) formulae $\phi(x),\psi(x)$ (both having at most $x$-free) returns the (G\"odel code of the) sentence $\neg\forall x (\phi\equiv \psi)$. Finally put 
		\[\rho(y, \phi,\psi):=\rho'(y, \phi,\psi )\wedge \forall y'\forall \psi'\bigl(\pair{y'}{\psi'}<\pair{y}{\psi}\rightarrow \neg\rho'(y', \phi,\psi')\bigr).\]

		Using the diagonal lemma in $U$ define $\gamma(x)$ to be the formula such that
		\[U\vdash \gamma(x)\equiv \exists y\exists\psi\bigl(\rho(y,\num{\qcr{\gamma}},\psi)\wedge \textnormal{Sat}_{k}(\psi,x)\bigr).\]
		Now fix any $\mathcal{M}\models U$, any $\psi\in\Sigma^*_k(\mathcal{L}_U)$ and aiming at a contradiction assume that there is no $\Sigma^*_n(\mathcal{L}_U)$-elementary extension of $\mathcal{M}$ making $\forall x \bigl(\gamma(x)\equiv \psi(x)\bigr)$ true. It follows that $U+ (n+1)\mhyphen\textnormal{Diag}(\mathcal{M})\vdash \neg \forall x \bigl(\gamma(x)\equiv \psi(x)\bigr).$ Hence, for some $\chi\in (n+1)\mhyphen\textnormal{ElDiag}(\mathcal{M})$
		\[U\vdash \chi\rightarrow \neg \forall x \bigl(\gamma(x)\equiv \psi(x)\bigr).\]
		By existentially generalizing on the additional parameters from $\mathcal{M}$ we can assume that $\chi$ is in the language of $U$. Let us pick $\psi\in M$ and the proof $p\in M$ such that $\pair{p}{\psi}$ is minimal such that $\mathcal{M}\models\rho'(\num{\qcr{p}}, \num{\qcr{\gamma}},\num{\qcr{\psi}})$. Such a pair exists, by the least number principle in the well-founded part of $\mathcal{M}$. In particular, $p$ witnesses that for some $\chi'\in (n+1)\mhyphen \textnormal{Diag}(\mathcal{M})$, $U\vdash \chi'\rightarrow \neg\forall x (\gamma \equiv \psi)$. As previously we can assume that $\chi'$ contains no parameters. Then obviously $\mathcal{M}\models \rho(\num{\qcr{p}},\num{\qcr{\gamma}}, \num{\qcr{\psi}})$. Moreover, for any $y$ and $z$, if $\mathcal{M}\models \rho(y,\num{\qcr{\gamma}}, z)$, then $y$ is in the $E$-equivalence class corresponding to $\qcr{p}$
		and $z$ is in the $E$-equivalence class corresponding to $\qcr{\psi}$ (See Convention \ref{konwencja_arytmetyka_w sekwencji}). 
		
		It follows that $\mathcal{M}\models \forall x \bigl(\gamma(x)\equiv \textnormal{Sat}_{k}^*(\num{\qcr{\psi}},x)\bigr)$. Consequently, $\mathcal{M}\models \forall x \bigl(\gamma(x)\equiv \psi(x)\bigr)$. However, since $\mathcal{M}\models U + \chi'$, $\mathcal{M}\models \neg\forall x\bigl(\gamma(x)\equiv \psi(x)\bigr)$. 
	\end{proof}
	
	\begin{lemat}\label{lem_hierarchical_model}
		For every r.e. sequential theory $U$ in a finite language $\mathcal{L}$, every $n,k\in\omega$ and every model $\mathcal{M}\models U$ which contains infinitely many $\Sigma^*_k(\mathcal{L})$-definable elements there is an $\mathcal{N}\succeq_n\mathcal{M}$ and a decomposition $N = \bigcup_{m\in\omega} M_m$ such that for every $m,l\in\omega$ there is an element of $N$ which is parameter-free definable in $\mathcal{N}$ but not $\Sigma^*_l(\mathcal{L}_{M_m})$-algebraic.
	\end{lemat}
	\begin{proof}
		Fix $U$, $\mathcal{M}$ and $n,k$ as above. Without loss of generality assume that $k<n$. We shall define 
		\begin{itemize}
			\item a chain of models $\was{\mathcal{M}_i}_{i\in\omega}$;
			\item a sequence of formulae $\was{\theta_i(x)}_{i\in\omega}$;
			\item a sequence of numbers $\was{n_i}_{i\in\omega}$. 
		\end{itemize} 
		such that
		\begin{enumerate}
			\item $n_0 = n+1$ and for each $i$, $n_i<\Sigma^*(\theta_{i+1})<n_{i+1}$, where $\Sigma^*(\theta)$ denotes the $\Sigma^*_n$ complexity of $\theta$.
			\item $\mathcal{M}_0 = \mathcal{M}$ and for each $i$, $\mathcal{M}_i\preceq_{n_i}\mathcal{M}_{i+1}$ and $\mathcal{M}_i\models U$.
			\item for each $i$, $\mathcal{M}_{i+1}$ contains an element which is definable in $\mathcal{M}_{i+1}$ with $\theta_{i+1}(x)$ but not $\Sigma^*_{n_i}(\mathcal{L}_{M_i})$-algebraic (in $\mathcal{M}_{i+1}$).
		\end{enumerate}
		Assume that we have succeeded. Let $\mathcal{N} = \bigcup_{i\in\omega}\mathcal{M}_i$. Then it follows that for every $i\in\omega$, $\mathcal{M}_i\preceq_{n_i}\mathcal{N}$. Hence, the following follows
		\begin{itemize}
			\item $\mathcal{N}\models U$ and $\mathcal{M}\preceq_n \mathcal{N}$.
			\item if $d$ is definable in $\mathcal{M}_{i+1}$ by the formula $\theta_{i+1}$, then $d$ is definable with $\theta_{i+1}$ in $\mathcal{N}$ and, in $\mathcal{N}$, $d$ is not $\Sigma^*_{n_i}(\mathcal{L}_{\mathcal{M}_{i}})$-algebraic.
		\end{itemize}
		Now we show how to construct the three sequences. For $n=0$ we do what is necessary
		with $n_0$ and $\mathcal{M}_0$ and let $\theta_0(x)$ be any formula. Assume that our sequences are constructed up to $k$. We let $\theta_{k+1}$ be an $(n_k+1, n_k+1)$-flexible
		formula. Let $\textnormal{Th}:= A\cup B \cup C$ be a theory in the language $\mathcal{L}(\mathcal{M}_{k})\cup\was{d}$, where $d$ is a fresh constant and $A,B,C$ are defined:
		\begin{itemize}
			\item[$A.$]  $(n_k+1)\mhyphen\textnormal{Diag}(\mathcal{M}_k)$
			\item[$B.$] $\set{\exists^{\leq i}x\phi(x)\rightarrow \neg \phi(d)}{\phi(x)\in \Sigma_{n_k}^*(\mathcal{L}_{\mathcal{M}_k}), i\in \omega}$
			\item[$C.$] $\exists ! x \theta_{k+1}(x) \wedge \theta_{k+1}(d).$
		\end{itemize}
		We claim that $\textnormal{Th}$ is consistent. Indeed, fix any finite fragment $K$ of $Th$,
		let $\phi_0,\ldots,\phi_m$ be all $\Sigma^*_{n_k}(\mathcal{L}_{\mathcal{M}_{k}})$-formulae that occur in $B\cap K$ and without loss of generality assume that each of them is satisfied by finitely many elements in $\mathcal{M}_k$. Pick any $\psi(x)\in\Sigma^*_k(\mathcal{L}_U)$ which defines in $\mathcal{M}_k$ an element which is different from any element satisfying $\bigvee_{j\leq m}\phi_j(x)$. I.e. $\psi(x)$ is such that
		\[\mathcal{M}_k\models  \exists !x\psi(x) \wedge \forall x \bigl(\psi(x)\rightarrow \bigwedge_{j\leq m} \neg\phi_j(x)\bigr).\] 
		Such a $\psi$ exists because in $\mathcal{M}$ there are infinitely many $\Sigma^*_k(\mathcal{L}_U)$ definable elements and $\mathcal{M}\preceq_{k} \mathcal{M}_k$. By flexibility of $\theta_{k+1}$ there exists $\mathcal{N}\succeq_{{n_k}}\mathcal{M}$ such that $\mathcal{N}\models U+ \forall x \bigl(\theta_{k+1}(x)\equiv \psi(x)\bigr)$. By the choice of $\psi$ and $n_k$, $\mathcal{N}\models \forall x \bigl(\psi(x)\rightarrow\bigwedge_{j\leq m}\neg\phi_j(x)\bigr)$. Hence $\mathcal{N}\models K$ and $\textnormal{Th}$ is indeed consistent.
		
		We put $\mathcal{M}_{k+1}$ to be any model of $\textnormal{Th}$. We set $n_{k+1}:= \Sigma^*(\theta_{k+1})+1$.
	\end{proof}

  
	\begin{tw}\label{tw_nondef_def_in_tb}
		Suppose that $U$ is a sequential, r.e. theory in a finite language $\mathcal{L}$, $K: S^1_2\lhd U$
		and $n$ is such that there is a model $\mathcal{M}\models U$ with infinitely many $\Sigma^*_n(\mathcal{L})$-definable elements. Then $\textnormal{TB}_K(\mathcal{L})$ does not semantically define $\textnormal{DEF}_K(\mathcal{L})$ modulo $\mathcal{L}$ and does not impose the equality of definables.
	\end{tw}
	\begin{proof}
		Fix $U$, $K$, $n\in\omega$ and let $\mathcal{M}\models U$ have infinitely many $\Sigma^*_n(\mathcal{L})$-definable elements. Without loss of generality assume that it is $\omega$-saturated, that is, $\mathcal{M}$ realizes all the types with finitely many parameters from $\mathcal{M}$. Then, for every $V$, complete and consistent extension of $U$, there is $c\in M$ which codes $V$ in $\mathcal{M}$ (according to the Definition \ref{defi_kodowanie}). 
		Let $\mathcal{N}$ be the $\Sigma^*_k(\mathcal{L})$-elementary extension of $\mathcal{M}$ constructed as in Lemma \ref{lem_hierarchical_model}, where $m$ is greater than the complexity of $x\in_U y$ (see Definition \ref{defi_sekwencyjność}). Since $m$ is large enough, in $\mathcal{N}$ there is an element which codes $\textnormal{Th}(\mathcal{N})$. 

		Hence we can fix $c\in N$ such that 
		\[(\mathcal{N},c)\models \textnormal{TB}_{K}(\mathcal{L}).\] 

		\paragraph{Claim} For all sufficiently large $k$, for all $b\in N$ there is an $\mathcal{N}'\succeq_k\mathcal{N}$ such that 
		\begin{enumerate}
			\item $(\mathcal{N}',c,b)\models \textnormal{Th}((\mathcal{N},c,b))$
			\item there is a definable element in $\mathcal{N}$ which is not definable in $\mathcal{N}'$.
		\end{enumerate}
		Before proving the claim we show that it implies that $\textnormal{TB}_K$ neither imposes the equality of ($\mathcal{L}$-)definables

		 nor semantically defines $\textnormal{DEF}_K$. Indeed, assuming the claim is true, for every $b\in \mathcal{N}$, $\textnormal{Th}((\mathcal{N},c,b))$ is a complete and consistent theory which syntactically defines $\textnormal{TB}_K$ and does not impose the equality of definables. It directly follows that $\textnormal{TB}_K$ does not impose the equality of definables. Finally, if there were a definition of $\textnormal{DEF}_K$ in $(\mathcal{N},c)$,

		 then for some $b\in N$ this definition would work provably in $\textnormal{Th}((\mathcal{N},c,b))$, hence $\textnormal{DEF}_K$ would be syntactically definable in $\textnormal{Th}((\mathcal{N},c,b))$. 
		 
		 
		  This would contradict the fact that $\textnormal{Th}((\mathcal{N},c,b))$ does not impose the equality of definables .
		
		
		Fix any $k$ which is larger than the complexity of $x\in y$ and any $b\in N$. Now, aiming at a proof of the claim, we define a model $\mathcal{N}'$ satisfying $1$ and $2$.  Let $l$ be such that $b\in \mathcal{M}_l$,
		where $\was{\mathcal{M}_i}_{i\in\omega}$ is the chain constructed for $N$ in Lemma \ref{lem_hierarchical_model}. Now, let $d$ be any element of $N$ which is parameter-free definable, but not $\Sigma_{k+1}^*(\mathcal{L}_{M_l})$-algebraic.
		
		Consider the theory $\textnormal{Th}$ which is the union of the following sets (we say that a formula $\phi(x)$ is syntactically a definition if for some $\phi'(x)$, $\phi(x)$ is of the form $\phi'(x) \wedge \forall y\bigl(\phi'(y)\rightarrow y=x\bigr)$):
		\begin{itemize}
			\item $\textnormal{Th}((\mathcal{N},c,b))$
			\item $(k+1)\mhyphen \textnormal{Diag}(\mathcal{N})$
			\item $\set{\neg\psi(d)}{\psi(x)\in\mathcal{L} \wedge \psi \textnormal{ is syntactically a definition}}$
		\end{itemize} 
		Clearly any model of $\textnormal{Th}$ will satisfy 1 and 2, so it is enough to show that $\textnormal{Th}$ is consistent. Suppose not. Then for finitely many formulae $\psi_0,\ldots,\psi_t$

		 and some formula $\nu(x)\in\Sigma^*_{k+1}(\mathcal{L}\cup\was{c,b})$ such that $\nu(d)\in (k+1)\mhyphen\textnormal{Diag}(\mathcal{N})$ and we have
		 
			\[\textnormal{Th}((\mathcal{N},c,b))\vdash \nu(x)\rightarrow \bigvee_{j\leq t}\psi_j(x).\]
			It follows that $\textnormal{Th}((\mathcal{N},c,b))\vdash \exists^{\leq t}x\nu(x)$. However, this is impossible since $\mathcal{N}\models \textnormal{Th}((\mathcal{N},c,b))$ and $d$ is not $\Sigma^*_{k+1}(\mathcal{L}\cup\was{c, b})$-algebraic in $\mathcal{N}$. 
	\end{proof}
	
	\begin{wniosek}\label{cor_nonres_def}
		Let $U$ be a sequential r.e. theory in a finite language with $K: S^1_2\lhd U$. Suppose that for some $n\in\omega$ there is a model $\mathcal{M}\models U$ with infinitely many $\Sigma^*_n(\mathcal{L})$-definable elements, then $\textnormal{DEF}_K$ does not have a restricted axiomatization modulo $U$.  

	\end{wniosek}
	\begin{proof}
		Fix $U$ as above and assume $V$ is a $\Sigma_k^*$-restricted $\mathcal{L} \cup \was{D}$-theory such that 
		\[U+V \equiv \textnormal{DEF}_K(\mathcal{L}).\]
		Take any model $\mathcal{M}\models U$ and $n\in\omega$ such that in $\mathcal{M}$ there are infinitely many $\Sigma^*_n(\mathcal{L})$-definable elements. Without loss of generality assume that $\mathcal{M}$ is recursively saturated. Hence, there is an element $c\in M$ such that for all $a\in M$, $\phi(x)\in\mathcal{L}$,
		\[\mathcal{M}\models \pair{\phi(x)}{a}\in_{\mathcal{M}} c \equiv \exists !x \phi(x)\wedge \phi(a).\]
		In the above both $\pair{\cdot}{\cdot}$, $\in_{\mathcal{M}}$ denote the set theoretical operations given by the direct interpretation of AS.

		 It follows that $\textnormal{ElDiag}(\mathcal{M})\vdash \textnormal{DEF}_K[\pair{x}{y}\in c / D(x,y)]$. Suppose that $l$ is the complexity of $\pair{x}{y}\in_{\mathcal{M}} z$. By our assumption, it follows that $U+(k+l)\mhyphen \textnormal{Th}((\mathcal{M},c))\vdash V[\pair{x}{y}\in_{\mathcal{M}} c / D(x,y)]$. Hence 
		\[U+(k+l)\mhyphen \textnormal{Th}((\mathcal{M},c))\vdash \textnormal{DEF}_K[\pair{x}{y}\in_{\mathcal{M}} c / D(x,y)].\]
		Let $\mathcal{N}\succeq_{k+l} \mathcal{M}$ be the model constructed in Lemma \ref{lem_hierarchical_model}. It follows that $\mathcal{N}\models U+ (k+l)\mhyphen \textnormal{Th}(\mathcal{M},c)$, hence, by our assumption
		\[\mathcal{N}\models \textnormal{DEF}_K[\pair{x}{y}\in_{\mathcal{M}} c / D(x,y)].\] Hence for some $m\in\omega$ in $\mathcal{N}$ all $\mathcal{L}$-definable elements are $\Sigma^*_m(\mathcal{L})$-definable with a parameter $c$.
		This contradicts the properties of $\mathcal{N}$. 	
	\end{proof}
	

	
	
	
	We finish this section with some observations regarding the relations between semantical and syntactical definability of $\textnormal{TB}$, $\textnormal{DEF}$ and $\textnormal{USB}$.
	
	\begin{stwierdzenie}\label{prop_UTB_pf}
		For any sequential model $\mathcal{M}$ for a finite language $\mathcal{L}$ and an interpretation $N:S^1_2\lhd \textnormal{ElDiag}(\mathcal{M})$, if $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $\textnormal{USB}_N(\mathcal{L})$, then $\textnormal{Th}(\mathcal{M})$ syntactically defines $\textnormal{USB}_N(\mathcal{L})$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $\mathcal{M}, N$ and suppose $T'_{\mathcal{M}}(x,y,z)$ is such that for some $b$, $T'_{\mathcal{M}}(x,y,b)$ defines $\textnormal{USB}_N(\mathcal{L})$ in $\mathcal{M}$. Let $n$ be the $\Delta^*$ complexity of $T'_{\mathcal{M}}$. Let $\textnormal{Sat}_n(x,y)$ be the partial satisfaction predicate for $\Delta_n$ formulae (as in Fact \ref{fakt_partial_truth} and the discussion following it). Let $\textnormal{Sat}_n'(\psi,z,w_0,w_1)$ be the formula
        \[\form^{v_0,v_1,v_2}_{\mathcal{L}}(\psi)\wedge\textnormal{Sat}_n(\psi,\left[v_0\mapsto w_0,v_1\mapsto w_1,v_2\mapsto z\right]).\]
  In the above, $\form^{v_0,v_1,v_2}_{\mathcal{L}}(\psi)$ expresses that $\psi$ is a formula whose free variables are exactly $v_0,v_1,v_2$ ($v_0,v_1,v_2$ being fixed variables) and $[v_0\mapsto x,v_1\mapsto y,v_2\mapsto z]$ denotes the unique assignment sending $v_0$ to $x$, $v_1$ to $y$ and $v_2$ to $z$. Now put
  \[\textnormal{Th}eta(\phi,\psi,x,z):= \textnormal{SAT}^{w_0,w_1}_n[\textnormal{Sat}'_{n}(\psi, z,w_0,w_1)]\rightarrow \textnormal{Sat}_{n}(\psi,[v_0\mapsto \phi, v_1\mapsto x, v_2\mapsto z]).\]
	Recall that $\textnormal{SAT}_n^{w_0,w_1}[\xi]$ is a formula expressing that $\xi(w_0,w_1)$ is a $\Delta_n^*$-satisfaction predicate with $w_0$ being the variable corresponding to formulae and $w_1$ being the variable corresponding to assignments (as introduced in the remarks following Fact \ref{fakt_partial_truth}). Therefore, the intuitive meaning of $\textnormal{Th}eta(\phi,\psi,x,z)$ is: if $\psi(z,w_0,w_1)$ is a satisfaction predicate for $\Delta_n^*$ formulae (where $z$ is treated as a parameter), then $\phi$ is satisfied by $x$ according to this satisfaction predicate."  Finally put $T_{\mathcal{M}}(\phi,x):= \forall \psi(v_0,v_1,v_2)\in\Delta^*_n \forall z\bigl(J_n(\textnormal{pdp}(\psi))\rightarrow \textnormal{Th}eta(\phi,\psi,x,z)\bigr).$ 

	
		The meaning of the definition is that $\phi$ is satisfied by $x$ if and only if $\phi$ is satisfied by $x$ according to all $\Sigma^*_{n}(\mathcal{L})$ truth definitions for formulae of complexity at most the complexity of $\phi$. $T_{\mathcal{M}}$ clearly does not involve any parameters. Such a definition does the job since first of all there is $\Delta_n^*$ definable satisfaction predicate (i.e. $T'_{\mathcal{M}}(x,y,b)$) and secondly, all satisfaction predicates have to agree on formulae of standard complexity. We omit the elementary details.

	
	\end{proof}
	
	
	\begin{wniosek}\label{wniosek_ogr_def_utb}
		Let $U$ be an r.e. sequential theory in a finite language and $N: S^1_2\lhd U$. If there is an $n$ such that for every $\mathcal{M}\models U$, $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $\textnormal{USB}_N$ with a formula of complexity $n$, then $U$ syntactically defines $\textnormal{USB}_N$.
	\end{wniosek}
	\begin{proof}
		It is enough to observe that the formula $T_{\mathcal{M}}$ from the proof of Proposition \ref{prop_UTB_pf} depends only on $n$, but not on $\mathcal{M}$.
	\end{proof}
	
	\begin{uwaga}
		In Theorem \ref{th_theory_with_rec_sat_without_utb} we shall construct a theory $U\supseteq\textnormal{PA}$ in an infinite language such that for every $\mathcal{M}\models U$ $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $\textnormal{UTB}_{id}(\mathcal{L}_{\textnormal{PA}})$ with an atomic formula but $U$ does not syntactically define $\textnormal{UTB}_{id}(\mathcal{L}_{\textnormal{PA}})$. Similarly, in Theorem \ref{th_theory_finlang_with_rec_sat_without_utb}, we will construct a theory $V$ in a finite language such that in every model $\mathcal{M} \models V$, $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $\textnormal{UTB}_{id}(\mathcal{L}_{\textnormal{PA}})$ without a uniform bound on the complexity of the definitions, such that $V$ does not syntactically define
	 $\textnormal{UTB}_{id}(\mathcal{L}_{\textnormal{PA}})$.  
	\end{uwaga}

	Corollary \ref{wniosek_ogr_def_utb} fails dramatically in the context of $\textnormal{TB}_N$.
	
	\begin{stwierdzenie}\label{prop_ogr_sem_tb_2}
		If $U$ is any sequential theory and $N:S^1_2\lhd U$, then there is a theory $\textnormal{Th}\supseteq U$ such that in every model of $\textnormal{Th}$, $\textnormal{TB}_N$

		 is definable with an atomic formula but $\textnormal{Th}$ does not syntactically define $\textnormal{TB}_N$ modulo $\mathcal{L}_U$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $U$ and an interpretation $N: S^1_2\lhd U$.

		 Consider the extension of $U$ in the language with two additional predicates $T_1(x)$, $T_2(x)$ with all sentences of the form
		\[T_1(\num{\qcr{\phi}})\equiv \phi \vee T_2(\num{\qcr{\psi}})\equiv \psi,\]
		for $\phi,\psi\in\mathcal{L}$. Call this theory $2\textnormal{TB}_N$. Observe that if $(\mathcal{M},T_1,T_2)\models 2\textnormal{TB}_N$, then 
		\[(\mathcal{M}, T_1)\models \textnormal{TB}_N \textnormal{ or } (\mathcal{M},T_2)\models \textnormal{TB}_N.\]
		So it is sufficient to show that $2\textnormal{TB}_N$ does not define $\textnormal{TB}_N$. We shall show that $2\textnormal{TB}_N$ does not impose elementary equivalence. Fix any $n$ and let $\mathcal{M}_1\models U$ be an $\omega$-saturated model of $U$. In particular, $\mathcal{M}_1$ codes (in the sense of the defined membership predicate $\in_U$ satisfying AS) every consistent and complete extension of $U$. Assume that $k$ is the complexity of $U$-definition of $x\in_U y$. Let $\theta$ be a $(k+n,0)$-flexible formula over $U$. Without loss of generality assume that $\mathcal{M}_1\models \exists x \theta(x)$. By Proposition \ref{prop_flexible} there is $\mathcal{M}_2\succeq_{k+n} \mathcal{M}_1$ such that $\mathcal{M}_2\models \forall x \neg\theta(x)$. Let $c_1, c_2\in M$ be the codes of the theories of $\mathcal{M}_1$ and $\mathcal{M}_2$ respectively.

		Now put 
		\begin{align*}
			T_1^{\mathcal{M}_i}&:= \set{a\in M_i}{\mathcal{M}_i\models a\in_U c_1}\\
			T_2^{\mathcal{M}_i}&:= \set{a\in M_i}{\mathcal{M}_i\models a\in_U c_2}
		\end{align*}
		It follows that $(\mathcal{M}_i,T_1^{\mathcal{M}_i}, T_2^{\mathcal{M}_i})\models 2\textnormal{TB}_N$ and 
		\[(\mathcal{M}_1,T_1^{\mathcal{M}_1}, T_2^{\mathcal{M}_1})\preceq_n (\mathcal{M}_2, T_1^{\mathcal{M}_2},T_2^{\mathcal{M}_2}).\]
		However $\textnormal{Th}(\mathcal{M}_1)\neq \textnormal{Th}(\mathcal{M}_2)$, which ends the proof.
	\end{proof}
In fact, the above proof gives us a stronger statement:

 \begin{stwierdzenie}\label{prop_ogr_sem_tb}
		If $U$ is any sequential theory and $N: S^1_2\lhd U$, then there is a theory $\textnormal{Th}\supseteq U$ such that every complete extension of $\textnormal{Th}$ syntactically defines
		$\textnormal{TB}_N$ modulo $\mathcal{L}_U$ with an atomic formula but $\textnormal{Th}$ does not syntactically define $\textnormal{TB}_N$ modulo $\mathcal{L}_U$.
\end{stwierdzenie}

Corollary below answers the question of Albert Visser from \cite{viss19enayat}[Question 5.7]

	\begin{wniosek}\label{cor_nonres_tb}
		For every sequential theory $U$ and interpretation $N: S^1_2\lhd U$, $\textnormal{TB}_N$ does not have a restricted axiomatization modulo $U$.
	\end{wniosek}
	\begin{proof}
		Suppose there is an $n$-restricted theory $V$ such that $U+V\equiv \textnormal{TB}_N$. Let $\mathcal{M}_1$, $\mathcal{M}_2$,  $T_1^{\mathcal{M}_1}$, $T_1^{\mathcal{M}_2}$ be constructed as in the proof of Proposition \ref{prop_ogr_sem_tb_2}.

		 Since $(\mathcal{M}_1, T_1^{\mathcal{M}_1})\models \textnormal{TB}_N$ it follows that $(\mathcal{M}_1, T_1^{\mathcal{M}_1})\models V$ and since $V$ is $n$-restricted, then $(\mathcal{M}_2, T_1^{\mathcal{M}_2})\models V$.  Hence $(\mathcal{M}_2, T_1^{\mathcal{M}_2})\models \textnormal{TB}_N$, which is impossible, because $\num{\qcr{\exists x \theta(x)}}\in T_1^{\mathcal{M}_2}$ but $\mathcal{M}_2\models \forall x \neg\theta(x)$. 
	\end{proof}
	
	An observant reader might wonder whether there is anything interesting to say about the uniform version of a theory $\textnormal{DEF}_K$. One way to formulate this theory is via the following collection of sentences
    \[\forall x\forall y \bigl(D(\num{\qcr{\phi(v,w)}}, x,y) \equiv \exists !v\phi(v,y) \wedge \phi(x,y)\bigr).\]
    The intuitive meaning of $D(\num{\qcr{\phi(v,w)}}, a,b)$ is that $a$ is definable via the formula $\phi(x,b)$, where $b$ is a parameter. Let us call this theory $\textnormal{UDEF}_K$

    Actually, it is very easy to see that for every $U$, $\textnormal{UDEF}_K$ and $\textnormal{USB}_K$ are mutually definable. Indeed, the definition of $D(x,y,z)$ in $\textnormal{USB}_K$ is analogous to the case of $\textnormal{DEF}_K$ and $\textnormal{USB}_K$, and the definition of $S(\phi(v),y)$ in $\textnormal{UDEF}_K$

     is given by the formula:
    \[D(\qcr{v=w \wedge \phi(v)}, y,y).\]
    
	
	\subsection{Skolem functions}\label{subsect_skolem}
	
	We devote this section to the concept of Skolem functions. We treat it separately, since we do not have a clear semantical property which characterizes it up to the definability. However it is worth mentioning since it is classical and nicely fits into our hierarchy. As previously we work over a fixed sequential theory $U$ in a language $\mathcal{L}$ and $K$ is a distinguished interpretation $S^1_2\lhd U$.
	
	\paragraph{Skolem functions} S$_K(\mathcal{L})$ extends $U$ with all sentences of the form
	\[\exists x \phi(x)\rightarrow \phi(H(\num{\qcr{\phi}})),\]
	where $\phi(x)$ is an $\mathcal{L}$-formula, with a single free variable and $H(x)$ is a fresh function symbol.
	
	\paragraph{Uniform Skolem functions} US$_K(\mathcal{L})$ extends $\textnormal{EA}$ with all sentences of the form
	\[\exists x \phi(x,y)\rightarrow \phi(H(\num{\qcr{\phi}}, y), y),\]
	where $\phi(x,y)$ is an $\mathcal{L}$-formula with at most $x,y$-free and $H(x,y)$ is a fresh function symbol.
	
	\begin{stwierdzenie}
		For every sequential theory $U$ and every $K: S^1_2\lhd U$, $\textnormal{TB}_K(\mathcal{L}_U)$ and $\textnormal{DEF}_K(\mathcal{L}_U)$ are syntactically definable in $\textnormal{S}_K(\mathcal{L}_U)$ modulo $\mathcal{L}_U$. Similarly, $\textnormal{USB}_K(\mathcal{L}_U)$ is syntactically definable in $\textnormal{US}_K(\mathcal{L}_U)$ modulo $\mathcal{L}_U$.  
	\end{stwierdzenie}
	\begin{proof}
		We do the case of $\textnormal{USB}_K(\mathcal{L}_U)$, the rest of cases is very similar. Define
		\[S(\phi,x):= \num{1}\bigl(H(\theta_{\phi},x)\bigr),\]
		where $\theta_{\phi}(z,x):= \bigl((\num{1}(z)\wedge \phi(x))\vee (\num{0}(z) \wedge \neg\phi(x))\bigr)$ (we recall that $\num{n}(x)$ is the analogue of $x = \num{n}$ in the context of a general sequential theory).

		
	\end{proof}
	
	Now, we turn to separations between theories of truth, definability, satisfaction on one side and skolem functions on the other. We start with the comparison od truth and witnessing functions. The following lemma is a variant of Lemma \ref{lem_hierarchical_model}. We stress, that unlike its predecessor it holds without the additional assumption on the existence of infinitely many $\Sigma_n^*(\mathcal{L})$ definable elements.
	
	\begin{lemat}\label{lem_hierarchical_model_2}
		For every r.e. sequential theory $U$ in  a finite language, every model $\mathcal{M}\models U$ and every $n\in \omega$, there is a model $\mathcal{M}\preceq_n \mathcal{N}$ such that $N = \bigcup_{i\in\omega}M_i$ and for every $l,m\in\omega$, there is $\theta(x)\in\mathcal{L}$ such that $\mathcal{N}\models \exists x\theta(x)$ but for every $\Sigma^*_l(\mathcal{L}_{M_m})$-definable element $a\in N$, $\mathcal{N}\models \neg\theta(a)$.
	\end{lemat}
	\begin{proof}
		The strategy is the same as in the proof of Lemma \ref{lem_hierarchical_model}. We build sequences $\was{\mathcal{M}_i}$, $\was{\theta_i}$ and $\was{n_i}$ which \rem{satisfy conditions $1.$ and $2.$ from the proof}
		and we switch condition $3.$ to the following one
		\begin{itemize}
			\item[3'.] for each $i$, $\mathcal{M}_{i+1}\models \exists x \theta_{i+1}(x)$ but for every $\Sigma_{n_i}^*(\mathcal{L}_{\mathcal{M}_i})$ definition $\phi(x)$, $\mathcal{M}_{i+1}\models \neg(\theta_{i+1}(x)\wedge \phi(x))$. 
		\end{itemize}
		It is a routine exercise to verify that for so defined sequence $\was{\mathcal{M}_i}_{i\in\omega}$, $\mathcal{N}:= \bigcup_{i\in\omega}\mathcal{M}_i$ satisfy the thesis of the lemma. Let us now show how to construct the relevant sequences. We define $\mathcal{M}_0 = \mathcal{M}, n_0 = n+1$

		 and choose $\theta_0$ to be any formula. Since $U$ is sequential,

		 there is $k\in\omega$ and $\was{\phi_i(x)}_{i\in\omega}$ such that for each $j$, $\phi_j$ is of complexity $\Sigma^*_k$, $\mathcal{M}\models \exists x \phi_j(x)$ and for any $i\neq j$, $\mathcal{M}\models \neg \bigl(\phi_i(x)\wedge \phi_j(x)\bigr)$ (for example $\phi_i$ defines the $E$-equivalence class corresponding to the natural number $i$). Assume that we are given $\mathcal{M}_i, n_i$. We let $\theta_{i+1}(x)$ be the $(n_i+1, k)$-flexible formula. Consider the following theory
		\[\textnormal{Th}:= U + (n_i+1)\mhyphen\textnormal{Diag}(\mathcal{M}_i) + \was{\theta_{i+1}(d)} + \set{\neg\theta_{i+1}(a)}{a\in M_i}.\]
		We claim that $\textnormal{Th}$ is consistent. For this, fix a finite fragment $A\subseteq \textnormal{Th}$ and  assume $a_1,\ldots, a_l$ are all elements from $\mathcal{M}_i$ such that $\neg\theta(a)$ occurs in $A$. Let $m$ be any natural number such that for all $i\leq l$, $\mathcal{M}_i\models \neg\phi_m(a_i)$. By the flexibility of $\theta_{i+1}$ there is a model $\mathcal{M}'\models U + \forall x (\theta_{i+1}(x)\equiv \phi_m(x))$ such that $\mathcal{M}_{i+1}\preceq_{n_i+1}\mathcal{M}'$. Clearly, $\mathcal{M}'\models A$. Now we set $\mathcal{M}_{i+1}$ to be any model of $\textnormal{Th}$ and put $n_{i+1}:= \Sigma^*(\theta_{i+1}) + 1$.

		 Observe that, by elementarity, every $\Sigma_{n_i}^*(\mathcal{L}_{M_i})$ definable element in $\mathcal{M}_{i+1}$ belongs to $M_i$. Hence, no witness for $\exists x \theta_{i+1}(x)$ is $\Sigma^*_{n_i}(\mathcal{L}_{M_i})$-definable in $\mathcal{M}_{i+1}$.
	\end{proof}
	
	\begin{tw}
		For every r.e. sequential $U$ in a finite language and every $K: S^1_2\lhd U$, $\textnormal{TB}_K(\mathcal{L}_U)$ does not semantically define $S_K(\mathcal{L}_U)$. 
	\end{tw}
	\begin{proof}
		Fix any model $\mathcal{M}\models U$ which is $\omega$-saturated. Let $\mathcal{N}$ be a model satisfying the thesis of Lemma \ref{lem_hierarchical_model_2}
		for $n$ equal to the complexity of the definition of $x\in y$ in $U$. In particular $\mathcal{N}$ is an $n-$elementary extension of $\mathcal{M}$. It follows that $\mathcal{N}$ codes $\textnormal{Th}(\mathcal{N})$. Let $c\in M$ be such a code. Consequently $(\mathcal{N},c)\models\textnormal{TB}_K[x \in_{\mathcal{N}} c/T(x)]$.

		 We claim that $\textnormal{ElDiag}(\mathcal{N}, c)$ does not syntactically define  $S_K$ modulo $\mathcal{L}_U$. Assume the contrary and let $k$ be the complexity of the definition of $H(x,y)$ (in a relational form).  Assume further that all the parameters used in the definition belong to $M_m$. Then $H(x,y)$ is $\Sigma_{k+n}^*(\mathcal{L}_{M_m})$-definable in $\mathcal{N}$.
		It follows that each non-empty parameter-free definable set $A\subseteq N$ contains a witness which is $\Sigma_{k+n}^*(\mathcal{L}_{M_m})$-definable in $\mathcal{N}$. This contradicts the property of $\mathcal{N}$.
	\end{proof}
	
	\begin{stwierdzenie}
		If $U\subseteq\mathcal{L}_{\textnormal{PA}}$ extends $\textnormal{PA}$, then $\textnormal{DEF}_{id}(\mathcal{L}_{\textnormal{PA}})$ defines $\textnormal{S}_{id}(\mathcal{L}_{\textnormal{PA}})$ and $\textnormal{USB}_{id}(\mathcal{L}_{\textnormal{PA}})$ syntactically defines $\textnormal{US}_{id}(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{stwierdzenie}
	\begin{proof}
		Essentially this follows, since $\textnormal{PA}$ has definable Skolem functions. Let us do the case of $\textnormal{US}_{id}(\mathcal{L}_{\textnormal{PA}})$. Working in $\textnormal{PA}+\textnormal{USB}_{id}(\mathcal{L}_{\textnormal{PA}})$ we define
		\[H(\phi(x,v),y) = z := S(\qcr{\phi(x,v)\wedge \forall w<x\neg\phi(w,v)}, \pair{z}{y}).\] 
	\end{proof}
	
	As the next two theorems show, in the above result $\textnormal{PA}$ cannot be replaced by any of its finite fragments. Unfortunately we do not know exactly over which sequential theories, $\textnormal{DEF}_N(\mathcal{L})$ semantically/syntactically  defines $\textnormal{S}_N(\mathcal{L})$. Similarly, we do not know over which sequential theories, $\textnormal{USB}_N{\mathcal{L}}$ semantically/syntactically defines $\textnormal{US}_N(\mathcal{L})$.
	However we can isolate a fairly natural class of theories over which the definability fails.
	
	\begin{tw}\label{stw_nondef_H_usb}
		For every $n\in\omega$, and every $U\subseteq \mathcal{L}_{\textnormal{PA}}$ consistent with $B\Sigma_n + \neg I\Sigma_n + \exp$, $\textnormal{USB}_{id}(\mathcal{L}_{\textnormal{PA}})$ does not parameter-free semantically define $\textnormal{S}_{id}(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.  
	\end{tw}
	\begin{proof}
		Fix $U$ and $n\in\omega$ and let $\mathcal{M}\models U$ be countable and recursively saturated. We claim that there is a (non-empty) parameter-free definable set $A\subseteq M$ such that $A$ contains no parameter-free definable element. Assume the contrary. Then, by the Tarski-Vaught test, $K(\mathcal{M})\preceq \mathcal{M}$. In particular $K(\mathcal{M})\models B\Sigma_n + \neg I\Sigma_n + \exp$ and every element of $K(\mathcal{M})$ is parameter-free definable in $K(\mathcal{M})$. Since $K(\mathcal{M})$ has no proper elementary submodel, this literally contradicts \cite[Theorem 7.4.4]{kossakschmerl}. 
		
		So assume $A\subseteq M$ is a parameter-free definable subset of $\mathcal{M}$ with no parameter-free definable element. Since $\mathcal{M}$ is recursively saturated, by an easy back-and-forth argument,
		for each $a\in A$ there is an automorphism of $\mathcal{M}$ which moves $a$. Let $S:= \set{\pair{\qcr{\phi(x)}}{a}\in \omega\times M}{\mathcal{M}\models \phi(a)}$ be the Tarskian satisfaction class for $\mathcal{M}$. It follows that $(\mathcal{M},S)\models \textnormal{USB}_{id}$. Moreover, the automorphism groups of $\mathcal{M}$ and $(\mathcal{M},S)$ are the same (because each isomorphism preserve definable sets and pointwise fixes $\omega$). Suppose $\textnormal{S}_{id}(\mathcal{L}_{\textnormal{PA}})$ is parameter-free definable in $(\mathcal{M},S)$. It follows that there is an element of $A$ which is parameter-free definable in $(\mathcal{M},S)$. However, by the choice of $A$, $S$ and $\mathcal{M}$, every element of $A$ can be moved by an automorphism of $(\mathcal{M},S)$. This concludes the proof.
	\end{proof}
	
	\begin{tw}\label{tw_nondef_US_in_UTB}
		For every $n\in\omega$, and every $U$ consistent with $B\Sigma_n + \neg I\Sigma_n + \exp$, $\textnormal{USB}_{id}(\mathcal{L}_{\textnormal{PA}})$ does not semantically define $\textnormal{US}_{id}$ modulo $U$.  
	\end{tw}
	\begin{proof}
		We modify the above proof of Proposition \ref{stw_nondef_H_usb}. We fix $U, n,\mathcal{M}$ exactly as above and claim that for each $a\in M$ there is an $\mathcal{L}_{\textnormal{PA}}\cup \was{a}$ definable subset of $M$ with no $\mathcal{L}_{\textnormal{PA}}\cup\was{a}$ definable element. The idea of the argument is as previously, only instead of $K(\mathcal{M})$ we are using $K(\mathcal{M},a)$ (the model consisting of $(\mathcal{L}_{\textnormal{PA}}\cup \was{a})$-definable elements of $\mathcal{M}$) and instead of \cite[Theorem 7.4.4]{kossakschmerl} we use \cite[Corollary 3.5]{kaye_model_char_PA}.
		
		Now we let $S$ be defined exactly in the same way as previously. We fix $a\in M$ and show that there is no definition of $H$ which uses $a$ as a parameter. Assume that there is such a definition. Let $A$ be the $a$-definable set with no $a$-definable element. It follows that for every element $b\in A$ there is an automorphism $f\in \textnormal{Aut}(\mathcal{M})$ which fixes $a$ and moves $b$. As previously it follows that no element in $A$ is $a$-definable in $(\mathcal{M},S)$, which ends the proof. 
	\end{proof}
	
	\begin{stwierdzenie} \label{stw_S_nie_definiuje_USB}
		For every sequential theory $U$ and $K: S^1_2\lhd U$, $\textnormal{S}_K(\mathcal{L}_U)$ does not semantically define $\textnormal{USB}_K(\mathcal{L}_U)$ modulo $\mathcal{L}_U$.
	\end{stwierdzenie}
	\begin{proof}
		This follows from the fact that each sequential theory has a model $\mathcal{M}$ such that for some $c\in M$, $(\mathcal{M},c)\models \textnormal{S}_N(\mathcal{L}_U)[\tuple{x,y} \in_{\mathcal{M}} c / H(x) = y ]$.

		 Indeed, let $\mathcal{M}\models U$ be any recursively saturated model of $U$. Consider the following recursive type $p(x)$ (recall (Convention \ref{konwencja_arytmetyka_w sekwencji}) that we treat $\num{\qcr{\phi(y)}}$ as a predicate
		which isolates $E$-equivalence class of elements corresponding to the numeral naming $\qcr{\phi}$, so $\num{\qcr{\phi(y)}}(z)$ means that $z$ is equal to the numeral naming $\qcr{\phi(y)}$):
		\[\set{\exists y \phi(y)\rightarrow \exists !z\exists! y (\phi(y)\wedge \num{\qcr{\phi(y)}}(z)\wedge \pair{z}{y}\in_{\mathcal{M}} x)}{\phi(y)\in\mathcal{L}}.\]
		By the sequentiality of $U$, $p(x)$ is a type. Any elements realizing this type codes a witnessing function for $\mathcal{L}$-formulae. However, a predicate satisfying $\textnormal{USB}$ can never be definable with a parameter. 
	\end{proof}
	
	
	\subsection{$\textnormal{PA}$ case}\label{subsect_PA}
	
	

	In this subsection and until the end of the paper (i.e. also in Section \ref{sect_truth_rec_sat}), we specialize to languages which extend $\mathcal{L}_{\textnormal{PA}}$ with at most countably many new predicate symbols and theories that extend $\textnormal{PA}$ and prove full scheme of induction for their respective languages. In particular, we will omit the mention of the interpretation of $S^1_2$ in our theory, as it will be assumed to be identity. 

	As it will be important to distinguish between the situation in which we have full induction for the truth predicate and the one in which induction is assumed only for arithmetical formulae, we shall employ the following notation: the minus sign in the superscript will indicate that we do not extend induction axioms to the whole language.

	 In particular, $\textnormal{USB}^-(\mathcal{L})$ 
	 denotes simply $\textnormal{PA} + \textnormal{USB}_{id}(\mathcal{L})$ (in the terminology of Section \ref{sect_prelim_truth}) and $\textnormal{USB}(\mathcal{L})$ is its extension with induction axioms for the extended language. The collection of all induction axioms for a language $\mathcal{L}$ will be denoted $\textnormal{Ind}_{\mathcal{L}}$.
	 

	 
	
	We start with a proposition that is properly weaker than already proved Theorem \ref{tw_nonuniform_impos_elem_utb}, but we give it here because in this context it has a particularly illustrative proof.
	
	\begin{stwierdzenie}
		If $\textnormal{PA}\subseteq U$ is an r.e. theory in a finite language which uniformly imposes $\mathcal{L}$-elementarity (elementary equivalence, preserves definability) and such that $U\vdash \textnormal{Ind}_{\mathcal{L}_U}$, then $\textnormal{USB}(\mathcal{L})$ ($\textnormal{TB}(\mathcal{L})$, $\textnormal{DEF}(\mathcal{L})$) is syntactically definable in $U$.
	\end{stwierdzenie}

	\begin{proof}
		We sketch the proof for $\textnormal{USB}(\mathcal{L})$ (the proof easily adapts to the other two cases). We use the following convention: if $\phi(x)$ is an arbitrary formula, then $\textnormal{Con}(\phi(x))$ denotes the assertion that the theory consisting of all those axioms that satisfy $\phi(x)$ is consistent. Choose $n$ witnessing that $U$ uniformly imposes $\mathcal{L}$-elementarity. 
		

		
		Consider the following formalized theory ($\textnormal{True}_k(x)$ is a partial truth predicate for $\Sigma^*_k$ sentences, which is based on $\textnormal{Sat}_k(x.y)$):
		\[\alpha(x):= \textnormal{True}_{n+1}(x) \vee \bigl(U(x)\wedge \textnormal{Con}(U\restr{x}+\textnormal{True}_{n+2})\bigr).\]
		In the above $U(x)$ is an elementary predicate which represents the axiom set of $U$ and $U\restr{x}$ denotes the theory consisting of all axioms of $U$ of G\"odel code $\leq x$ and $\textnormal{Con}(U\restr{x}+\textnormal{True}_{n+2})$ expresses that every $\Sigma^*_{n+2}$ sentence provable in $U\restr{x}$ is true.  Since $U$ contains full $\textnormal{PA}$, $U$ proves cut-elimination theorem for first-order logic.
		In particular, for every $k,n$ separately, by considering cut-free proofs, inside $U$ we can reprove the standard inductive argument and show that $U\restr{k} + \textnormal{True}_{n+1}$ is consistent (i.e. axioms of $U$ smaller than $k$ are consistent with all $\Sigma^*_{n+1}$ true sentences). Hence $U\vdash\textnormal{Con}(\alpha(x))$ (i.e. the set of axioms defined by $\alpha(x)$ is a consistent theory.)
		and, for every $k$ separately, 
		\begin{equation}\label{equat_N_models_U}
			U\vdash U\restr{k}\subseteq \alpha.
		\end{equation}
		By the Arithmetized Completeness Theorem (see \cite[Section 13.2]{kaye}) there is a definable model $\mathcal{N} = (N, +^{\mathcal{N}}, \cdot^{\mathcal{N}}, 0^{\mathcal{N}}, 1^{\mathcal{N}})$ which comes with a definable truth predicate $\models^{\mathcal{N}}$ such that $U$ proves
		\begin{equation}\label{equat_N_models_alpha}
			\forall \phi\bigl(\alpha(\phi)\rightarrow \mathcal{N}\models^{\mathcal{N}} \phi\bigr)
		\end{equation}
		Let $\iota$ denote the canonical initial embedding of the universe onto an initial segment of $\mathcal{N}$, defined recursively $\iota(0) = 0^{\mathcal{N}}$, $\iota(x+1) = \iota(x)+^{\mathcal{N}} 1^{\mathcal{N}}$ 
		(i.e. $x$ is mapped to the value if the $x$-th numeral as computed in $\mathcal{N}$) and define
		\[T_U(\phi, x):= \mathcal{N}\models^{\mathcal{N}}\phi[\iota(x)].\]
		We check that $U\vdash \textnormal{USB}^-(\mathcal{L})[T_U/T]$. Pick any model $\mathcal{M}\models U$. Then the definable model $\mathcal{N}$ gives rise to a true model (which will be denoted with the same letter) and $\models^{\mathcal{N}}$ coincides with the usual satisfaction class for $\mathcal{N}$. Hence, by \eqref{equat_N_models_U} and \eqref{equat_N_models_alpha}, $\mathcal{N}\models U$. By the properties of $\iota$, $\iota[\mathcal{M}]\subseteq_e \mathcal{N}$. Since $\mathcal{M}\models \textnormal{True}_{n+1}\subseteq \alpha$, $\iota[\mathcal{M}]\preceq_n \mathcal{N}$. It follows that $\iota[\mathcal{M}\restr{\mathcal{L}}]\preceq \mathcal{N}\restr{\mathcal{L}}$, because $U$ imposes $\mathcal{L}$-elementarity. In particular, for an arbitrary $a\in M$ and $\phi(x)\in\mathcal{L}$ the following are equivalent
		\begin{enumerate}
			\item $\mathcal{M}\models T_U(\phi,a)$
			\item $\mathcal{M}\models \mathcal{N}\models^{\mathcal{N}}\phi[\iota(a)]$
			\item $\mathcal{N}\models \phi[\iota(a)]$
			\item $\iota[\mathcal{M}]\models \phi[\iota(a)]$
			\item $\mathcal{M}\models \phi(a)$
		\end{enumerate}
		The equivalence between $2.$ and $3.$ is the absoluteness of the satisfaction relation and the equivalence between $3.$ and $4.$ follows, since $\iota[\mathcal{M}\restr{\mathcal{L}}]\preceq \mathcal{N}\restr{\mathcal{L}}$.
	
	\end{proof}
	
	In the separations below we shall use the following observation:
	
	\begin{stwierdzenie}\label{stw_def_bounded}
		Let $\mathcal{L}$ be at most countable language. Suppose $(\mathcal{M},D)\models \textnormal{PA} + \textnormal{DEF}(\mathcal{L})$ is nonstandard. Then the $\mathcal{L}$-definable elements are bounded in $\mathcal{M}$.	
	\end{stwierdzenie}

	\begin{proof}
		We use overspill on the formula
		\[\psi(x):= \exists c \forall \phi(z)<x \forall y \bigl(D(\phi(z), y)\rightarrow y<c\bigr).\]
		Clearly $(\mathcal{M},D)\models \psi(n)$ for every $n\in\omega$. Hence $\psi(d)$ holds for some $d\in M\setminus\omega$ and the witness for $\psi(d)$ bounds all the definable elements.
	\end{proof}
	
	\begin{stwierdzenie}
		If $U\supseteq \textnormal{PA}$ is an r.e. theory in at most countable language $\mathcal{L}_U$ such that $U\vdash \textnormal{Ind}_{\mathcal{L}_U}$, then $U+\textnormal{USB}(\mathcal{L}_U)\nleq^s_{\mathcal{L}_U} U+\textnormal{DEF}(\mathcal{L}_U)\nleq^s_{\mathcal{L}_U} U+\textnormal{TB}(\mathcal{L}_U)$.
	\end{stwierdzenie}
	\begin{proof}
		The second separation follows, since there is a model $(\mathcal{M},T)\models U+\textnormal{TB}(\mathcal{L}_U)$ in which the $\mathcal{L}_U$-definable elements are cofinal. This model cannot be expanded to a model of $\textnormal{DEF}(\mathcal{L}_U)$, by Proposition \ref{stw_def_bounded}. To get this model fix any $(\mathcal{M}, T)\models \textnormal{TB}(\mathcal{L}_U)$, which is not a model of true arithmetic. Let $c\in SSy(\mathcal{M})$ be the code of the theory of $\mathcal{M}$ (this element exists because we have induction for the truth predicate). Then $\mathcal{K}(\mathcal{M})$ (the submodel consisting of $\mathcal{L}_U$-definable elements) is nonstandard and elementary in $\mathcal{M}$. By the Gaifman splitting theorem for $U$ (se \cite[Corollary 7.10]{kaye}) there is $\mathcal{N}$ such that 
		\[\mathcal{K}(\mathcal{M})\preceq_{cof}\mathcal{N}\preceq_e \mathcal{M}.\]
		(in fact, $\mathcal{N}$ is simply the supremum of $\mathcal{K}(\mathcal{M})$ in $\mathcal{M}$). Since $\mathcal{N}\preceq_e\mathcal{M}$, we may assume that $c\in N$, $(\mathcal{N}, c)\models \textnormal{TB}(\mathcal{L}_U)[x \in c/T(x) ]$.

		 However in $\mathcal{N}$ the definable elements are cofinal, because $\mathcal{K}(\mathcal{M})\preceq_{cof}\mathcal{N}$.
		
		The first separation follows, since there is a model of $\textnormal{DEF}(\mathcal{L}_U)$ whose $\mathcal{L}_U$-reduct is not short recursively saturated, and $\textnormal{USB}(\mathcal{L}_U)$ imposes $\mathcal{L}_U$-recursive saturation (see e.g. \cite{wcislyk_models_weak}). To see that such a model exists, fix any nonstandard $(\mathcal{M},D)\models \textnormal{DEF}(\mathcal{L}_U)$ and let $d$ be such that for every $\phi(x)$ and every $a\in M$
		\[(\mathcal{M},D)\models \pair{\num{\qcr{\phi(x)}}}{a}\in d \equiv D(\num{\qcr{\phi(x)}}, a).\]
		The existence of $d$ follows once again by overspill. Take $\mathcal{N}:= \mathcal{K}(\mathcal{M},d)$ (i.e. the submodel of $\mathcal{M}$ consisting of elements $(\mathcal{L}_U \cup\was{d})$-definable with parameter $d$). Then $d\in\mathcal{N}\preceq_{\mathcal{L}_U}\mathcal{M}$ and $\mathcal{N}$ is not short recursively saturated, since it does not realise the type $p(x,d)$ 
	
		
		\[\set{x<d \wedge \bigl(\exists!y\phi(y,d)\rightarrow \neg \phi(x,d)\bigr)}{\phi(y)\in\mathcal{L}_{U}}.\]
		However, $\mathcal{N}$ expands to a model of $\textnormal{DEF}(\mathcal{L}_U)$, because in $\mathcal{N}$ the predicate satisfying $\textnormal{DEF}(\mathcal{L}_U)$ is definable with a parameter via the formula
		\[D(x,y):= \form^{1}(x) \wedge \pair{x}{y}\in d.\]
		where $\form^1(x)$ says that $x$ is a formula with one free variable.
	\end{proof}	
	
	Recall that $\leq^s_{\mathcal{L}}$ and $\leq^m_{\mathcal{L}}$ denote syntactical and semantical definability modulo $\mathcal{L}$ (respectively).
	\begin{wniosek}
		$\textnormal{TB}\leq^s_{\mathcal{L}_{\textnormal{PA}}}\textnormal{DEF}\leq^s_{\mathcal{L}_{\textnormal{PA}}}\textnormal{USB}$ but $\textnormal{TB}\ngeq^m_{\mathcal{L}_{\textnormal{PA}}} \textnormal{DEF}\ngeq^{m}_{\mathcal{L}_{\textnormal{PA}}} \textnormal{USB}$.
	\end{wniosek}

\begin{uwaga} \label{rem_separation_noninductive_PA}
	As a corollary we also obtain the above separations and reductions also for noninductive version of the above theories. For the separations: notice that if there were reductions in the noninductive case, they would simply imply the respective reductions in the fully inductive case. On the other, the reductions which we obtained for the inductive versions of the theories, actually only used the axioms of $\textnormal{DEF}^-, \textnormal{TB}^-$ and $\textnormal{USB}^-$, respectively, not the induction scheme for the predicates $D$, $T$, and $S$. 
\end{uwaga}

	
	\subsubsection{Definability in no model}\label{subsect_PA_def_inno}
	
	In this subsection we strengthen the non-definability results obtained above. Once again, we switch to non-inductive variants of $\textnormal{TB}$, $\textnormal{DEF}$ and $\textnormal{USB}$, which will be denoted simply $\textnormal{TB}^-$, $\textnormal{DEF}^-$ and $\textnormal{USB}^-$, respectively.

    In the proposition below we are going to use the following result due to Stuart Smith (\cite[Theorem 3.11]{Smith_extendible}, and the remark immediately after the proof on p. 351)

    \begin{tw}\label{Smith_omega}
    Suppose that $\mathcal{M}\models \textnormal{PA}$ is nonstandard. Then for every $\mathcal{N}$ such that $\mathcal{M}\preceq \mathcal{N}$ and every $A\subseteq \omega$, $(\mathcal{M},A)\preceq (\mathcal{N},A)$.
    \end{tw}
    In the above, $(\mathcal{M},A)$ denotes the expansion of a structure $\mathcal{M}$ to a language with a fresh predicate interpreted as set $A$.
	\begin{stwierdzenie}\label{tw_ost_niedef_TB_UTB}
		In every nonstandard model
		$\mathcal{M}\models \textnormal{PA}$ there is a set $T$ such that $(\mathcal{M},T)\models\textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$ but $\textnormal{ElDiag}(\mathcal{M},T)$ does not syntactically define $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $\mathcal{M}\models \textnormal{PA}$ and let $T = \set{\qcr{\phi}\in\omega}{\mathcal{M}\models \phi}$. We claim that $\textnormal{ElDiag}(\mathcal{M},T)$ does not define syntactically define $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$. Assume the contrary and pick any formula $S(x,y)\in \mathcal{L}_M$. Let $a$ be a parameter used in this definition and without loss of generality assume that $a$ is nonstandard. 
		Let $\mathcal{N}$ be any proper elementary end extension of $\mathcal{M}$ (which exists by the Macdowell-Specker Theorem \cite[Theorem 8.6]{kaye}) and let $\mathcal{K}(a)$ be the submodel of $\mathcal{M}$ generated by the elements which are definable in $\mathcal{M}$ from $a$. Moreover, let $\mathcal{M}'$ be the submodel of $\mathcal{M}$ with the domain $\set{d\in M}{\exists x\in \mathcal{K}(a) \mathcal{M}\models d<x}$.

		By the result of Gaifman (see \cite[Corollary 7.10]{kaye}) $\mathcal{M}'\preceq_e \mathcal{M}$ (we do not assume that this extension is proper.)
		 We have 
		\[\mathcal{M}'\preceq_e \mathcal{M}\precneqq_e \mathcal{N},\]
		so by Theorem \ref{Smith_omega}
		for $A=T\subset\omega$
		\[(\mathcal{M}',T)\preceq_e(\mathcal{M},T)\precneqq_e (\mathcal{N},T).\]
		Note that $\omega$ is definable in all the three models with a formula $\phi(x):= \exists y \bigl(x\leq y \wedge T(y)\bigr)$. Moreover $S(x,y)$ defines $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$ in both $(\mathcal{M}',T)$ and $(\mathcal{N},T)$ and hence 
		\begin{equation}\label{elementarity}\tag{E}
			(\mathcal{M}',S^{\mathcal{M}'}, \omega)\precneqq_e(\mathcal{N},S^{\mathcal{N}},\omega)
		\end{equation}
		(recall that for a formula $\phi$ and a model $\mathcal{U}$, $\phi^{\mathcal{U}}$ denotes the set of elements which satisfy $\phi$ in $\mathcal{U}$.) However, the $\mathcal{L}_{M'}\cup \was{T}$ formula
		\[\zeta(x,a):= \exists \psi(v_0,v_1)\in \omega\bigl[ S(\qcr{\psi(v_0,\num{a}/v_1)}, x)\wedge \forall z\bigl(S(\qcr{\psi(v_0, \num{a}/v_1)}, z)\rightarrow x=z\bigr)\bigr]\]
		in both $(\mathcal{M}',S^{\mathcal{M}'},\omega)$ and $(\mathcal{N}, S^{\mathcal{N}}, \omega)$ defines the set of $\mathcal{L}_{\was{a}}$-definable elements of $\mathcal{M}'$ and $\mathcal{N}$, respectively. Since $(\mathcal{M}',S^{\mathcal{M}'},\omega)\models \forall y\exists x>y \zeta(x,a)$ and $(\mathcal{N},S^{\mathcal{N}}, \omega)\models \exists y \forall x>y \neg \zeta(x,a)$, this contradicts \eqref{elementarity}.
	\end{proof}
	
	\begin{stwierdzenie}
		For every model $\mathcal{M}\models \textnormal{PA}$ the following are equivalent:
		\begin{enumerate}
			\item $\mathcal{M}\models \textnormal{Th}(\mathbb{N})$
			\item For every $T\subseteq M$, if $(\mathcal{M},T)\models \textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$, then $\textnormal{ElDiag}(\mathcal{M},T)$ syntactically defines $\textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$.
		\end{enumerate}
	\end{stwierdzenie}
	\begin{proof}
		Fix any $\mathcal{M}\models \textnormal{PA}$. Assume first that $\mathcal{M}\models \textnormal{Th}(\mathbb{N})$ and take any $T\subseteq M$ such that $(\mathcal{M},T)\models \textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$. The following formula is then a definition of $\textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$
		\[D(\phi(x),y):= T(\qcr{\exists! x \phi(x)})\wedge T(\qcr{\phi(\dot{y})})\wedge \forall z< y \neg T(\qcr{\phi(\dot{z})}).\]
		We prove that it works. Assume first $\mathcal{M}\models \exists !x \phi(x)\wedge \phi(a)$. Since $\mathcal{M}\models \textnormal{Th}(\mathbb{N})$, $a\in \omega$. In particular $\phi(\num{a})$ is a standard sentence and by $\textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$ $(\mathcal{M},T)\models T(\exists!x\phi(x))\wedge T(\qcr{\phi(\num{a})})$. Since every $b<a$ is also a standard number, then for any such $b$ we have $(\mathcal{M},T)\models \neg T(\qcr{\phi(\num{b})})$. Now assume $(\mathcal{M},T)\models D(\phi,a)$. By $\textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$ it follows that $\mathcal{M}\models \exists!x\phi(x)$. We claim that $\mathcal{M}\models \phi(a)$. Assume the contrary. Since $(\mathcal{M},T)\models T(\qcr{\phi(\num{a})})\wedge \neg\phi(a)$ then $a$ is nonstandard. However, since $\mathcal{M}\models \textnormal{Th}(\mathbb{N})$ there is the unique $n\in\omega$ such that $\mathcal{M}\models \phi(\num{n})$. 
		It follows that $(\mathcal{M},T)\models \exists x<a T(\qcr{\phi(\dot{x})})$, contradicting $D(\phi,a)$.
		
		Now assume that $\mathcal{M}$ fails to satisfy $\textnormal{Th}(\mathbb{N})$ and let $T:= \set{\phi\in\omega}{\mathcal{M}\models \phi}$. Let $\mathcal{K}$ be the submodel of $\mathcal{M}$ consisting of $\mathcal{L}_{\textnormal{PA}}$ (i.e. parameter-free) definable elements of $\mathcal{M}$. Let $\mathcal{M}'$ satisfy $\mathcal{K}\preceq_{cf}\mathcal{M}'\preceq_e \mathcal{M}$. Let $\mathcal{N}$ be any proper elementary end-extension of $\mathcal{M}$. Now mimic the proof of Theorem \ref{tw_ost_niedef_TB_UTB} to conclude that if $\textnormal{ElDiag}(\mathcal{M},T)$ defines $\textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$,

		 then the extensions
		\[(\mathcal{M}', T)\subseteq_e (\mathcal{M},T)\subsetneq_e (\mathcal{N},T)\]
		cannot all be elementary, contradicting Theorem \ref{Smith_omega}.
	\end{proof}

	Now we comment on the relation between $\textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$ ans $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$. Here, unlike in the previous two cases, we lack the full characterisation of the class of models whose every expansion to a model of $\textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$ defines $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$.
	
	\begin{stwierdzenie}
		Assume $\mathcal{M}\models \textnormal{PA}$ is such that every element in $\mathcal{M}$ is definable without parameters. Let $D\subseteq M^2$ be such that $(\mathcal{M},D)\models \textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$. Then $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$ is syntactically definable in $\textnormal{ElDiag}(\mathcal{L}_{\textnormal{PA}})$.
	\end{stwierdzenie}
	\begin{proof}
		Let $\mathcal{M}\models \textnormal{PA}$ be prime and assume $(\mathcal{M},D)\models \textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$. Let $T(x)$ be a definition of a truth predicate satisfying $\textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$ in $(\mathcal{M}, D)$ (as in Proposition \ref{stw_latwa_definiowalnosc}). We define $S(\phi,x)$ in the following way
		\[\exists \psi \bigl(D(\psi,x)\wedge \forall y<\psi \neg D(y,x)\wedge T(\qcr{\forall x (\psi(x)\rightarrow \phi)})\bigr).\]
		The correctness of the definition is guaranteed by the fact that every element of $\mathcal{M}$ has a standard definition without parameters.
	\end{proof}
	
	
	Finally we notice that Theorem \ref{tw_ost_niedef_TB_UTB} fails for fragments of $\textnormal{PA}$ of restricted quantifier complexity. Let $\textnormal{PA}\restr{n}$ denote the set of consequences of $\textnormal{PA}$ of complexity $\Sigma_n$.
	
	\begin{stwierdzenie}
		For every $n$ there is a model $\mathcal{M}\models \textnormal{PA}\restr n$ such that for every $T\subseteq M$ such that $(\mathcal{M},T)\models \textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$, $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$ is syntactically definable in $\textnormal{ElDiag}(\mathcal{M},T)$.
	\end{stwierdzenie}
	\begin{proof}
		Fix $n$ and any model $\mathcal{N}\models \textnormal{PA}$. Let $\mathcal{K}^n$ be the submodel of $\mathcal{M}$ consisting of $\Sigma_n$-definable elements. Then, by \cite[Theorem 10.1]{kaye} $\mathcal{K}^n\preceq_n \mathcal{M}$, hence $\mathcal{K}^n\models \textnormal{PA}\restr{n}$. Moreover there is a formula $\phi(x)$ such that $\phi^{\mathcal{K}^n} = \omega$. Fix any $T$, a subset of the universe of $\mathcal{K}^n$

		 such that $(\mathcal{K}^n,T)\models \textnormal{TB}^-(\mathcal{L}_{\textnormal{PA}})$. Then it is easy to check that the following formula defines $\textnormal{USB}^-(\mathcal{L}_{\textnormal{PA}})$ in $(\mathcal{K}^n,T)$
		\[\theta(\psi(v),a):= \exists \chi(v) \in\Sigma_n \bigl(\phi(\chi) \wedge \textnormal{Sat}_{n}(\chi, a)\wedge \forall x\neq a\neg\textnormal{Sat}_n(\chi,x) \wedge T\bigl(\qcr{\forall v \bigl(\chi(v)\rightarrow \psi(v)\bigr)}\bigr).\]
	\end{proof}
	
	
	\section{Truth and recursive saturation}\label{sect_truth_rec_sat}
	
	We recall that in this section all theories in considerations are extensions of $\textnormal{PA}$ (possibly in an extended language) and $^-$ superscript signalizes that induction is assumed only for arithmetical formulae. The following definition will be handy in the particular context of $\textnormal{PA}$ as the base theory.
	
	\begin{definicja}
		In what follows
		the variables $s,t,u$ will range over G\"odel codes of arithmetical terms and variables $v$, $v_i$, $w$ - over codes of variables. For example the quantification $\forall t\psi$ should be understood as $\forall x \bigl(\textnormal{ClTerm}(x) \rightarrow \psi[x/t]\bigr)$. Similarly $\phi,\psi$ will range over codes of arithmetical sentences, $w,v,$ over codes of variables and $\phi(v)$, $\psi(v)$ over codes of arithmetical formulae with at most one free variable shown. For an arbitrary closed term $t$, $\val{t}$ denotes the value of $t$. The function $t\mapsto \val{t}$ is provably total in $\textnormal{PA}$, so we shall use the \rem{symbol $\val{x}$}
		as if it were a function symbol in our language. $\phi\in\textnormal{dp}(x)$ is an $\mathcal{L}_{\textnormal{PA}}$ formula in variables $\phi$ and $x$ which expresses that $\phi$ is a $\mathcal{L}_{\textnormal{PA}}$ formula of syntactical depth at most $x$, i.e. each path in the syntactic tree of $\phi$ has length at most $x$ (compare \ref{def_complexity}).
		
		$\textnormal{CT}^-(x)$ denotes the conjunction of the axiom of $I\Delta_0+\exp$ and the following sentences of $\mathcal{L}_{\textnormal{PA}}\cup \was{T}$:
		\begin{enumerate}
			\item[CT1] $\forall s,t \bigl(T(\qcr{s=t})\equiv \val{s} = \val{t}\bigr)$ 
			\item[CT2] $\forall \phi\in\textnormal{dp}(x)\forall\psi\in\textnormal{dp}(x) \bigl(T(\qcr{\phi\vee\psi})\equiv T(\phi)\vee T(\psi)\bigr)$.
			\item[CT3] $\forall \phi\in\textnormal{dp}(x)\bigl(T(\qcr{\neg\phi})\equiv \neg T(\phi)\bigr)$. 
			\item[CT4] $\forall v\forall \phi(v)\in\textnormal{dp}(x)\bigl(T(\exists v \phi)\equiv \exists y T(\qcr{\phi(\dot{y}/v)})$.
		\end{enumerate}
		In the above, as introduced in Convention \ref{konwencja_arytmetyka_w sekwencji}, $\qcr{\neg\phi}$ denotes a definable function in variable $\phi$ that given a sentence $\phi$ returns the G\"odel code of $\neg\phi$. The use of $\qcr{\cdot}$ in axioms $\textnormal{CT}1$, $\textnormal{CT}2$ and $\textnormal{CT}4$ should be understood analogously.
		
		$\textnormal{CT}^-$ extends $\textnormal{PA}$ with the sentence $\forall x \textnormal{CT}^-(x)$ and $\textnormal{CT}(x)$ is the theory extending $\textnormal{PA}$ with $\textnormal{CT}^-(x)$ and full induction scheme for $\mathcal{L}_{\textnormal{PA}}\cup \was{T}$.
	\end{definicja}
	
	
	\begin{uwaga}
		For theories $U$ extending $\textnormal{PA}$ (in fact much less is needed), $\textnormal{UTB}^-_{id}(\mathcal{L}_{U})$ is mutually syntactically definable modulo $\mathcal{L}_{\textnormal{PA}}$ with the following term variant of $\textnormal{UTB}^-_{id}(\mathcal{L}_{U})$,

		 consisting of the following biconditionals:
		\[\forall t \bigl(T(\qcr{\phi(t)})\equiv \phi(\val{t})\bigr).\]
		In the above, $\phi(x)$ is an arbitrary formula of $\mathcal{L}_{\textnormal{PA}}$ and $\qcr{\phi(t)}$ denotes the effect of formal substitution of $t$ for $x$ in $\phi(x)$. The definability holds, because sufficiently strong arithmetical theories prove that every object from the universe can be named by a closed term. The above will be our official definition of $\textnormal{UTB}_{id}(\mathcal{L}_{U})$ in this section. 	 Arguably, it is the best known version of the considered theories of satisfaction. Following the conventions from the previous section, we will omit the subscript indicating the identity interpretation of $S^1_2$ in our theories. Moreover, we will sometimes also omit the mention of the arithmetical language $\mathcal{L}_{\textnormal{PA}}$.

	
	\end{uwaga}
	
	It is a well known fact that if a model $(M,T)$ satisfies $\textnormal{UTB}$, then its arithmetical part $M$ is recursively saturated. Surprisingly, as shown by \cite{lachlan}, the same holds if we assume that $(M,T)$ satisfies $\textnormal{CT}^-$, a theory with compositional axioms for arithmetical sentences and no induction.
	
	Roman Kossak, in \cite{kossak_cztery_problematy}, has shown that a partial reverse holds. The proof makes a crucial use of the MacDowell-Specker Theorem (see \cite{kossakschmerl}). Recall that a model $\mathcal{N}$ is a conservative extension of $\mathcal{M}$ if $\mathcal{M}$ is a submodel of $\mathcal{N}$ and for every $A\subseteq N$, if $A$ is definable in $\mathcal{N}$ with parameters, then $A\cap M$ is definable in $\mathcal{M}$ with parameters.

    \begin{tw}[Macdowell-Specker]
    Let $\textnormal{Th}$ be a theory in at most countable language $\mathcal{L}$ such that $\textnormal{Th}\vdash \textnormal{PA}$  and $\textnormal{Th}$ proves all the instantiations of the induction scheme with formulae of $\mathcal{L}$. Then every model of $\textnormal{Th}$ has a proper, conservative, elementary extension.
    \end{tw}
	
	\begin{tw}[Kossak] \label{tw_kossak_indukcja_vs_nasycenie}
		Let $U$ be a theory in a countable language, containing $\textnormal{PA}$ and the full induction scheme (for the extended language). Then, if $U$ imposes (short) $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, then $U$ semantically defines $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{tw}
	
	\begin{proof}
		Let $\mathcal{M} \models U$ and let $\mathcal{M} \precneqq_e \mathcal{M}'$ be a proper, conservative and elementary end-extension of $\mathcal{M}$. $\mathcal{M}'$ exists since $U$ is a theory in countable language satisfying full induction, so the Macdowell-Specker Theorem holds for $U$. 
		
		Fix an arbitrary $a \in M' \setminus M$. Let $s$ be an arbitrary element which realizes the following recursive type:
		\[p(x):= \set{\forall t<a\bigl( \qcr{\phi(t)}\in x \equiv \phi(\val{t})\bigr)}{\phi\in \mathcal{L}_{\textnormal{PA}}}.\]
		In particular, $s$ codes the set of true arithmetical sentences of standard complexity with terms smaller than $a$. Let $T = \set{ x \in M }{\mathcal{M}' \models x \in s}.$ Then $T$ is a class in $\mathcal{M}$, hence it is definable in $\mathcal{M}$ by conservativeness of the extension. By definition, $(\mathcal{M},T)$ satisfies $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$. Since $\mathcal{M}$ satisfies full induction, actually $(\mathcal{M},T) \models \textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$.
	\end{proof}
	
	In the above argument, induction is used as a crucial ingredient in order to obtain a conservative end-extension. If a model of a fragment of $\textnormal{PA}$ does not satisfy full induction, it can never have an elementary end-extension at all, so the argument as-is breaks down completely. This motivates the following question: Does Theorem \ref{tw_kossak_indukcja_vs_nasycenie} hold if we drop the assumption that $U$ proves the induction scheme for its own language? Let us start with a simple example showing that the strict analogue cannot be true for rather general reasons. 
	
	\begin{uwaga} \label{rem_theory_of_realisers}
		Consider the following theory $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ in the language extending $\mathcal{L}_{\textnormal{PA}}$ with a fresh ternary predicate $R(p,x,y)$. $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ extends $\textnormal{PA}$  with the following axioms of optimality (OP) and nonemptiness (NE):
		\begin{enumerate}
			\item[OP] $\exists x  \bigwedge_{i = 1}^n \phi^p_i(y_1,\ldots, y_k,x) \rightarrow \forall x\left( R(\num{p}, x, \tuple{y_1,\ldots,y_k}) \rightarrow \bigwedge_{i=1}^n  \phi^p_i(y_1,\ldots,y_k,x)\right),$
			\item[NE] $\exists x R(\num{p}, x,\tuple{y_1,\ldots,y_k})$,
		\end{enumerate}
		where $\num{p}$ is the G\"odel code of a total p.r. function $i\mapsto \phi_i^p$ and $\tuple{y_1,\ldots,y_k}$ is an arithmetical code for a sequence $y_1,\ldots, y_k$. To improve readability we shall write $R_p(x,y)$ instead of $R(p,x,y)$.
		
		We think of $R_p$ as ``type-realisers.'' Each $x$ such that $R_p(x,\bar{y})$

		holds satisfies as large a portion of  the type $p$ as possible (with parametres $\bar{y}$).
		
		Clearly, any model of $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ is recursively saturated and, conversely, any recursively saturated model of $\textnormal{PA}$ expands to a model of $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$. In particular, if $M$ is a recursively saturated rather classless model of $\textnormal{PA}$ (see \cite{kossakschmerl}), then it expands to a model of RSAT, but not to a model of $\textnormal{UTB}$. (Notice that in the definition of $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ we do not assume induction for the extended language).
	\end{uwaga}

	
	The obstruction discussed in the above remark is rather general in nature and shows that a direct strengthening of Theorem \ref{tw_kossak_indukcja_vs_nasycenie} is not possible. However, we might still hope that Kossak's result essentially holds in greater generality, in that the only way to impose recursive saturation in a theory is ``essentially'' to use a truth predicate. This intuition turns out to be correct, at least for theories extending a sufficiently strong arithmetic. The following strengthening of Kossak's theorem is true:
	
	\begin{tw} \label{th_recursive_saturation_implies_truth}
		Every theory in a countable language which extends $\textnormal{PA}$ and imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation semantically defines $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{tw}
	Notice that if $U$ contains full induction and semantically defines $\textnormal{UTB}^-$($\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$, then in each model the definable truth predicate automatically satisfies full induction scheme, hence the above theorem is indeed a strengthening of the result by Kossak. 
	
	Before we present the proof of the result, let us note a counterexample to a stronger thesis, since it actually precedes Theorem \ref{th_recursive_saturation_implies_truth} and partly serves as an inspiration for its proof. We could ask whether we could strengthen the conclusion of the theorem to \emph{syntactical definability}. It turns out that such a strengthening does not hold.  
	
	\begin{tw} \label{th_theory_with_rec_sat_without_utb}
		There exists a theory $U \supseteq \textnormal{PA} +\textnormal{Ind}_{\mathcal{L}_U}$ which imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation but does not syntactically define $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{tw}
	
	\begin{proof}
		Let $(\phi_j)_{j\in\omega}$ be a primitive recursive enumeration of all arithmetical formulae. Consider the following theory $U$ in the arithmetical language with additional predicates $T_i, T_{\omega}, i \in \omega$. $U$ contains $\textnormal{PA}$, full induction for the extended language, and the following axioms:
		\begin{displaymath}
			\neg \forall t \Big(T_j (\qcr{\phi_i(t)}) \equiv \phi_i(\val{t})\Big) 
			\rightarrow \forall t \Big(T_{\omega} (\qcr{\phi_j(t)}) \equiv \phi_j(\val{t})\Big),
		\end{displaymath}
		where $i, j \in \omega$.
	
		
		We claim that for every model $\mathcal{M} \models U$, the arithmetical reduct of $\mathcal{M}$ is recursively saturated. Indeed, in every such model, there exists a predicate $S$ satisfying full $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$, since if a predicate $T_j$ does not satisfy all the axioms of $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$, then $T_{\omega}$ satisfies the instance of the uniform biconditional scheme for the formula $\phi_j$. Hence either one of $T_j$, $j<\omega$, satisfies the axioms of $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$, or none of them does, in which case $T_{\omega}$ satisfies it.  
		
		We further claim that $U$ does not syntactically define $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$. Indeed, suppose that there exists such a definition $\phi$. Then $\phi$ uses only finitely many predicates $T_i$. Fix any $N \in \omega$ large enough so that all such predicates have index $i< N$ or $i=\omega$.
		
		Consider a model of $U$ such that the arithmetical part is standard (i.e., isomorphic to $(\mathbb{N},+, \times,0)$) and the predicates $T_i$ are interpreted as follows: all predicates $T_i$ for $i \leq N$ are interpreted as empty sets, $T_{\omega}$ is defined as the partial truth predicate for formulae $\phi_i, i \leq N$:
		\begin{equation*}
			T_{\omega} := \set{\qcr{\phi_i(t)} \in \textnormal{Sent}_{\mathcal{L}_{\textnormal{PA}}}(\mathbb{N})}{i \leq N \wedge \mathbb{N} \models \phi_i(\val{t})},
		\end{equation*}
		and all $T_j$ for $j > N$ are defined as the standard arithmetical truth predicate, i.e.:
		\begin{equation*}
			T_j := \set{\qcr{\phi(t)} \in \textnormal{Sent}_{\mathcal{L}_{\textnormal{PA}}}(\mathbb{N})}{\mathbb{N} \models \phi(\val{t})}.
		\end{equation*}
		One can check that the model $(\mathbb{N},T_i,T_{\omega})_{i < \omega}$ satisfies the axioms of the theory $U$. On the other hand, in that model the predicates $T_i, i \leq N$ and $T_{\omega}$ are arithmetically definable, so the set defined by the formula $\phi$ is also arithmetically definable and hence it cannot satisfy the disquotational axioms of $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$. 
	\end{proof}
	
	In the proof of Theorem  \ref{th_theory_with_rec_sat_without_utb}, we introduced an infinite family of predicates. The ``further'' predicates $T_i$ are from satisfying $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$, the "closer" $T_{\omega}$ gets to satisfying it. In particular, any completion of $U$ will  actually have a predicate which satisfies $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ provably in the theory. In fact, this pattern essentially turns out to hold in the full generality which is the key idea of Theorem \ref{th_theory_with_rec_sat_without_utb}. Let us note that the proof is largely inspired by a related work of \cite{casanovas_farre}. 
	
	\begin{proof} [Proof of Theorem \ref{th_recursive_saturation_implies_truth}]
		
		Let $U$ be a theory in a countable language $\mathcal{L}$ extending $\textnormal{PA}$. Suppose that for every model $\mathcal{M}\models U$, the arithmetical part of $\mathcal{M}$ is recursively saturated.		
		Let us introduce some notation. By $\tau(x,y)$ we mean the type consisting of all formulae of the form:
		\begin{displaymath}
			\forall t < x \ \Big( \phi(\val{t}) \equiv \qcr{\phi(t)} \in y \Big),
		\end{displaymath}
		where $\phi$ is an arithmetical formula. In other words, $\tau(x,y)$ expresses "$y$ is a code of the truth predicate for standard formulae and terms not greater than $x$." Observe that for every $\mathcal{M}\models \textnormal{PA}$ and every $a\in M$, $\tau(a,y)$ is a type over $\mathcal{M}$. Moreover, if $\mathcal{M}$ is any model of the elementary arithmetic $\textnormal{EA}$ and for every $a\in M$, $\tau(a,y)$ is realized in $\mathcal{M}$, then $\mathcal{M}\models \textnormal{PA}$. 
		
		Let $\mathcal{L}^*$ extend $\mathcal{L}$ with one fresh constant $a$. We will inductively build $\mathcal{L}^*$-theories $U_{\alpha}$ extending $U$ and sets of $\mathcal{L}^*$-formulae $A_{\alpha}$. We let $U = U_0$. For any $\alpha$, let
		\begin{displaymath}
			A_{\alpha} = \set{\exists y \phi(x,y) \in \textnormal{Form}_{\mathcal{L}}}{ U_{\alpha} \vdash \forall y \left( \phi(a,y) \rightarrow  \tau(a,y) \right)}.
		\end{displaymath}
		The occurrence of $\tau$ should be understood schematically: $U_{\alpha}$ proves every sentence resulting from the above template, where we substitute some formula $\pi \in \tau$ for $\tau$. For any $\alpha$, we let:
		\begin{displaymath}
			U_{\alpha+1} = U_{\alpha} \cup \set{\neg \psi(a)}{\psi(x) \in A_{\alpha}}. 
		\end{displaymath} 
		Finally, we define $U_{\gamma}$ as the union of $U_{\beta}$ for $\beta<\gamma$ for limit ordinals $\gamma$.
		
		Observe that if $U_{\alpha}$ is consistent, then $U_{\alpha+1}$ strictly extends $U_{\alpha}$. Indeed, since  $U_{\alpha}$ extends $U$ and therefore in each model of $U$, $\tau(a,y)$ is realised, this follows immediately  by the Omitting Types Theorem (see \cite[Theorem 2.2.9]{chang-keisler}).

		
		
		
		
	
		Now, since $U_{\alpha}$'s form an increasing chain of sets, it has to stabilise. Let $\alpha$ be the least ordinal such that $U_{\alpha} = U_{\alpha+1}$. This means that $U_{\alpha}$ is inconsistent. In particular, $\alpha$ has to be a successor ordinal, say $\alpha = \beta+1$. Since $U_{\beta+1}$ is inconsistent, by compactness there has to be a finite collection $\psi_1(a), \ldots, \psi_n(a) \in A_{\beta}$ such that 
		\begin{displaymath}
			U_{\beta} \vdash \bigvee_{i \leq n} \psi_i(a).
		\end{displaymath}
		
		We now turn to the main part of the proof. Fix any model $\mathcal{M} \models U$. Let $\mathcal{M}^* \succeq \mathcal{M}$ be a countably saturated elementary extension of $\mathcal{M}$.  We claim that for some $\gamma$ and some $\psi \in A_{\gamma}$, $\psi(x)$ holds cofinally in $\mathcal{M}^*$. Indeed, suppose for contradiction that for any ordinal $\delta$, for any $\psi \in A_{\delta}$, there exists $b$ such that $\neg \psi(a)$ holds for all $a>b$. By saturation, this means that for any $\delta$, there exists $b_{\delta}$ such that for all $a>b_{\delta}$, $\neg \psi(a)$ holds for all $\psi \in A_{\delta}$. By  transfinite induction, this means that for all $\delta$, and all $a>b_{\delta}$, $(\mathcal{M}^*, a)\models U_{\delta+1}$. However, as we already noticed, there exists $\beta$ such that $U_{\beta} \vdash \bigvee_{i \leq n} \psi_i(a)$ for a finite family of formulae in $A_\beta$. Since there are finitely many of them, one of these formulae has to hold cofinally in $\mathcal{M}^*$. This is a contradiction.
		
		So fix the minimal $\gamma$ such that one of the formulae in $A_{\gamma}$ holds cofinally in $\mathcal{M}^*$. By minimality, for every $\delta < \gamma$ and every formula $\xi \in A_{\delta}$, the elements satisfying $\xi$ are bounded in $\mathcal{M}^*$. Again by saturation, there exists $b_{\gamma}$ such that no element $a>b_{\gamma}$ satisfies any formula $\xi \in A_{\delta}, \delta < \gamma$. In other words, for every element $a$ greater than $b_{\delta}$, $(\mathcal{M},a)\models U_{\gamma}$. Fix any such $b_{\gamma}$.
		
		Let $\psi=\exists y\phi(x,y) \in A_{\gamma}$ be an arbitrary formula which is satisfied for cofinally many elements in $\mathcal{M}^*$. Then the following formula $T^*(\xi)$ defines a predicate satisfying $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ in $\mathcal{M}^*$:
		\begin{displaymath}
			T^*(\xi):= \forall x \exists y> x\exists z \ \Big( \phi(y,z) \wedge \xi \in z \Big).
		\end{displaymath}
		I.e., $T^*$ says that there are arbitrarily large elements $y$ such that for some $z$, $\phi(y,z)$ holds and $\xi \in z$. We check that $T^*$ satisfies $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ in $\mathcal{M}^*$. We work in $\mathcal{M}^*$. Assume first $T^*(\qcr{\eta(t)}))$ holds. Let $a\in M^*$ be greater than $\max\{t, b_{\gamma}\}$. Then there are $b,c>a$ such that $\phi(b,c)$ and $\xi \in c$. Since $\exists y \phi(x,y)\in A_{\gamma}$ and $(\mathcal{M}^*,b)\models U_{\gamma}$, $c$ realizes the type $\tau(b,c)$. It follows by the definition of $\tau(x,y)$ that $\eta(\val{t})$ holds in $\mathcal{M}^*$. Assume conversely that $\eta(\val{t})$ holds. We show that $T^*(\eta(t))$ holds as well. Fix any $a$ and let $b$ be any element greater than $\max\{b_{\gamma}, a, t\}$ such that for some $c$, $\phi(b,c)$ holds. Since $(\mathcal{M}^*, b)\models U_{\gamma}$, it follows that $c$ realizes $\tau(b,y)$ and in particular, $\qcr{\eta(t)}\in c$. Since the initially chosen $a$ was arbitrary, it follows that $T^*(\qcr{\eta(t)})$.
		
		Since $T^*$ is in fact an $\mathcal{L}$-formula, by elementarity, $T^*$ witnesses that $\textnormal{ElDiag}(\mathcal{M})$ syntactically defines $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{proof}
	

	
	
	
	
	Using $\textnormal{UTB}^-$ as a bootstrap we can in fact give an example of the least theory, in the sense of semantic definability, which imposes recursive saturation. Recall the theory $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ from Remark \ref{rem_theory_of_realisers}.

    In the proof of Theorem \ref{tw_universality_rsat} we shall make use of the following result(\cite[Theorem 4.1]{wcislyk_models_weak})
    \begin{tw}\label{tw_CT_defines_UTB}
    Suppose that $\mathcal{M}\models \textnormal{PA} + \textnormal{CT}^-(a)$, where $a$ is nonstandard. Then there is a formula $\theta(x)\in\mathcal{L}_{\mathcal{M}}$ and a nonstandard $b$ such that $\mathcal{M}\models \textnormal{CT}(b)[\theta(x)/T(x)].$
    \end{tw}
	
	\begin{tw}\label{tw_universality_rsat}
		For an arbitrary theory $U\supseteq \textnormal{PA}$ in a countable language $\mathcal{L}$ extending $\textnormal{PA}$ the following conditions are equivalent:
		\begin{enumerate}
			\item $U$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation.
			\item $U$ semantically defines $\textnormal{RSAT}(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
		\end{enumerate}
	\end{tw}
	\begin{proof}
		The implication $2.\Rightarrow 1.$ is straightforward, so we prove the reverse direction. Assume $U$ imposes recursive saturation and take any $\mathcal{M}\models U$. Let $T(x)$ be a definable $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$-predicate and let $\mathcal{L}_T$ denote the language $\mathcal{L}_{\textnormal{PA}}\cup \was{T}$. For an arbitrary primitive recursive type $p(x,y)$, let $\was{\phi_i(x,y)}_{i\in\omega}$ be its p.r. enumeration. To enhance readability we will treat the function $i\mapsto \phi_i$ as a new primitive symbol (that should be eliminated by substituting the proper absolute $\Sigma_1$ representation of this function). Let Prog$_z$[$P(z,\bar{x})$] be the following formula ($P(z,\bar{x})$ is a placeholder for an arbitrary formula):
		\[\forall z \bigl(\forall i<z P(i,\bar{x})\rightarrow P(z,\bar{x})\bigr).\]
		We distinguish two cases:
		\paragraph{Case 1: The standard cut is definable in $\mathcal{M}$.} 
		
		Let $\omega(x)$ be a $\mathcal{L}(\mathcal{M})$ definition of the standard cut of $\mathcal{M}$. 
		Our definition of $R_p(x,y)$ formalizes the following definition by cases:
		\begin{displaymath}
				\begin{cases}\forall z \bigl(\omega(z)\rightarrow T(\phi_z(\dot{x},\dot{y})\bigr), &\textnormal{if } \textnormal{Prog}_v[\exists x\forall z<vT(\phi_z(\dot{x},\dot{y}))] \\ 
					\forall z<vT(\phi_z(\dot{x},\dot{y})), &\textnormal{if $v$ is the greatest such that }\bigcap_{z<v}\set{x}{T(\phi_z(\dot{x},\dot{y}))}\neq \emptyset
				\end{cases}
		\end{displaymath} 
		We now prove that this definition works. That the optimality axioms hold is clear: fix any parameter $y$ and any $n\in\omega$ and suppose that $\bigcap_{z<n}\set{x}{T(\phi_z(\bar{x},\bar{y}))}\neq \emptyset$. Then regardless of which case of our definition holds, any $x$ satisfying $R_p(x,y)$ belongs to the set $\bigcap_{z<n}\set{x}{T(\phi_z(\dot{x},\dot{y})}$, which, by the axioms of $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$, is the same as $\set{x}{\bigwedge_{z<n}\phi_z(x,y)}$. Let us deal with the  non-emptiness axioms. Fix any $y$. If $\neg \textnormal{Prog}_v[\exists x\forall z<vT(\phi_z(\dot{x},\dot{y}))]$, then by definition we have $\exists x R_p(x,y)$. Suppose now $\textnormal{Prog}_v[\exists x\forall z<vT(\phi_z(\dot{x},\dot{y}))]$ holds.
		Then $p(x,y)$ is realised, since $\mathcal{M}$ is recursively saturated. In particular $\exists x \forall z \bigl(\omega(z)\rightarrow T(\phi_z(\dot{x},\dot{y})\bigr)$, which concludes the (current case of the) proof.
		
		\paragraph{Case 2: The standard cut is not definable in $\mathcal{M}$.} 
		
		By the compositional axioms of $\textnormal{UTB}^-$ we have that for every $n\in\omega$ $(\mathcal{M},T^{\mathcal{M}})\models\textnormal{CT}^-(n)$. So, by our assumption there is a nonstandard number $a$ such that $(\mathcal{M}, T^{\mathcal{M}})\models \textnormal{CT}^-(a)$, i.e. $T$ is a compositional truth predicate for all sentences of depth at most $a$. Then, by Theorem \ref{tw_CT_defines_UTB}, 
		there is a $\mathcal{L}_{M}$- formula $T'(x)$ which defines a partial inductive satisfaction class, i.e. for some nonstandard $b$
		\[(\mathcal{M}, (T')^{\mathcal{M}})\models \textnormal{CT}^-(b) + \textnormal{Ind}_{\mathcal{L}_{T}}.\]
		Let us fix $T'$ and $b$ such that the above holds. Let $c$ be any nonstandard number such that $\mathcal{M}\models \forall i<c \ \phi_i\in\textnormal{dp}(b)$. Now we can simply define $R_p(x,y)$ to be the following formula:
		\rem{\begin{equation*}
				\exists v \bigl[\forall i <v T'(\phi_i(\dot{x},\dot{y})) \wedge  \forall v'>v \bigl(v'>c \vee \neg \exists z\forall i<v' T'(\phi_i(\dot{z},\dot{y}))\bigr) \bigr].
		\end{equation*}}
		Thus $R_p(x,y)$ defines the set $\bigcap_{z<v}\set{x}{T'(\phi_z(\dot{x},\dot{y}))}$, where $v$ is the greatest number $\leq c$ such that  the above intersection is not empty (by convention the intersection of the empty family is the whole universe of the model). Such a $v$ always exists by the fact that $(\mathcal{M}, (T')^{\mathcal{M}})\models \textnormal{Ind}_{\mathcal{L}_{T}}$. It is now a routine exercise to check that for this definition both the nonemptiness and optimality axioms hold.
	\end{proof}

	
	\begin{uwaga}
		It is easy to observe that Theorems \ref{th_recursive_saturation_implies_truth} and \ref{tw_universality_rsat} still hold if $\textnormal{PA}$ and $\mathcal{L}_{\textnormal{PA}}$ are substituted by a pair $V$, $\mathcal{L}$ such that $\textnormal{PA}\subseteq V$, $\mathcal{L}$ has at most countably many additional predicates and $V\vdash \textnormal{Ind}_{\mathcal{L}}$.
	\end{uwaga}
	

	
	By modifying the proof of Pakhomov and Visser (\cite[Theorem 4.1]{pakhomov_visser}) we can show that actually no finite theory can replace RSAT in Theorem \ref{tw_universality_rsat}:
	
	\begin{stwierdzenie}
		If $U$ is a finite theory such that $\textnormal{PA}+U$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, then there is a finite theory $V$ such that $\textnormal{PA} + V$ does not semantically define $U$ modulo $\mathcal{L}_{\textnormal{PA}}$ and $\textnormal{PA}+V$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation.
	\end{stwierdzenie}
	\begin{proof}
		In the proof all definability between theories is modulo $\mathcal{L}_{\textnormal{PA}}$. First observe that for a finite theory $U$ and an arbitrary theory $V$, $V$ semantically defines $U$ if and only if $V$ syntactically defines $U$. Fix $U$ and assume that $U$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation. For an arithmetical formula $\phi(x)$ let $\textnormal{CT}^-\restr{\phi(x)}$ denote the following $\mathcal{L}_T$ sentence:

		\[\forall x \bigl(\forall y<x \ \phi(y)\rightarrow \textnormal{CT}^-(\mathcal{L}_{\textnormal{PA}})(x)\bigr).\]
		Now apply the diagonal lemma to get a $\Sigma_1$ formula $\psi = \exists x \phi(x)$ such that
		\[\textnormal{EA}\vdash \psi\equiv "\textnormal{PA} + \textnormal{CT}^-\restr{\neg\phi(x)}\textnormal{ syntactically defines } U".\]
		We shall show that $\textnormal{CT}^-\restr{\neg\phi(x)}$ satisfies the requirements put on a theory $V$ in the thesis of our proposition. First, we claim that $\psi$ is false. Assume the opposite and take $n\in\omega$ such that $\textnormal{EA}\vdash \phi(\num{n})$. By the existence of partial truth predicates, it follows that $\textnormal{EA}$ defines $\textnormal{EA}+ \textnormal{CT}^-\restr{\neg\phi(x)}$. However, by the fixpoint property of $\psi$, it follows that $\textnormal{PA}$ defines $U$. Since $U+\textnormal{PA}$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, it follows that $\textnormal{PA}$ imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, which is obviously false.
		Hence $\psi$ is false and it follows that $\textnormal{PA}+\textnormal{CT}^-\restr{\neg\phi(x)}$ does not define $U$. We claim that $\textnormal{PA}+\textnormal{CT}^-\restr{\neg\phi(x)}$ imposes $\mathcal{L}_{\textnormal{PA}}$ recursive saturation. Indeed, fix any $\mathcal{M}\models \textnormal{PA} + \textnormal{CT}^-\restr{\neg\phi(x)}$. Since $\psi$ is false, then for every $n\in\omega$, $\mathcal{M}\models \neg\phi(\num{n})$, hence by the overspill principle, for some nonstandard $c$, $\mathcal{M}\models \forall x<c \neg\phi(x)$. As a consequence, $\mathcal{M}\models \textnormal{CT}^-(c)$. It follows by Lachlan's theorem (see \cite[Theorem 15.5]{kaye}) that $\mathcal{M}\restr{\mathcal{L}_{\textnormal{PA}}}$ is $\mathcal{L}_{\textnormal{PA}}$-recursively saturated, which ends the proof.
	\end{proof}
	
	Finally, we would like to return to Theorem \ref{th_theory_with_rec_sat_without_utb}. We will show that the infinite language we used in the proof of that theorem was not an indispensable ingredient of our argument. In the refined proof, instead of saying that an alleged definition of a truth predicate cannot use all the symbols, we will only say that it cannot have a bounded complexity. Thus, this shall fullfil our promise made in the introduction of delivering a theory in a finite language which defines $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ semantically but not syntactically. 
	
	In the proof, we will use properties of generic sets in computability theory. Our argument consists of two parts. We will first show in Lemma \ref{lem_hard_coding_in_N} that for an arbitrary $n$, we can find a set $A \subseteq \mathbb{N}$ (in the standard model) such that it defines the standard truth predicate for the arithmetical sentences, but not with a formula of complexity $\leq n$. To accomplish this, we amalgamate two constructions: (iterated) jump-inversion theorem and the construction of an $n$-generic (as presented in \cite[Chapter V]{odifreddiI} and \cite[Chapter XII]{odifreddiII}). Then we will show that this argument formalises in arithmetic and we will use Lemma \ref{lem_hard_coding_in_N} to construct a theory in a finite language which defines a $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ predicate in every model but does not do so uniformly. Below $\leq_T$, $\equiv_T$ denote Turing-reducibility and Turing-equivalence, respectively. 
	
	Let us recall the definition and the basic properties of an $n$-generic set.

	\begin{definicja} \label{def_arithmetical_forcing}
		Let $s$ be a finite binary sequence. We define the forcing relation $s \mathcal{V}dash \phi$ for $\phi$ first order formulae with a single second-order variable $X$ by induction on the complexity of $\phi$:
		\begin{itemize}
			\item If $\phi$ is a first-order atomic formula, then $s \mathcal{V}dash \phi$ iff $\mathbb{N} \models \phi$.
			\item If $\phi = n \in X$, then $s \mathcal{V}dash \phi$ iff $s(n) = 1$ (in particular $|s| > n$).
			\item If $\phi = \neg \psi$, then $s \mathcal{V}dash \phi$ iff for all $t \supseteq s$, $t \nVdash \psi$.
			\item If $\phi = \psi \vee \eta$, then $s \mathcal{V}dash \phi$ iff $s \mathcal{V}dash \psi$ or $s \mathcal{V}dash \eta$. 
			\item If $\phi = \exists x \psi(x)$, then $s \mathcal{V}dash \phi$ iff for some $n \in \mathbb{N}$, $s \mathcal{V}dash \psi(n)$. 
		\end{itemize} 
	\end{definicja}

    \begin{definicja}
    Let $A\subseteq \mathbb{N}$.
    \begin{itemize}
        \item We say that $A$ forces $\phi$, $A\mathcal{V}dash \phi$ iff for some finite $s\subseteq A$, $s\mathcal{V}dash \phi$.

        \item $A$ is $n$-generic iff for every $\Sigma^0_n$ sentence $\phi$ $A\mathcal{V}dash \phi$ or $A\mathcal{V}dash \neg\phi$.
    \end{itemize}
    \end{definicja}

    \begin{tw}
    A set $A\subseteq \mathbb{N}$ is $n$-generic iff for every $\phi\in\Sigma^0_n \cup \Pi_n^0$, $(\mathbb{N},A)\models \phi$ iff $A\mathcal{V}dash \phi$.
    \end{tw}
	
	\begin{lemat} \label{lem_hard_coding_in_N}
		For any $n \in \omega$, there exists a set $A \subseteq \mathbb{N}$ such that $\textnormal{Th}(\mathbb{N})\subseteq\mathbb{N}$ is definable in $(\mathbb{N},A)$, but $\textnormal{Th}(\mathbb{N})$ is not definable in $(\mathbb{N},A)$ with a formula of complexity $< \Sigma_n$.
	\end{lemat}
	\begin{proof}
		For a given $n$, we will find a set $A$ such that:
		\begin{itemize}
			\item[a.] $A \oplus 0^{(n)}$ computes $0^{(\omega)}$.
			\item[b.] $A \oplus 0^{(n)}$ computes $A^{(n)}$. 
		\end{itemize}
		We claim that if $A$ satisfies a. and b., then $\textnormal{Th}(\mathbb{N})$ is not definable in $(\mathbb{N},A)$ with a formula of complexity $k< n$.

		 If it is, then $0^{(\omega)} \leq_T  A^{(k)}.$ This yields a contradiction as follows:
		\begin{displaymath}
			A^{(n)} \leq_T 0^{(n)} \oplus A \leq_T 0^{(\omega)} \oplus A \leq_T  A^{(k)}. 
		\end{displaymath}
		
		Condition a. will be guaranteed by the construction from the Jump Inversion Theorem (see \cite[Theorem V.2.24]{odifreddiI}) while b. will be guaranteed by the construction of an $n$-generic (see \cite[XII.1.11]{odifreddiII}). 

		As stated in \cite[Proposition XII.1.6]{odifreddiII}, the restriction of the forcing relation to $\Sigma_n$ sentences is computable in $0^{(n)}$. We fix an enumeration $\phi_i(X)$ of $\Sigma^0_n$ formulae with one second-order variable 

		 and an enumeration $\xi_i$ of all $\mathcal{L}_{\textnormal{PA}}$ sentences.
		
		We construct $A$ in stages. At each stage $n$, we have a finite binary sequence $s_n$. We proceed as follows:
		\begin{itemize}
			\item If $n+1$ is even, say $2k$, then we look at the formula $\phi_k$. If there exists an extension $s \supsetneq s_n$ such that $s\mathcal{V}dash \phi_k$ holds, then we let $s_{n+1}$ be the lexicographically least such $s$. If not, we let $s_{n+1} :=s_n$. 
			\item If $n+1$ is odd, say $2k+1$, then we set $s_{n+1}$ equal to $s_n\frown \tuple{1}$ if $\xi_k$ is true and $s_n\frown \tuple{0}$ if it is false.
		\end{itemize}
		Finally, we let $s= \bigcup s_n$ and we let $A$ be the only set whose characteristic function is $s$. Clearly, $A$ is $n$-generic.
		
		Indeed, assume that $A\nVdash \phi$ and $\phi = \phi_k$. By definition, for every $s\subseteq A$, $s\nVdash \phi_k$. In particular $s_{2k}\nVdash \phi_k$, hence $s_{2k} = s_{2k-1}$. Moreover no $\tau\supset s_{2k}$ forces $\phi_k$, so in particular we get that $s_{2k}\mathcal{V}dash \neg\phi_k$. This concludes the proof of $n$-genericity of $A$. We want to check that $A$ satisfies both conditions a. and b. 
		
		\paragraph*{Claim I: $A \oplus 0^{(n)}$ computes $0^{(\omega)}$.}
		
		The set $0^{(\omega)}$, the simple join of $0^{(k)}$ for $k < \omega$ is the Turing degree of the standard arithmetical truth predicate $\textnormal{Th}(\mathbb{N})$. We will show how to compute the latter set from $A \oplus 0^{(n)}$. Fix any $k$. We want to decide whether $\xi_k \in \textnormal{Th}(\mathbb{N})$. We inductively compute the sequence of finite sequences
		\begin{displaymath}
			s_0 \subseteq s_1 \subseteq \ldots \subseteq s_{2k+1}.
		\end{displaymath}
		Suppose that we know $s_{2m}$. Then we compute $s_{2m+1}$ as the only one-step extension of $s_{2m}$ agreeing with $A$. On the other hand, if we know $s_{2m-1}$, we can define $s_{2m}$ as the lexicographically smallest sequence extending $s_{2m-1}$ and forcing $\phi_m$. 
		
		Finally, we set $\xi_k \in \textnormal{Th}(\mathbb{N})$ iff $s_{2k+1}$ extends $s_{2k}$ with a single digit $1$. 
		
		\paragraph*{Claim II: $A^{(n)} \equiv_T A \oplus 0^{(n)}$.}
		
		It is enough to show that $A^{(n)} \leq_T A \oplus 0^{(n)}$. We want to check, for any $\Sigma_n^0(A)$ formula $\phi$ whether $\phi(A)$ holds. As noted before, we can compute the sequence $s_0, s_1, s_2, \ldots$ from $A\oplus 0^{(n)}$. Assume that $\phi = \phi_k$. We claim that $\phi_k(A)$ holds iff $s_{2k}$ nontrivially extends $s_{2k-1}$. Since $A$ is $n$-generic, we can reason as follows: 
		\begin{align*}
			(\mathbb{N},A)\models \phi_k(A) &\equiv A\mathcal{V}dash \phi_k\\
			&\equiv \exists s\subset A\ \ s\mathcal{V}dash \phi_k\\
			&\equiv s_{2k}\mathcal{V}dash \phi_k\\
			&\equiv s_{2k-1}\subsetneq s_{2k}
		\end{align*}
		The first equivalence is by \cite[Proposition XII.1.10]{odifreddiII}, the second is a definition, the third and fourth follow by the construction. Now, notice that the sequences $s_i$ can be computed using  $A \oplus 0^{(n)}$ as an oracle. Indeed, in order to compute $s_{2k}$ from $s_{2k-1}$, we only need to know whether there exists $s \supsetneq s_{2k-1}$ such that $s \mathcal{V}dash \phi_k$ which, as we already mentioned, is a $\Sigma_n$ fact. In order to compute $s_{2k+1}$ from $s_{2k}$, we only have to check whether the corresponding single digit of the set $A$ is $0$ or $1$. This concludes the argument and completes the proof of the lemma. 

	\end{proof}
	
	In Lemma \ref{lem_hard_coding_in_N}, we produced some subsets of $\mathbb{N}$ which define $\textnormal{Th}(\mathbb{N})$ but only with a formula no simpler than a fixed complexity $k$. We will check that the construction can actually be captured by a \emph{theory}, which allows us to improve Theorem \ref{th_theory_with_rec_sat_without_utb} to theories in finite languages. 
	
	\begin{tw} \label{th_theory_finlang_with_rec_sat_without_utb}
		There exists a theory $U$ in a finite language extending $\textnormal{PA}$ which imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation but does not syntactically define $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$ modulo $\mathcal{L}_{\textnormal{PA}}$.
	\end{tw}
	
	\begin{proof}
		As previously, in the proof all definability between theories is modulo $\mathcal{L}_{\textnormal{PA}}$. Let us fix a primitive recursive enumerations $(\phi_i)$ of arithmetical formulae and, for each $k$, $(\psi^k_j)$ of arithmetical $\Sigma_k$ sentences with a single second order variable $X$. We shall construct a theory $U$ in the arithmetical language expanded with two predicates $A$, $T_\omega$, and a constant $c$. The axioms of $U$ will comprise the axioms of $\textnormal{PA}$, full scheme of induction for the extended language and an infinite list of axioms described below.
		
		We first define an auxiliary sequence of theories. For each $k$, the theory $\alpha_k$ says that $A$ arises from a construction of the $k$-generic code of $\textnormal{Th}(\mathbb{N})$. More precisely, $\alpha_k$ consists of sentences $\alpha_k^{\phi(x)}$, for $\phi(x)\in\mathcal{L}_{\textnormal{PA}}$, where $\alpha_k^{\phi(x)}$ says: 
		\begin{center}
			,,For each $x$, there exists an $m$ and a sequence of finite sequences $\emptyset = s_0 \subseteq s_1 \subseteq \ldots \subseteq s_m$ satisfying the conditions specified below, such that for all $y \leq x$, $A(y)$ iff $s_m(y) =1$, where the conditions on the sequences $s_{i+1}$ are as follows:
			\begin{itemize}
				\item Case I: if $j = 2l$ for some $l$, then
				\begin{itemize}
					\item If there exists a sequence $s \supsetneq s_{j}$ such that $s\mathcal{V}dash \psi^k_j$, then $s_{j+1}$ is the lexicographically minimal such $s$ strictly extending $s_j$.
					\item $s_{j+1} = s_j$, otherwise. 
				\end{itemize}
				\item Case II: if $j = 2l+1$, then $s_j = s_{2l} \frown \tuple{i}$ for $i \in \{0,1\}$; moreover, if there exists a closed term $t$ such that $\phi_j = \phi(t)$,  then:
				\begin{itemize}
					\item If $\phi(\val{t})$, then $s_{j+1} = s_j \frown \tuple{1}$.
					\item If $\neg \phi(\val{t})$, then $s_{j+1} = s_j \frown \tuple{0}$.
				\end{itemize} 
			\end{itemize}

		\end{center}
		Note that, while in Case I there is no bound on the number of bits $s_{j+1}$ adds to $s_j$, in Case II $s_{j+1}$ is always an extension of $s_j$ by a single bit.
		
		Finally, $U$ is the union of the following sentences:	
		\begin{itemize}
			\item $	\textnormal{PA}$.
			\item The full induction scheme for the extended language.
			\item $c=\num{k} \rightarrow \alpha_k^{\phi(\bar{x})}$, for $\phi$ formulae of $\mathcal{L}_{\textnormal{PA}}$.
			\item $	c > \num{3m} \rightarrow \forall t\Big(T_{\omega}(\qcr{\phi_m(t)}) \equiv \phi_m(\val{t})\Big)$.
		\end{itemize}
		
		It is enough to check that $U$ defines $\textnormal{UTB}$ semantically but not syntactically.
		
		\textbf{Claim I: $U$ defines $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$ semantically}
		
		Let $\mathcal{M} \models U$. Then, in $M$, $c$ is either a standard or a nonstandard number. If $c$ is nonstandard, then $T_{\omega}$ satisfies $\textnormal{UTB}$. If $c = k \in \omega$, then fix any standard arithmetical formula $\phi$ and a closed term $t\in M$ (perhaps nonstandard). We desrcibe an $\mathcal{M}$-definable procedure for checking whether $\phi(\val{t})$ holds in $\mathcal{M}$.
		
		Fix $d$ such that $\phi(t) = \phi_d$ in our enumeration. We perform the construction of $A$. Notice that initial segments of the sequence $s_0 \subseteq s_1 \subset \ldots$ defined in the axiom $\alpha^{\phi(x)}_k$ are actually definable from $A$: the even steps are computable in the sense of $\mathcal{M}$ using as the oracle the definable set of all true $\Sigma_k$ sentences (with parametres). The odd steps are directly definable in the oracle $A$ (we simply check whether $A$ has $0$ or $1$ in the respective places). In particular, we set $T(\phi(t))$ iff the last bit of $s_{2d+1}$ is $1$. 
		
		\textbf{Claim II: $U$ does not syntactically define $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$}
		
		Suppose that $U$ syntactically defines $\textnormal{UTB}(\mathcal{L}_{\textnormal{PA}})$ with a formula $\phi$. Suppose that $\phi \in \Sigma_{k}$. Consider the model $\mathcal{N}$ whose arithmetical part is the standard model $\mathbb{N}$, the constant $c$ is interpreted as $3k$, $T_{\omega}$ is interpreted as the partial arithmetical truth predicate for the arithmetical $\Sigma_{k}$ formulae (which can be assumed to include $\phi_0, \ldots, \phi_{k-1}$) and $A$ is the set constructed in the proof of Lemma \ref{lem_hard_coding_in_N} for $n= 3k$.	Then obviously $\mathcal{N}\models U$. 
		
		In the $\Sigma_k$ formula $\phi$, we can substitute the partial arithmetical predicate $\textnormal{Tr}_{\Sigma_{k}}$ for $T_{\omega}$ and $\num{3k}$ for $c$, obtaining a $\Sigma_{2k+1}$ formula $\phi^*$ which defines $\textnormal{Th}(\mathbb{N})$ in $(\mathbb{N}, A)$. However, by Lemma \ref{lem_hard_coding_in_N}, for any $l<3k$, $\textnormal{Th}(\mathbb{N})$ cannot be defined with a $\Sigma_{l}$ formula from the predicate $A$. 
	\end{proof}

	
	
	\section{Summary and open problems}
	
	As we mentioned in the introduction, the questions which we tackle in this article have several different ``dimensions''. In order to facilitate navigating between them, we summarise our findings below.
	
	The table below concerns the problem which theories impose truth-like semantic properties. 
	\begin{center}
		
		\begin{tabular}{c||c|c||c|c||c|c||c}
			
			&\multicolumn{6}{c||}{Sequential theories, finite languages} & $\textnormal{PA}$, ctble languages \\ 
			\cmidrule{2-8}
			& \multicolumn{2}{c||}{ImpElemEq} & \multicolumn{2}{c||}{PreservDef} & \multicolumn{2}{c||}{ImpElem} & \multirow{2}{*}{\cellcolor{gray!10}ImpRecSat}\\ \cmidrule{2-7}
			& \cellcolor{gray!10}non-Uni & \cellcolor{gray!40}Uni & \cellcolor{gray!10}non-Uni & \cellcolor{gray!40}Uni &\cellcolor{gray!10}non-Uni & \cellcolor{gray!40}Uni &\cellcolor{gray!10} \\ \toprule
			Sem. defi. & \cellcolor{gray!10}$\textnormal{TB}$ & \cellcolor{gray!40}$\textnormal{TB}$ & \cellcolor{gray!10}$\textnormal{DEF}$  &  \cellcolor{gray!40}$\textnormal{DEF}$ & \cellcolor{gray!10}$\textnormal{USB}$ & \cellcolor{gray!40}$\textnormal{USB}$ & \cellcolor{gray!10}$\textnormal{RSAT}$\\ \hline
			Synt. defi. & none & \cellcolor{gray!40}$\textnormal{TB}$ & none & \cellcolor{gray!40}$\textnormal{DEF}$ & none & \cellcolor{gray!40}$\textnormal{USB}$ & none	\\
			\bottomrule
		\end{tabular}
	\end{center}
	The first row contains information	for which theories our classification works. The second row contains (the abbreviations of) the main model-theoretic properties considered in this paper. The first three come in two variants: uniform and non-uniform. The row "Sem. (Synt.) defi." contains theories that are characterized by the respective property up to semantic (syntactic) definability. When we write "none," this means that none \textit{of the main theories} is characterized by the respective property. In all the cases the theory defined in the proof of Theorem \ref{th_theory_finlang_with_rec_sat_without_utb} serves as a counterexample. Moreover, in the semantic sense and for extensions of $\textnormal{PA}$, the non-uniform versions of the properties get properly more restrictive from left to right (light grey properties and theories). For instance, every theory which imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation (for extensions of $\textnormal{PA}$) preserves $\mathcal{L}_{\textnormal{PA}}$-definability, but there is a theory ($\textnormal{DEF}$) which preserves $\mathcal{L}_{\textnormal{PA}}$-definability but does not impose $\mathcal{L}_{\textnormal{PA}}$-recursive saturation. The same holds over all natural sequential theories, except for some degenerate cases, for uniform versions of model-theoretical properties and their respective theories (dark grey properties and theories).

	In this article, we have also analysed and investigated relations between the axiomatic theories corresponding to the semantic properties which truth-like predicates can impose. We would now like to lay down a diagram depicting the interdependencies between those theories. 
	
	Below, by writing a filled-arrow from $U$ to $V$, we mean that $V$ defines $U$ \textbf{syntactically} (think of that as a statement that $U$ embeds into $V$). Whenever we \emph{do not} write an arrow from $V$ to $U$ this means that $V$ does not define $U$ \textbf{semantically}, over any sequential theory. The only exception is when there is a path consisting of other arrows. If we \emph{do not know} whether $V$ \textbf{semantically} defines $U$ or this happens sometimes but not in typical cases, we write a dashed arrow with a question mark (which always means that we do not even know whether semantic definability obtains) and, possibly, some comments as to what is known.
	\begin{displaymath}
		\xymatrix{
			&  & & \textnormal{RSAT}  & & \\
			& & & & & \\
			& &  & \textnormal{S} \ar @{-->} [dd]|{\txt{\scriptsize{PA} \\ \scriptsize{in general ?}}} \ar @{-->} [uu]|{\txt{\scriptsize{PA} \\ \scriptsize{in general ?}}} \ar @/^/ [drr]  \ar @{-->} @/_/ [lld]_{\txt{\scriptsize{PA} \\ \scriptsize{in general ?}}} & & \\
\textnormal{TB} \ar @/^/ [r]^{\txt{\scriptsize
		{def. elem.}}} & \textnormal{DEF} \ar @/^2.3pc/ [uuurr] \ar @/^/ @{-->} [l]^{\txt{\scriptsize{few def. elem.} \\ \scriptsize{in general no}}}	\ar @/_/ [urr] \ar @/_/ [drr]	& & & & \textnormal{US} \ar @{-->} @/_2.3pc/ [uuull]_{\txt{\scriptsize{PA} \\ \scriptsize{in general no}}} \ar @{-->} @/^/ [lld]^{\txt{\scriptsize{PA} \\ \scriptsize{in general no}}} \\
 	& & & \textnormal{USB} \ar@/_3.5pc/  [uuuu]  \ar @/^/ [urr] & &
		}
	\end{displaymath}
Most of the entries in the diagram, both positive and negative are directly stated in this article, mostly in Section \ref{sec_definability_between_theories}. The fact that there is no arrow from $\textnormal{US}$ to $\textnormal{S}$ follows from the fact that $\textnormal{US}$ naturally defines $\textnormal{USB}$ and by Proposition \ref{stw_S_nie_definiuje_USB}, we know that over no sequential theory can $\textnormal{S}$ define $\textnormal{USB}$ semantically, so any arrow from $\textnormal{US}$ to $\textnormal{S}$ would yield a nonexistent arrow between $\textnormal{USB}$ and $\textnormal{S}$.

The theory $\textnormal{RSAT}$ is a bit of an outlier.\footnote{In this article, we have defined $\textnormal{RSAT}$ only in the context of $\textnormal{PA}$. However, one could formulate a definition suitable for arbitrary sequential theories, following the cases of other theories, like $\textnormal{USB}$.} First, notice that over an arbitrary sequential theory $\textnormal{RSAT}$ imposes recursive saturation which in general none of the other listed theories does, so it is not semantically definable over any of them. 

On the other hand, it can be easily checked that $\textnormal{RSAT}_K$ syntactically defines $\textnormal{USB}_K$ (hence also $\textnormal{DEF}_K$). Namely $S(\qcr{\phi(x)},y)$ holds iff $\forall x \bigl(R(p_{\phi(y)},x,y)\rightarrow \num{1}(x)\bigr)$, where $p_{\phi(y)}$ is the (easily definable from $\qcr{\phi(y)}$)) one-element type
\begin{displaymath}
	(\phi(y)\wedge \num{1}(x)) \vee (\neg\phi(y)\wedge \num{0}(x)).
\end{displaymath}
It follows that, over theories containing $\textnormal{PA}$, $\textnormal{RSAT}_{id}$ defines $\textnormal{US}_{id}$. Moreover, the proof of Theorem \ref{tw_nondef_US_in_UTB} can be adapted to show that over theories in $\mathcal{L}_{\textnormal{PA}}$ consistent with $B\Sigma_n+\neg I\Sigma_n + \exp$, $\textnormal{RSAT}_{id}$ does not semantically define $\textnormal{US}_{id}$: given a recursively saturated model $\mathcal{M}\models B\Sigma_n+\neg I\Sigma_n + \exp$ one finds a $A$ set which is definable with a parameter $a\in M$ but which does not contain any element definable from $a$. Then one canonically expands $\mathcal{M}$ to a model of $\textnormal{RSAT}_{id}$ by interpreting $R(p,x,b)$ to be the set of all elements which realize the maximal fragment of $\was{\phi_i^p(x,b)}$. The automorphism group of the expanded model is the same as that of $\mathcal{M}$ and one can simply rewrite the rest of the proof. In the case of general theories, essentially nothing else is known. 

	
Below we list some open questions and perspectives for further research.
	\begin{enumerate}
		\item[Q1] In this article, we considered the notion of definability preservation (so arithmetically definable elements satisfy the same definitions between submodels of a given theory). We also considered theories which impose equality of definables, but we were unable to provide a good characterisation of such theories. One possible candidate is the theory $\textnormal{DEF}$ of definability. 
		
	\textit{
			Let $U$ be any sequential theory in a language $\mathcal{L}$ and $K: S^1_2\lhd U$. Is there an r.e. sequential theory in a finite language which imposes equality of $\mathcal{L}$ definables but does not semantically define $\textnormal{DEF}_K(\mathcal{L})$ modulo $\mathcal{L}$? If the answer is negative, how about syntactic definability of $\textnormal{DEF}_K(\mathcal{L})$ (modulo $\mathcal{L}$)?
	}

	\item[Q2] Most questions about relationships between semantic properties and defining respective theories investigated in this paper found a definite answer. However, this is not quite so in the case of the recursive saturation. There are three reasons for that: first of all, we assume that our theory contains full $\textnormal{PA}$, and consequently we loose a lot o generality. Secondly we are only able to obtain semantic, rather than syntactic definability of $\textnormal{RSAT}$ which makes our characterisation deficient in a sense, because it is not a nice ``completeness-style'' result of the kind which holds for other semantic notions of interest. However, our counterexamples seem to make the essential use of the fact that the theory in question is infinite.  Thirdly, our characterisation works only for theories in countable languages (because of the use of the Omitting Types Theorem). These three issues lead to the following questions: 
	
	\textit{Assume that $U$ is a finite theory with $\textnormal{PA}\subset U$ which imposes $\mathcal{L}_{U}$-recursive saturation. Does $U$ define $\textnormal{RSAT}_{id}(\mathcal{L}_{\textnormal{PA}}$) syntactically?}
	
	\textit{Assume that $U$ is a sequential theory in a countable language $\mathcal{L}_U \supset \mathcal{L}$ with $K: S^1_2 \lhd U$ which imposes $\mathcal{L}$-recursive saturation. Does $U$ define $\textnormal{RSAT}_{K}(\mathcal{L})$ semantically? Assume that $U$ is finite. Does it define $\textnormal{RSAT}_{K}(\mathcal{L})$ syntactically?}
	
	\textit{Assume that $U$ is an arbitrary theory with $\textnormal{PA}\subset U$ (not necessarily in a countable language) which imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation. Does $U$ define $\textnormal{RSAT}_{id}(\mathcal{L}_{\textnormal{PA}}$) semantically?}
	
		\item[Q3] We know that for theories $U$ extending $\textnormal{PA}$ with the identity embedding of $S^1_2$, $\textnormal{USB}_{id}(\mathcal{L}_{U})$ defines $\textnormal{S}_{id}(\mathcal{L}_{U})$. However, the use of $\textnormal{PA}$ seems essential for this definability and we can expect that the methods used to separate $\textnormal{USB}$ from $\textnormal{US}$ can be modified to get this stronger separation. We note that by Theorem \ref{stw_nondef_H_usb} over any finite fragment of $\textnormal{PA}$, $\textnormal{USB}_{id}$ does not \textit{parameter-free} semantically define $S_{id}$. However, at this point we cannot exclude the existence of a definition with parameters.
		
		\textit{Let $U$ be an r.e. sequential theory and let $K:S^1_2\lhd U$. Does $\textnormal{USB}_K(\mathcal{L}_U)$ semantically define $\textnormal{S}_K(\mathcal{L}_U)$ modulo $\mathcal{L}$ (possibly with parametres)? Does it hold if we take $U$ to be a finite fragment of $\textnormal{PA}$ and $K$ to be the identity embedding?} 

		\item[Q4] One arrow from our diagram of the interdependencies between theories is missing and it is really not clear what kind of separation should hold between them. 
		
		\textit{Let $U$ be an r.e. sequential theory and let $K:S^1_2\lhd U$. Does $\textnormal{DEF}_K(\mathcal{L}_U)$ semantically define $\textnormal{S}_K(\mathcal{L}_U)$ modulo $\mathcal{L}_U$?}
		
		\item[Q5] As we have already mentioned, the status of $\textnormal{RSAT}$ in the diagram of definability between theories is completely open, besides rather trivial observations. 
		
		\textit{Let $U$ be an r.e. sequential theory and let $K:S^1_2\lhd U$. Does $\textnormal{RSAT}_K(\mathcal{L}_U)$ semantically define $\textnormal{S}_K(\mathcal{L}_U)$ modulo $\mathcal{L}_U$? Does it define $\textnormal{USB}_K(\mathcal{L}_{U})$?}

		\item[Q6] In this article, we have investigated relations between semantic properties of theories and defining truth-like predicates as well as definability relations between those predicates. Those results combined allow us to obtain some implication between various semantic properties themselves. For instance, if $U$ contains $\textnormal{PA}$ and imposes $\mathcal{L}_{\textnormal{PA}}$-recursive saturation, then it also imposes $\mathcal{L}_{\textnormal{PA}}$-elementarity between the models. While we have not systematically investigated this kind of relations, we observed that at least some of them lead to nontrivial questions, especially if we impose additional conditions, such as finiteness of theories. Possibly more questions in this spirit can be formulated.
		
		
		 \textit{Let $\mathcal{L}$ be a language. Is there a finite sequential theory which (uniformly) imposes $\mathcal{L}$-elementary equivalence but does not (uniformly) preserve $\mathcal{L}$-definability? Same question for the pair preserving definability/imposing elementarity.}
	
		\item[Q7] Above, we have already asked whether $\textnormal{RSAT}$ can be defined semantically in general sequential theories imposing recursive saturation. The following question approaches this problem from a somewhat different angle.
		
		\textit{Let $\mathcal{L}$ be a language. Is there a finite sequential theory which imposes $\mathcal{L}$-recursive saturation but does not uniformly impose $\mathcal{L}$-elementarity?}
	
		\item[Q8] In Subsection \ref{subsect_PA_def_inno}, we analysed definability between the predicates satisfying theories of truth-like notions in specific models. We established that in every nonstandard model of $\textnormal{PA}$, there exists a predicate satisfying $\textnormal{TB}^-$ which does not allow us to define a predicate satisfying $\textnormal{USB}^-$ and, similarly, that predicates satisfying $\textnormal{DEF}^-$ are definable from predicates satisfying $\textnormal{TB}^-$ only in the models of $\textnormal{Th}(\mathbb{N})$. This sort of questions about interdefinability of truth-like theories can be extended to other theories we introduced in this paper. For instance, we can ask about the relationship between $\textnormal{DEF}^-$ and $\textnormal{USB}^-$.
		
		\textit{For which models $\mathcal{M}\models \textnormal{PA}$ it holds that for every $D\subseteq M^2$ such that $(\mathcal{M},D)\models \textnormal{DEF}^-(\mathcal{L}_{\textnormal{PA}})$, $\textnormal{ElDiag}(\mathcal{M},D)$ defines $\textnormal{UTB}^-(\mathcal{L}_{\textnormal{PA}})$? We conjecture that these are precisely the prime models of $\textnormal{PA}$.}
	\end{enumerate}
	
	

	

	

\end{document}