Recall the notion of [[Club sets and stationary sets#Club and stationary subsets of $P_{ omega_{1}}(X)$|generalized stationarity]] in $\mathcal{P}_{\omega_{1}}(X)$:
>[!info] Definition
>or an arbitrary set $X$, $C\subseteq\mathcal{P}_{\omega_{1}}(X)$ is called *club in $\mathcal{P}_{\omega_{1}}(X)$* if there is some algebra $\mathfrak{A}=\left\langle X,f_{n}\right\rangle _{n<\omega}$ (where $f_{n}:X^{k}\to X$ for some $k$) such that $C=C_{\mathfrak{A}}:=\left\{ z\in\mathcal{P}_{\omega_{1}}(X)\mid\forall n(f_{n}''z^{k}\subseteq z)\right\}$ i.e the collection of all subsets of $X$ closed under all functions of $\mathfrak{A}$.
>$S\subseteq\mathcal{P}_{\omega_{1}}(X)$ is called *stationary in $\mathcal{P}_{\omega_{1}}(X)$* if for every algebra $\mathfrak{A}$ on $X$, $S\cap C_{\mathfrak{A}}\ne\varnothing$.
^def-stationarity
>[!info] Definition
>Stationary logic $\mathcal{L}(\mathtt{aa})$ is obtained from first order logic by allowing variables representing countable subsets and adding the following (dual) quantifiers:
>$\begin{aligned} \mathcal{M}\vDash\mathtt{aa}s\varphi\left(s,\boldsymbol{t},\boldsymbol{a}\right)\iff & \left\{ A\in\mathcal{P}_{\omega_{1}}(M) \mid\mathcal{M}\vDash\varphi\left(A,\boldsymbol{t},\boldsymbol{a}\right)\right\} \\
> & \textstyle \text{contains a club in }\mathcal{P}_{\omega_{1}}(M) \\\mathcal{M\vDash\mathtt{stat}}s\varphi\left(s,\boldsymbol{t},\boldsymbol{a}\right)\iff & {\left\{ A\in\mathcal{P}_{\omega_{1}}(M)\mid\mathcal{M}\vDash\varphi\left(A,\boldsymbol{t},\boldsymbol{a}\right)\right\} } \\
> & \textstyle \text{is stationary in } \mathcal{P}_{\omega_{1}}(M)
> \end{aligned}$
> where $\boldsymbol{a}$ is a finite sequence of elements of $M$ and $\boldsymbol{t}$ a finite sequence of countable subsets of $M$.
^def-logic
## Kueker's game-theoretic description
If $X \subseteq P_{\omega_1}(A)$, then $X$ contains a club iff $\forall x_0 \exists y_0 \forall x_1 \exists y_1 \ldots \forall x_n \exists y_n \ldots\left(\left\{x_i: i<\omega\right\} \cup\right.$ $\left\{y_i: i<\omega\right\} \in X$ ).
# Expressive power
- " $\varphi(\cdot)$ is countable": $\mathtt{aa}s\forall y(\varphi(y) \rightarrow s(y))$.
- Assume $\varphi(\cdot, \cdot)$ defines a linear order
- $\varphi(\cdot, \cdot)$ has cofinality $\omega$ : $\mathtt{aa}s \forall x \exists y(\varphi(x, y) \wedge s(y))$.
- $\varphi(\cdot, \cdot)$ is $\aleph_1$-like: $\forall x \mathtt{aa} s\forall y(\varphi(y, x) \rightarrow s(y))$.
- There is a $\sup$-preserving mapping from $\langle \omega_{1},< \rangle$ to $\varphi(\cdot,\cdot)$: $\mathtt{aa}s \exists x \forall y (s(y)\to y<x)$.
- $\varphi(\cdot, \cdot)$ is separable: $\mathtt{aa}s \forall x,y(\varphi(x,y)\to \exists z (s(z))\land \varphi(x,z)\land \varphi(z,y))$
- $\varphi(\cdot, \cdot)$ contains a closed unbounded subset (i.e. a copy of $\omega_1$ ): $\mathtt{aa}s(\sup (s) \in \operatorname{dom}(\varphi))$
- The set $\{\alpha<\kappa: \operatorname{cf}(\alpha)=\omega\}$ is $\mathcal{L}(\mathtt{aa})$ definable on $(\kappa,<)$ by means of $\mathtt{aa}s(\sup (s)=\alpha)$.
- The property of a set $A \subseteq$ $\{\alpha<\kappa: \operatorname{cf}(\alpha)=\omega\}$ of being stationary is definable in $\mathcal{L}(\mathtt{aa})$ by means of $\mathtt{stat}s(\sup (s) \in A)$.
- $E$ is an equivalence relation with countably many classes: $\mathtt{aa}s \forall y \exists z(s(z)\land E(y,z))$
**Remark.** This is Keisler's counterexample for interpolation in $\mathcal{L}(Q_{1})$.
- ![[Dense linear ordering#$ omega_{1}$-like dense linear ordering]]
For any $A \subseteq \omega_{1}$, $A$ contains a club iff $\Phi(A)\vDash \mathtt{aa} s \exists x \forall y\in s (y<x \to \exists z\in s (s<x))$.
# Properties
## Completeness
[[Barwise, Kaufmann, Makkai - Stationary logic]]
The following axioms (with the addition of axioms for first order logic) give a complete axiomatization of the logic $\mathcal{L}(\mathrm{aa})$:
$(A 0) \quad \mathtt{aa}s \varphi(s) \leftrightarrow \mathtt{aa}t \varphi(t)$
$(A 1) \quad \neg \mathtt{aa}s(\perp)$
$(A 2) \quad \mathtt{aa}s(x \in s)$, $\mathtt{aa}t(s \subseteq t)$
$(A 3) \quad(\mathtt{aa}s \varphi \wedge \mathtt{aa}s \psi) \rightarrow \mathtt{aa}s(\varphi \wedge \psi)$
$(A 4) \quad \mathtt{aa}s(\varphi \rightarrow \psi) \rightarrow(\mathtt{aa}s \varphi \rightarrow \mathtt{aa}s \psi)$
$(A 5) \quad \forall x \mathtt{aa}s \varphi(x, s) \rightarrow$ $\mathtt{aa}s \forall x \in s \varphi(x, s)$.
Where the rules are Modus Ponens, generalization and $\mathtt{aa}$-generalization: if $T\vdash \varphi\to \psi$ and $s$ is not free in $T\cup \{\varphi\}$ then $T\vdash \varphi\to \mathtt{aa}s\psi$.
>[!note] Remark
> - While $\mathtt{aa}s\ \mathtt{aa}t\ (s \subseteq t)$ is an axiom, $\mathtt{aa}t\ \mathtt{aa}s\ (s \subseteq t)$ is always false.
## Compactness
Countably compact (Compactness for countable vocabularies).
## Löwenheim-Skolem
Downward Löwenheim-Skolem down to $\aleph_{1}$ for countable theories - every countable consistent theory has a model of cardinality $\aleph_{1}$.
# Games / Back-and-Forth systems
## Kaufmann
[[Kaufmann - SOME RESULTS IN STATIONARY LOGIC]]
![[Kaufmann - SOME RESULTS IN STATIONARY LOGIC#^a59ff8]]
In terms of games, this corresponds to a game of length $\alpha+1$ where there are two types of moves Player I can choose from:
- $\exists$-move: Player I chooses an element in one of the model, Player II responds with an element of the other model.
- $\mathtt{stat}$-move:
- Player II chooses a club of countable subsets from one model
- Player I then chooses a member of this club
- Player II responds with a stationary set of the other model.
- Player I chooses a member of this stationary set
- The club and stationary sets are forgotten.
*Justification:* Player I is $\forall$ and Player II is $\exists$. Clause (iii) for example reads
$
\exists C \text{club} \forall s\in C \exists S_{s} \text{stationary}\forall t\in S_{s} [\dots]
$
Also note that this is considered a $\mathtt{stat}$ move and not an $\mathtt{aa}$ move, as it is used to show that if $A\vDash \mathtt{stat}s\varphi$ then also $B \vDash \mathtt{stat}s \varphi$.
So if we know that $A\vDash \mathtt{stat}s \varphi (s)$, player II chooses their club $C$ according to the strategy, by the assumption there is some $s\in C$ such that $A\vDash \varphi(s)$, we let player I choose this $s$, then player II chooses their corresponding stationary $S \subseteq \mathcal{P}_{\omega_1}(B)$. We want to show that for any $t\in S$, $B\vDash \varphi(t)$, so we let Player I choose any $t\in S$. Since II is using their winning strategy, they can win the shorter game with the first move $(s,t)$, so the induction hypothesis says that $(s,t)$ can be extended to a partial isomorphism, so that in particular also $B\vDash \varphi(t)$.
![[Kaufmann - SOME RESULTS IN STATIONARY LOGIC#^3b15e5]]
## Caicedo
[[Caicedo - On extensions of L_ωω(Q₁)]] - Not relevant
[[Caicedo - Back-and-Forth Systems for Arbitrary Quantifiers]]
[[Caicedo - A back-and-forth characterization of elementary equivalence in stationary logic]] (not available, not published?)
Maximality and interpolation in abstract logics, Ph.D. dissertation, University of Maryland
## Makowsky
[[Makowsky - A note on stationary logic]]
>[!quote]
>A back and forth criterion for elementary equivalence for $\mathrm{L}(\mathrm{aa})$ and $\mathrm{L}_{\infty\omega_1}(\mathrm{aa})$ is given.
[[Makowsky - Quantifying Over Countable Sets_ Positive vs Stationary Logic]]
[[Makowsky - Elementary equivalence and definability in stationary logic]] (not available, not published)
The game is presented in [[Makowsky, Shelah - The theorems of Beth and Craig in abstract model theory II. Compact logics#2. Some Ehrenfeucht Games]].
## Seese and Weese?
[[Seese - Stationary logic and ordinals]]
[[Seese, Weese - L(Aa)‐Elementary Types of Well‐Orderings]]
>[!note] Remark
>They might have an independent formulation in unpublished notes entiteled [[Seese, Weese, Ehrenfeucht's game for stationary logic]] (1977).
>In the above papers they use [[Kaufmann - SOME RESULTS IN STATIONARY LOGIC|Kaufmann's results]] on back-and-forth systems for *determined* structures.
# Generalization
$\delta$ is an uncountable cardinal such that $\delta=\delta^{<\delta}$, we consider the quantifier $\mathtt{aa}_\delta$ with the following meaning: If $\boldsymbol{a}$ is a finite sequence of elements of $M$ and $t$ is a finite sequence of subsets of $M$ of cardinality
lt;\delta$, then we define
$
\mathcal{M} \models \operatorname{aas} \varphi(s, \boldsymbol{t}, \boldsymbol{a})
$
if and only if $\left\{s \in \mathcal{P}_\delta(M): \mathcal{M} \models \varphi(s, \boldsymbol{t}, \boldsymbol{a})\right\}$ contains a club of subsets of $M$ of cardinality lt;\delta$.
It is proved in [[Alan H. Mekler and Saharon Shelah. Stationary logic and its friends. II.]] that a sentence of $\mathcal{L}(\mathtt{aa})$ has a model if and only if it has a model when $\mathtt{aa}$ is interpreted as a $\mathtt{aa}_\delta$.
# Variants
>[!info] Definition
> Let $(M,R)$ be a linear order, and $\mathcal{D}$ the set of all proper initial segments of $M$ under $R$.
> $\mathcal{J} \subseteq \mathcal{D}$ is called
> - unbounded in $\mathcal{D}$ if $\forall x \in \mathcal{D} \exists y \in \mathcal{J}(x \subseteq y)$
> - $\sigma$-closed in $\mathcal{D}$ if $x_0 \subseteq x_1 \subseteq \ldots$ in $\mathcal{J}$, then $\bigcup_n x_n \in \mathcal{J}$
>
> $\mathcal{I} \subseteq \mathcal{D}$ is called stationary in $\mathcal{D}$ if for every unbounded $\sigma$-closed $\mathcal{J}$, $\mathcal{J} \cap \mathcal{I} \neq \emptyset$.
>[!info] Definition
> $\mathcal{M} \models Q^{S t} x y z \varphi(x, \boldsymbol{a}) \psi(y, z, \boldsymbol{a})$ if and only if, when setting $M_0=\{b \in M: \mathcal{M} \models \varphi(b, \boldsymbol{a})\}$ and $R_0=\{(b, c) \in M: \mathcal{M} \models \psi(b, c, \boldsymbol{a})\}$,
> $\left(M_0, R_0\right)$ is an $\aleph_1$-like linear order and the set $\mathcal{I}$ of initial segments of $\left(M_0, R_0\right)$ with an $R_{0}$ supremum in $M_0$ is stationary in $\mathcal{D}$.
^st
The logic $\mathcal{L}\left(Q^{S t}\right)$, a sublogic of $\mathcal{L}(\mathrm{aa})$, is recursively axiomatizable and $\aleph_0$-compact
>[!info] Definition
> $\mathcal{M} \models Q^{S t, 0} x y z \varphi(x, y, \boldsymbol{a}) \psi(z, \boldsymbol{a})$ if and only if $R_0=\{(b, c) \in$ $M: \mathcal{M} \models \varphi(b, c, \boldsymbol{a})\}$ is a linear order of cofinality $\omega_1$ on its field and the set of initial segments with supremum in $S_0=\{b \in M: \mathcal{M} \models \psi(b, a)\}$ is stationary.
^st0
# References
[[Barwise, Feferman - Model-theoretic logics]] sections II.3 and IV.4
[[Kennedy, Magidor, Väänänen - Inner models from extended logics Part 2]]