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.

Title	first order logic
Canonical name	FirstOrderLogic
Date of creation	2013-03-22 13:00:06
Last modified on	2013-03-22 13:00:06
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	7
Author	Henry (455)
Entry type	Definition
Classification	msc 03B10
Synonym	classical first order logic
Synonym	FO