first order logic

A logic is first order if it has exactly one type. Usually the term refers specifically to the logic with connectives $\mathrm{\neg }$, $\vee$, $\wedge$, $\to$, and $\leftrightarrow$ and the quantifiers $\forall$ and $\exists$, all given the usual semantics:

• $\mathrm{\neg }\varphi$ is true iff $\varphi$ is not true

• $\varphi \vee \psi$ is true if either $\varphi$ is true or $\psi$ is true

• $\forall x\varphi (x)$ is true iff ${\varphi }_x^t$ is true for every object $t$ (where ${\varphi }_x^t$ is the result of replacing every unbound occurrence of $x$ in $\varphi$ with $t$)

• $\varphi \wedge \psi$ is the same as $\mathrm{\neg }(\mathrm{\neg }\varphi \vee \mathrm{\neg }\psi )$

• $\varphi \to \psi$ is the same as $(\mathrm{\neg }\varphi )\vee \psi$

• $\varphi \leftrightarrow \psi$ is the same as $(\varphi \to \psi )\wedge (\psi \to \varphi )$

• $\exists x\varphi (x)$ is the same as $\mathrm{\neg }\forall x\mathrm{\neg }\varphi (x)$

However languages with slightly different quantifiers and connectives are sometimes still called first order as long as there is only one type.