Free logic and the concept of existence (Q2541889)

Modern logic amended the traditional square of opposition by removing the existential import of general terms. In an analogous fashion, free logic removes the existential import of singular terms, amending the inference of \((Ex)Fx\) from \(Fy\) by requiring the additional premise \(E!y\) (to be read as ``\(y\) exists''). After explaining this motivation in some detail, the author gives an axiomatic formulation of free logic, provably equivalent to one previously shown consistent and complete. The new axioms include the usual axiom schemes for sentential logic and identity theory, rules of detachment and generalization (Hilbert-Ackermann form), and in addition the axiom schemes \[(Ex)Fx \supset (Ex) (E!x\cdot Fx)\quad\text{and}\quad Fy \supset \cdot E!y \supset (Ex)Fx. \] It is then proved that for a variable \(y\) distinct from \(x\), \((E!x)\equiv (Ex)(x=y)\) is a theorem, thus justifying the definitional elimination of the existence predicate. Several philosophical discussions of existence are evaluated with reference to free logic.