Given a Language and a -Structure , we define ” is true in ” or:

for a formula , recursively on . Crucial step is:

if and only if for some :

Theorem (Tarski)

There is no formula defining

for all formulas . In particular, if all formulas are encoded as elements of , there is no formula determining which elements of encode true formulas.