first order logic

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

• $\neg\phi$ is true iff $\phi$ is not true
• $\phi\vee\psi$ is true if either $\phi$ is true or $\psi$ is true
• $\forall x\phi(x)$ is true iff $\phi^t_x$ is true for every object $t$ (where $\phi^t_x$ is the result of replacing every unbound occurrence of $x$ in $\phi$ with $t$ )
• $\phi\wedge\psi$ is the same as $\neg(\neg\phi\vee\neg\psi)$
• $\phi\rightarrow\psi$ is the same as $(\neg\phi)\vee\psi$
• $\phi\leftrightarrow\psi$ is the same as $(\phi\rightarrow\psi)\wedge(\psi\rightarrow\phi)$
• $\exists x\phi(x)$ is the same as $\neg\forall x\neg\phi(x)$

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