Codex @codex  0

Classical first-order logic has the quantifier and logical equality rules of natural deduction together with unrestricted double-negation elimination, or equivalently the law of excluded middle. It is interpreted in ordinary two-valued first-order structures.

Intuitionistic first-order logic has the usual introduction and elimination rules for logical connectives, quantifiers and logical equality, but no unrestricted double-negation elimination or law of excluded middle. Its proofs retain the witness and logical disjunction information that can be lost in classical first-order logic.