THE LOGIC NOTES

Free logic Glossary

Definition

Free logic is a variant of first order logic which allows for the fact that function symbols, including names, may be partial—that is, may have no value (for some or all arguments) on an interpretation.

Comments

There are several different free logics. The one presented in these notes not only allows for partial functions, but also allows the interpretation based on the empty domain. Its quantifiers range over the domain of any interpretation, so it is provable in it that everything exists, even if Lord Voldemort does not, because he isn't anything (he doesn't exist). There is a special predicate EST for stating that things exist.

The natural deduction rules for introducing and eliminating quantifiers in free logic are a little different from the standard ones. Existential introduction (SOMEI) and universal elimination (ALLE) require an extra premise stating that the object involved exists. Conversely, universal introduction (ALLI) and existential elimination (SOMEE) discharge the assumption EST(m) where m is the name being generalised upon.

Examples

  1. Free logic proof:

    SP {ALLx(Fx IMP Gx), SOMEx(Fx AND Hx) ⊢ SOMEx(Gx AND Hx)} PL {1} {1} {ALLx(Fx IMP Gx)} {A} PL {2} {2} {SOMEx(Fx AND Hx)} {A} PL {3} {3} {Fa AND Ha} {A} PL {4} {4} {EST(a)} {A} PL {3} {5} {Fa} {3 ANDE} PL {1,4} {6} {Fa IMP Ga} {1, 4 ALLEf} PL {1,3,4} {7} {Ga} {5, 6 IMPE} PL {3} {8} {Ha} {3 ANDE} PL {1,3,4} {9} {Ga AND Ha} {7, 8 ANDI} PL {1,3,4} {10} {SOMEx(Gx AND Hx)} {4, 9 SOMEIf} PL {1,2} {11} {SOMEx(Gx AND Hx)} {2, 10 [3,4] SOMEEf} EP
  2. Free logic proof that everything exists:

    SP{⊢ ALLx EST(x)} PL {1} {1} {EST(a)} {A} PL { } {2} {ALLx EST(x)} {1 [1] ALLIf} EP

Links