[FOM] Reply to Avron and Friedman on how to prove inclusion of the empty set, without using EFQ

[Tennant, Neil]

We take the set term-forming operator as a primitive. So {x|Fx} is a well-formed singular term.
So we have to work in a free logic, designed to deal with non-denoting singular terms.
We express "x is a member of y" by "x in y" in ascii.
Ex is our existential quantifier in ascii.
Ax is our universal quantifier in ascii.
We abbreviate Ex(x=t) to E!t.
The absurdity symbol is #. It occurs only as a punctuation marker in proofs, never as a subformula of any formula.

The Axiom of Existence of Empty Set is the zero-premise rule

           ________
           E!{x|~x=x}

The Rule of Reflexivity of Identity in free logic is

           E!t
           ___
           t=t

Core Logic has as a primitive rule that one can prove a conditional by refuting its antecedent. This forms part of the rule of ->Introduction. Note the absence of any application of EFQ:

         ____(i)
           P
           :
           #
        _____(i)
         P->Q

Remember A is our ascii universal quantifier. The rule of A-Introduction in free logic allows one to discharge the parametric assumption "a is a thing", if one has used it:

         ___(i)
         E!a
           :
         Fa
       ____(i)
       AxFx

One of the elimination rules for the set-abstraction operator is the following:

                              ___(i)
                               Fu
                                 :
     t={x|Fx}   u in t    G
    __________________(i)
                     G

Assume that the only things we are talking about are sets.
That the empty set {x|~x=x} is a subset of any set  z can be expressed as

           AzAy(y in {x|~x=x} -> y in z)

We prove this formally in Core Logic as follows, using only the foregoing axioms and rules:

                                                                                     ___(1)
                                                                                      E!a
    _________                                             _____(3)       ____
     E!{x|~x=x}                                           ~a=a             a=a
_________________     ____________(2)    _______________
{x|~x=x}={x|~x=x}      a in {x|~x=x}                     #
______________________________________________(3)
                                            #
                             _____________________(2)
                              a in {x|~x=x} -> a in b
                         ________________________(1)
                          Ay(y in {x|~x=x} -> y in b)
                        _________________________
                        AzAy(y in {x|~x=x} -> y in z)


[I apologize if this proof suffers from any unintended horizontal deformations; spaces in ascii are rendered with different widths in different viewers.]

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150901/e8bde2aa/attachment-0001.html>