Intuitionistic first-order logic
= Intuitionistic first-order logic
{title2=$\vdash_{\mathrm{IL}}$}
<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>.