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.

Title first order logic FirstOrderLogic 2013-03-22 13:00:06 2013-03-22 13:00:06 Henry (455) Henry (455) 7 Henry (455) Definition msc 03B10 classical first order logic FO