Tarski Semantics

Idea

Tarski semantics defines truth and logical consequence for formal languages through the satisfaction relation between a structure and a formula. It underpins classical model theory.

Definition

Tarski semantics provides a recursive definition of the satisfaction relation for a first-order language $\mathcal{L}$ within a structure $\mathcal{M}$. A structure $\mathcal{M}=⟨D,I⟩$ consists of a non-empty domain $D$ and an interpretation function $I$.

Satisfaction Relation

Let $s:V\to D$ be a variable assignment. The relation $\mathcal{M},s\models \varphi$ is defined inductively:

1. Atomic: $\mathcal{M},s\models P(\vec{t})$ iff $I(P)({\vec{t}}^{\mathcal{M},s})$ holds.
2. Connectives: $\mathcal{M},s\models \neg \varphi$ iff it is not the case that $\mathcal{M},s\models \varphi$.
3. Quantifiers: $\mathcal{M},s\models \forall x.\varphi$ iff for all $d\in D$, $\mathcal{M},s[x\mapsto d]\models \varphi$.

Truth and Validity

• Truth: $\varphi$ is true in $\mathcal{M}$ (denoted $\mathcal{M}\models \varphi$) if satisfied by every assignment $s$.
• Validity: $\varphi$ is valid ($\models \varphi$) if true in every structure $\mathcal{M}$.
• Consequence: $\Gamma \models \varphi$ if every model of $\Gamma$ is a model of $\varphi$.

Type Theory Context

Tarski semantics assumes a classical metalogic (LEM). This contrasts with Heyting Algebra semantics for intuitionistic first-order logic or Kripke Semantics. In HoTT, semantic approaches often involve $\infty$-topoi¹, though the Univalence Principle allows treating isomorphic structures as identical, refining the model-theoretic view.

Footnotes

1. Infinity-Topos ↩