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  20130322 13:00:06 
Last modified on  20130322 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 