 An axiomatization of inclusive quantificational logic should weaken the axiom of universal instantiation in order to prevent the derivation of theorems such as \((\forall xPx \rightarrow \exists x Px)\) or \(\exists x(Px \rightarrow Px)\). One option independently explored by Kripke (1963) and Lambert (1963) is to replace (\(\forall 1\)) with a closed axiom schema: