Formal Proofs
in Axiomatic Set Theory

A Tutorial for the SetTheory.m Package

by Matthew P. Szudzik

1 Introduction

The SetTheory.m package checks formal proofs in Zermelo-Fraenkel set theory with first-order logic, and provides some facilities to aid in the writing of such proofs.  The package can easily be modified to accommodate different sets of axioms.  Before beginning, please make sure that a copy of SetTheory.m is in one of the directories which is listed by Mathematica's $Path variable.

$Path

This tutorial assumes that the user knows how to use Mathematica, and is familiar with axiomatic set theory and first-order logic.  The notation and terminology specific to the SetTheory.m package is derived from that which is used in Herbert B. Enderton's textbooks, Elements of Set Theory and A Mathematical Introduction to Logic.  Both texts, together with this tutorial, provide the background material which is necessary for a user familiar with Mathematica to use the SetTheory.m package.

<< SetTheory.m

2 Well-Formed Formulas

Formulas in set theory are traditionally written with a collection of symbols including the alphabetic characters, the space character, "∀", "&", "⌀", "=", "↔", "→", "⋂", "∈", "¬", "or", "𝒫", "{", ",", "}", "⊆", "⋃", "(", and ")".  A formula is said to be well-formed if and only if its symbols are combined in a manner which conforms to certain rules of  grammar.  The SetTheory.m package requires that formulas be entered in a specific manner to guarantee that they are well-formed.  Let α and β be any pair of well-formed formulas, let s and t be any pair of terms, and let x be any variable.  The table below describes how well-formed formulas and parts of well-formed formulas must be entered.

Please note that the SET command is not restricted to two arguments; it will accept one or more arguments.  All of the other commands are restricted to the number of arguments shown.  The variables must be entered as strings, with any two strings representing the same variable if and only if the strings are identical.  For example, the well-formed formula ∀x ⌀⊆x is entered as is shown below.

ALL["x",  SUBSET[EMPTYSET[],  "x"]]

If a not-well-formed formula is entered, then an error message is generated and the evaluation is aborted.

ALL[x,  SUBSET[EMPTYSET[],  x]]

The formula in this example is not well-formed because x is a symbol, not a string, and hence does not represent a term or variable.

3 Axioms

In axiomatic set theory with first-order logic, each formula which appears in a proof is justified by either a rule of inference or an axiom.  Following Enderton's A Mathematical Introduction to Logic, the only rule of inference which is recognized by the SetTheory.m package is modus ponens.  This is discussed in greater detail in section 4, below.  The SetTheory.m package recognizes twenty-two axioms: six logical axioms, six definitions, and ten set-theoretic axioms.  Note that the word "axiom" is used in a more general sense than that used by Enderton.  Here, definitions are treated as axioms, and not as separate entities.  Each axiom has a name which is stored as a string in the list $AxiomList.

$AxiomList  //  InputForm

Logical Axioms

The axioms of first-order logic are described in section 2.4 of Enderton's A Mathematical Introduction to Logic.  The six logical axioms recognized by the SetTheory.m package are identical to Enderton's axioms, except that Enderton restricts well-formed formulas to two logical connectives (→ and ¬), while the package allows a well-formed formula to contain all of the traditional connectives (&, ↔, →, ¬, and or).

The concept of a generalization of a formula is common to each of the six logical axioms.  If α is a formula, then α is a generalization of itself, and any formula of the form ∀x(β) is a generalization of α, where x is any variable and β is a generalization of α.  For definitions of other terminology which appear in the logical axioms, such as atomic, free, substitutable, and tautology, see Enderton's A Mathematical Introduction to Logic.

Axiom 1

Logical axiom 1 is identified by the string "Ax. 1".  A well-formed formula is an instance of axiom 1 if and only if it is a generalization of a tautology.  For example, ∀u(u⊆x → u⊆x) is an instance of axiom 1.

Axiom 2

Logical axiom 2 is identified by the string "Ax. 2".  A well-formed formula is an instance of axiom 2 if and only if it is a generalization of a formula of the form ∀x(α) → β, where x is any variable, α is any well-formed formula, and β is the formula obtained by substituting some term t for x in α, provided that t is substitutable for x in α.  For example, ∀r r∈s → ⋃s∈s is an instance of axiom 2.

Axiom 3

Logical axiom 3 is identified by the string "Ax. 3".  A well-formed formula is an instance of axiom 3 if and only if it is a generalization of a formula of the form ∀x(α -> β) -> (∀x(α) -> ∀x(β)), where x is any variable and α and β are any pair of well-formed formulas.  For example, ∀x(x=⌀ -> ⌀=x) -> (∀x x=⌀ -> ∀x ⌀=x) is an instance of axiom 3.

Axiom 4

Logical axiom 4 is identified by the string "Ax. 4".  A well-formed formula is an instance of axiom 4 if and only if it is a generalization of a formula of the form α -> ∀x(α), where x is any variable and α is any well-formed formula in which x does not occur free.  For example, ⌀∈𝒫⌀ -> ∀z ⌀∈𝒫⌀ is an instance of axiom 4.

Axiom 5

Logical axiom 5 is identified by the string "Ax. 5".  A well-formed formula is an instance of axiom 5 if and only if it is a generalization of a formula of the form x=x, where x is any variable.  For example, ∀x ∀y z=z is an instance of axiom 5.

Axiom 6

Logical axiom 6 is identified by the string "Ax. 6".  A well-formed formula is an instance of axiom 6 if and only if it is a generalization of a formula of the form x=y -> (α -> β), where x and y are any pair of variables, α is any atomic formula, and β is a formula obtained by replacing x in zero or more places (but not necessarily in all places) with y in the formula α.  For example, a=b -> (a∈b -> b∈b) is an instance of axiom 6.

Definitions

In Elements of Set Theory, Enderton treats the defined symbols of set theory, such as "⌀", "⋂", "𝒫", "{", ",", "}", "⊆", and "⋃", differently than the SetTheory.m package does.  Enderton has a fairly restrictive definition of a well-formed formula which forbids the use of these symbols within formal proofs.  The SetTheory.m package allows the defined symbols to appear in formal proofs, and hence requires that their definitions appear as "axioms".  It also allows some freedom in the choice of variables, so the definitions do not have to be entered exactly as they are shown below.

Empty Set Definition

The empty set definition is identified by the string "Empty Set Def.", and is given by the formula ∀x(x=⌀ ↔ ∀a ¬a∈x).

Intersection Definition

The intersection definition is identified by the string "Intersection Def.", and is given by the formula ∀x ∀y(x=⋂y ↔ ∀a(a∈x ↔ ∀b(b∈y -> a∈b))).  Note that a logical consequence of this definition, together with the empty set definition and subset axiom, is that ⋂⌀ does not exist.

Power Set Definition

The power set definition is identified by the string "Power Set Def.", and is given by the formula ∀x ∀y(x=𝒫y ↔ ∀a(a∈x ↔ a⊆y)).

Set Definition

The set definition is identified by the string "Set Def.", and is given by any formula of the form "\[ForAll]x \[ForAll]\!\(y\_1\) \[ForAll]\!\(y\_2\) \[Ellipsis] \
\[ForAll]\!\(y\_n\)(x={\!\(y\_1\), \!\(y\_2\), \[Ellipsis], \!\(y\_n\)} \
\[LeftRightArrow] \[ForAll]a(a\[Element]x \[LeftRightArrow] (a=\!\(y\_1\) or \
a=\!\(y\_2\) or \[Ellipsis] or a=\!\(y\_n\))))".

Subset Definition

The subset definition is identified by the string "Subset Def.", and is given by the formula ∀x ∀y(x⊆y ↔ ∀a(a∈x -> a∈y)).

Union Definition

The union definition is identified by the string "Union Def.", and is given by the formula ∀x ∀y(x=⋃y ↔ ∀a(a∈x ↔ ¬∀b ¬(b∈y & a∈b))).

Set-Theoretic Axioms

Enderton describes the ten Zermelo-Fraenkel set-theoretic axioms in Elements of Set Theory.  These axioms are reformulated in the SetTheory.m package to take advantage of the defined symbols.  The package allows some freedom in the choice of variables, so the set-theoretic axioms do not have to be entered exactly as they are shown below.

Choice Axiom

The choice axiom is identified by the string "Choice Ax.", and is given by the formula ∀x((∀a(a∈x -> ¬a=⌀) & ∀a ∀b((a∈x & b∈x & ¬a=b) -> ⋂{a, b}=⌀)) -> ¬∀s ¬∀a(a∈x -> ¬∀b ¬⋂{s, a}={b})).

Empty Set Axiom

The empty set axiom is identified by the string "Empty Set Ax.", and is given by the formula ¬∀s ¬s=⌀.

Extensionality Axiom

The extensionality axiom is identified by the string "Extensionality Ax.", and is given by the formula ∀x ∀y(∀a(a∈x ↔ a∈y) -> x=y).

Infinity Axiom

The infinity axiom is identified by the string "Infinity Ax.", and is given by the formula ¬∀s ¬(⌀∈s & ∀a(a∈s -> {a}∈s)).

Pairing Axiom

The pairing axiom is identified by the string "Pairing Ax.", and is given by the formula ∀x ∀y ¬∀s ¬s={x, y}.

Power Set Axiom

The power set axiom is identified by the string "Power Set Ax.", and is given by the formula ∀x ¬∀s ¬s=𝒫x.

Regularity Axiom

The regularity axiom is identified by the string "Regularity Ax.", and is given by the formula ∀x(¬x=⌀ -> ¬∀s ¬(s∈x & ⋂{s, x}=⌀)).

Replacement Axiom

The replacement axiom is identified by the string "Replacement Ax.", and is given by any generalization of a formula of the form ∀x(∀a(a∈x -> ∀b ∀c((ϕ(a, b) & ϕ(a, c)) -> b=c)) -> ¬∀s ¬∀d(d∈s ↔ ¬∀e ¬(e∈x & ϕ(e, d)))).  Let ϕ(x, y) be a well-formed formula in which a, b, c, d, and e do not occur free, and for which a and e are substitutable for x, and b, c, and d are substitutable for y.  Let ϕ(v, w), for any pair of variables v and w, be obtained by substituting v for x and w for y in ϕ(x, y).  The variable s must not occur free in ϕ(e, d), unless the variables s and e are the same.

Subset Axiom

The subset axiom is identified by the string "Subset Ax.", and is given by any generalization of a formula of the form ∀x ¬∀s ¬∀a(a∈s ↔ (a∈x & ϕ)), where ϕ is any well-formed formula in which s does not occur free.

Union Axiom

The union axiom is identified by the string "Union Ax.", and is given by the formula ∀x ¬∀s ¬s=⋃x.

4 Proofs

A formal proof in axiomatic set theory with first-order logic consists of a sequence of well-formed formulas, each justified by an axiom or modus ponens.  The SetTheory.m package requires that a proof be entered as a list of a certain form which is referred to here as a proof-list.  A valid proof-list is a list of lines,each of the form {num, wff, jst}, where the line number num is a whole number (i.e. a positive integer), wff is a well-formed formula, and jst is an expression which is intended to justify the well-formed formula wff.  No two lines in a valid proof-list should have the same line number.  The expression jst must be a Mathematica expression whose head is either Axiom, ModusPonens, Algorithm, or Given.  Any line numbers which are referred to by a justification (ModusPonens or Algorithm) must be less than num.  The following is a proof-list corresponding to a proof that ⌀∈x -> ¬∀x ¬⌀∈x.

\(simpleproof\  = 
	{
		{1, \ 
			IMPLIES[
            ALL["x", \ NOT[MEMBER[EMPTYSET[], "x"]]], 
            NOT[MEMBER[
                EMPTYSET[], "x"]]], 
			\ Axiom["Ax. 2"]
		}, 
		{2, 
			IMPLIES[
            IMPLIES[ALL["x", \ NOT[MEMBER[EMPTYSET[], "x"]]], 
              NOT[MEMBER[EMPTYSET[], "x"]]], 
            IMPLIES[MEMBER[EMPTYSET[], \ "x"], 
              NOT[ALL["x", \ 
                  NOT[MEMBER[
                      EMPTYSET[], \ "x"]]]]]], 
			Axiom["Ax. 1"]
		}, 
		{3, 
			IMPLIES[MEMBER[EMPTYSET[], \ "x"], 
            NOT[ALL["x", \ 
                NOT[MEMBER[EMPTYSET[], \ "x"]]]]], 
			ModusPonens[
            1, \ 2]
		}
	}\)

Given a proof-list prf, the expression CheckProof[prf] can be used to check the corresponding proof.  If the proof is valid, then CheckProof[prf] displays the proof, followed by "Q.E.D." to signify that its validity has been demonstrated.

CheckProof[ simpleproof]

For a proof to be valid, the well-formed formula on each line of the proof must be accompanied by the proper justification.  If a well-formed formula wff is justified by Axiom[axm], then wff must be an instance of the axiom named by the string axm.  If a well-formed formula wff is justified by ModusPonens[x, y], then well-formed formulas of the form α and IMPLIES[α, wff], where α is any well-formed formula, must appear in the proof on the lines with numbers x and y.  The order of the arguments x and y is unimportant—if a formula can be justified by ModusPonens[x, y], then it can also be justified by ModusPonens[y, x].  Besides Axiom and ModusPonens, it is also possible for well-formed formulas to be justified by expressions with the heads Algorithm and Given, but neither of these justifications is essential in a valid proof, so a discussion of them is postponed until section 5, below.

If CheckProof can demonstrate that the proof-list prf corresponds to an invalid proof, then CheckProof[prf] produces a message which identifies one of the lines as invalid, and then displays the valid lines up to that invalid one.  Note that the proof which is thus displayed is not followed by "Q.E.D." because the proof is invalid.

\(invalidproof\  = 
	{
		{1, \ 
			IMPLIES[
            ALL["x", \ NOT[MEMBER[EMPTYSET[], "x"]]], 
            NOT[MEMBER[
                EMPTYSET[], "x"]]], 
			\ Axiom["Ax. 2"]
		}, 
		{2, 
			IMPLIES[
            IMPLIES[ALL["x", \ NOT[MEMBER[EMPTYSET[], "x"]]], 
              NOT[MEMBER[EMPTYSET[], "x"]]], 
            IMPLIES[MEMBER[EMPTYSET[], \ "x"], 
              NOT[ALL["x", 
                  NOT[MEMBER[
                      EMPTYSET[], \ "x"]]]]]], 
			Axiom["Ax. 1"]
		}, 
		{3, 
			IMPLIES[MEMBER[EMPTYSET[], \ "x"], 
            NOT[ALL["x", 
                NOT[MEMBER[
                    EMPTYSET[], \ "x"]]]]], 
			Axiom["Empty Set Ax."]
		}
	}\)

CheckProof[ invalidproof]

Sometimes it is preferable for CheckProof[prf] to output True if the proof is valid and False if it discovers an invalid line, rather than displaying the valid lines of the proof.  CheckProof[prf, DisplayProof->False] provides this alternative form of output.

CheckProof[simpleproof,  DisplayProof  ->  False]

CheckProof[invalidproof,  DisplayProof  ->  False]

When a proof is displayed by CheckProof, it is generally easier to read than the corresponding proof-list.  While writing or correcting a proof, you may wish to display the proof without checking it.  DisplayProof[prf] will display the proof which corresponds to the proof-list prf, but will not check the proof.  Of course, the proof which is thus displayed is not followed by "Q.E.D." because the validity of the proof is not guaranteed.

DisplayProof[invalidproof]

To assist in entering proof-lists, the SetTheory.m package provides the AddLine function.  The AddLine function can be entered with the infix operator **.  sym ** num ** wff ** jst, appends the line {num, wff, jst} to the proof-list which is named by the symbol sym.  It is important that sym be a symbol which stands for a proof-list and not a proof-list.

\({}\  ** \ 
1\  ** \ 

      ALL["x", 
        IMPLIES[IMPLIES[MEMBER["x", "a"], MEMBER["x", "b"]], 
          IMPLIES[NOT[MEMBER["x", \ "b"]], 
            NOT[MEMBER["x", \ "a"]]]]]\  ** \ 

      Axiom["Ax. 1"]\)

example  =  {}

\(example\  ** \ 
1\  ** \ 

      ALL["x", 
        IMPLIES[IMPLIES[MEMBER["x", "a"], MEMBER["x", "b"]], 
          IMPLIES[NOT[MEMBER["x", \ "b"]], 
            NOT[MEMBER["x", \ "a"]]]]]\  ** \ 

      Axiom["Ax. 1"]\)

DisplayProof[ example]

Once a symbol has been called by AddLine, that symbol is stored as ProofName[].

ProofName[]

If sym is the symbol named by ProofName[], then entering the abbreviated input  num ** wff ** jst is equivalent to entering sym ** num ** wff ** jst.

\(2\  ** 

      IMPLIES[ALL["x", 
          IMPLIES[IMPLIES[MEMBER["x", "a"], 
              MEMBER["x", "b"]], 
            IMPLIES[NOT[MEMBER["x", \ "b"]], 
              NOT[MEMBER["x", \ "a"]]]]], 
        IMPLIES[ALL["x", 
            IMPLIES[MEMBER["x", "a"], \ MEMBER["x", "b"]]], 
          ALL["x", 
            IMPLIES[NOT[MEMBER["x", \ "b"]], 
              NOT[MEMBER["x", \ "a"]]]]]]\  ** 

      Axiom["Ax. 3"]\)

DisplayProof[ example]

Occasionally, you might forget the number of the last line in a proof-list.  The expression LastLine[prf] gives the greatest line number in the proof-list prf.

LastLine[example]

If you intend to add a line numbered LastLine[prf] + 1 to the proof-list prf which is named by ProofName[], then entering wff ** jst is equivalent to entering num ** wff ** jst, where num is LastLine[prf] + 1.

\(IMPLIES[
        ALL["x", 
          IMPLIES[IMPLIES[MEMBER["x", "a"], 
              MEMBER["x", "b"]], 
            IMPLIES[NOT[MEMBER["x", \ "b"]], 
              NOT[MEMBER["x", \ "a"]]]]], 
        IMPLIES[ALL["x", 
            IMPLIES[MEMBER["x", "a"], \ MEMBER["x", "b"]]], 
          ALL["x", 
            IMPLIES[NOT[MEMBER["x", \ "b"]], 
              NOT[MEMBER["x", \ "a"]]]]]]\  ** 

      Axiom["Ax. 3"]\)

DisplayProof[ example]

Entering a proof with a series of expressions of the form wff ** jst can be much more convenient than explicitly typing the entire proof-list.  Nevertheless, typing the well-formed formulas can still be quite cumbersome.  While entering a proof, it is helpful to keep in mind the relationships between the various formulas, and to take advantage of those relationships by using Mathematica's commands to transform previously entered formulas into new formulas.

\(\(Part[example, \ \(-1\), \ 2, \ 2]\  ** 

        ModusPonens[1, \ 3];\)\)

\(\(IMPLIES[Part[example, \ \(-1\), \ 2, \ 2], 
          IMPLIES[ALL["x", \ NOT[MEMBER["x", \ "b"]]], 
            ALL["x", \ NOT[MEMBER["x", \ "a"]]]]]\  ** 

        Axiom["Ax. 3"];\)\)

\(\(IMPLIES[Part[example, \ \(-2\), \ 2], 
          IMPLIES[Part[example, \ \(-1\), \ 2], 
            IMPLIES[Part[example, \ \(-2\), \ 2, \ 1], 
              IMPLIES[NOT[ALL["x", \ NOT[MEMBER["x", \ "a"]]]], 
                NOT[ALL["x", NOT[MEMBER["x", \ "b"]]]]]]]]\  ** 

        Axiom["Ax. 1"];\)\)

\(\(Part[example, \ \(-1\), \ 2, \ 2]\  ** 

        ModusPonens[4, \ 6];\)\)

\(\(Part[example, \ \(-1\), \ 2, \ 2]\  ** 

        ModusPonens[5, \ 7];\)\)

CheckProof[ example]

Note that an error was made while entering the above proof.  The formula in line 2 was entered twice, and appears again in line 3.  Although this error does not affect the validity of the proof, it makes the proof longer than is necessary.  The expression RemoveLine[sym, num] removes the line numbered num from the proof-list which is named by the symbol sym.  If sym is the symbol named by ProofName[], then RemoveLine[num] may be entered place of RemoveLine[sym, num].

RemoveLine[2];

CheckProof[example]

But with line 2 removed, the proof jumps from line 1 to line 3.  The expression RenumberProof[prf, x, Δx] outputs a proof-list whose proof is equivalent to that of the proof-list prf, but whose first line is numbered x and whose consecutive lines have numbers which increase by Δx.

example  =  RenumberProof[example,  1,  1];

CheckProof[example]

5 Algorithms

Formal proofs have the advantage of being entirely explicit, allowing them to be checked by a purely mechanical procedure.  Unfortunately, formal proofs tend to be prohibitively long for all but the most simple propositions.  One solution to this problem is to allow the use of algorithms.  For example, given any formula of the form ∀x(α -> β), where x is any variable and α and β are any pair of well-formed formulas, it is possible to deduce that ∀x(α) -> ∀x(β) by invoking axiom 3 and applying modus ponens.  The algorithm distribute writes a proof of ∀x(α) -> ∀x(β) given ∀x(α -> β).

\(distribute[wff_ALL]\  := 
	
      Module[\ {dist, \ imply, \ x}, 
		imply\  = Last[wff]; 	
		If[
          Head[imply]\  =!= \ IMPLIES, 
			False, 
			
			x\  = 
            First[wff]; 
			dist\  = 
            IMPLIES[ALL[x, \ First[imply]], 
              ALL[x, \ Last[imply]]]; 
			{{1, \ wff, 
              Given[]}, 
					{2, \ IMPLIES[wff, dist], 
              Axiom["Ax. 3"]}, 
					{3, \ dist, 
              ModusPonens[1, 2]}}
		]
	]\)

Consider the special case where ∀x x∈a -> ∀x x∈b is deduced from ∀x(x∈a -> x∈b).

\(specialproof\  = \ 
	
      distribute[
        ALL["x", 
          IMPLIES[MEMBER["x", "a"], 
            MEMBER["x", "b"]]]]\)

DisplayProof[specialproof]

Note that the first line of specialproof is justified by Given[].  In the proof-list of a fully formal proof, Given[] is not a valid justification for a well-formed formula.  If it were, then it would be possible to prove any arbitrary formula simply by justifying it with Given[].

CheckProof[specialproof]

CheckProof only accepts a well-formed formula wff justified with Given[] if the option GivensList -> lst is specified, and wff is a member of the list lst.

\(CheckProof[specialproof, \ 
	
      GivensList\  -> \ {ALL["x", 
            IMPLIES[MEMBER["x", "a"], 
              MEMBER["x", "b"]]]}
]\)

Formal proofs could be much shorter if new rules of inference were adopted.  For example, it might be helpful if there were a rule of inference which allows ∀x(α) -> ∀x(β) to be concluded from ∀x(α -> β), for all variables x and well-formed formulas α and β.  The Algorithm command allows you to use just such a rule of inference in a proof, while guaranteeing that an equivalent (but possibly longer) proof could have been written without resorting to the command.  In a valid proof, if a well-formed formula wff is justified by Algorithm[f, {(Subscript[num, 1]), (Subscript[num, 2]), …, (Subscript[num, n])}], then CheckProof[f[(Subscript[wff, 1]), (Subscript[wff, 2]), …, (Subscript[wff, n])], DisplayProof -> False, GivensList -> {(Subscript[wff, 1]), (Subscript[wff, 2]), …, (Subscript[wff, n])}] must be True and f[(Subscript[wff, 1]), (Subscript[wff, 2]), …, (Subscript[wff, n])] must be a proof of wff, where (Subscript[wff, 1]), (Subscript[wff, 2]), …, (Subscript[wff, n]) are the well-formed formulas which appear on lines (Subscript[num, 1]), (Subscript[num, 2]), …, (Subscript[num, n]) in the main proof.

\(\(shortproof\  ** 
1\  ** 

        ALL["y", 
          IMPLIES[ALL["x", SUBSET["x", \ "y"]], 
            SUBSET["y", \ "y"]]]\  ** 

        Axiom["Ax. 2"];\)\)

\(\(IMPLIES[ALL["y", \ ALL["x", \ SUBSET["x", \ "y"]]], 
          ALL["y", \ SUBSET["y", \ "y"]]]\  ** 

        Algorithm[distribute, \ {1}];\)\)

CheckProof[shortproof]

The expression FullProof[prf] produces a proof-list whose corresponding proof is equivalent to that of the proof-list prf, but in which no formulas are justified with Algorithm.

CheckProof[FullProof[shortproof]]

To shorten an otherwise long proof, you will find it useful to learn to write your own algorithms.  For example, a fundamental result of Zermelo-Fraenkel set theory is that ¬¬∀u ¬∀x x∈u.  That is, in Zermelo-Fraenkel set theory there does not exist any universal set u which contains every set as an element.  Enderton outlines a proof of this fact in chapter 2 of his Elements of Set Theory, but the fully formal proof is quite long.  In addition to the distribute algorithm, the algorithms a1, a2, and generalize are useful in shortening the proof that ¬¬∀u ¬∀x x∈u.

\(a1[x_, \ a_, 
        b_]\  := 
	{
		{1, 
          ALL[x, \ IMPLIES[IMPLIES[a, b], \ IMPLIES[NOT[b], NOT[a]]]], 
          Axiom["Ax. 1"]}, 
		{2, 
          IMPLIES[ALL[x, 
              IMPLIES[IMPLIES[a, b], 
                IMPLIES[NOT[b], NOT[a]]]], 
				IMPLIES[
              ALL[x, IMPLIES[a, b]], \ ALL[x, IMPLIES[NOT[b], NOT[a]]]]], 
          Axiom["Ax. 3"]}, 
		{3, 
          IMPLIES[ALL[x, IMPLIES[a, b]], ALL[x, IMPLIES[NOT[b], NOT[a]]]], 
          ModusPonens[1, 2]}, 
		{4, 
          IMPLIES[ALL[x, IMPLIES[NOT[b], NOT[a]]], 
            IMPLIES[ALL[x, \ NOT[b]], \ ALL[x, \ NOT[a]]]], 
          Axiom["Ax. 3"]}, 
		{5, 
          IMPLIES[IMPLIES[ALL[x, IMPLIES[a, b]], 
              ALL[x, IMPLIES[NOT[b], NOT[a]]]], 
            IMPLIES[IMPLIES[ALL[x, IMPLIES[NOT[b], NOT[a]]], 
                IMPLIES[ALL[x, \ NOT[b]], \ ALL[x, \ NOT[a]]]], 
              IMPLIES[ALL[x, \ IMPLIES[a, b]], 
                IMPLIES[NOT[ALL[x, NOT[a]]], \ NOT[ALL[x, NOT[b]]]]]]], 
          Axiom["Ax. 1"]}, 
		{6, 
          IMPLIES[IMPLIES[ALL[x, IMPLIES[NOT[b], NOT[a]]], 
              IMPLIES[ALL[x, \ NOT[b]], \ ALL[x, \ NOT[a]]]], 
            IMPLIES[ALL[x, \ IMPLIES[a, b]], 
              IMPLIES[NOT[ALL[x, NOT[a]]], \ NOT[ALL[x, NOT[b]]]]]], 
          ModusPonens[3, 5]}, 
		{7, 
          IMPLIES[ALL[x, \ IMPLIES[a, b]], 
            IMPLIES[NOT[ALL[x, NOT[a]]], \ NOT[ALL[x, NOT[b]]]]], 
          ModusPonens[4, 6]}
	}\)

\(a2[x_, \ a_, 
        b_]\  := 
	{
		{1, 
          IMPLIES[ALL[x, \ IMPLIES[a, \ NOT[b]]], 
            IMPLIES[ALL[x, a], \ ALL[x, \ NOT[b]]]], 
          Axiom["Ax. 3"]}, 
		{2, \ IMPLIES[a, \ ALL[x, a]], 
          Axiom["Ax. 4"]}, 
		{3, 
          IMPLIES[IMPLIES[ALL[x, \ IMPLIES[a, \ NOT[b]]], 
              IMPLIES[ALL[x, a], \ ALL[x, \ NOT[b]]]], 
            IMPLIES[IMPLIES[a, \ ALL[x, a]], 
              IMPLIES[AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
                NOT[ALL[x, \ IMPLIES[a, \ NOT[b]]]]]]], 
          Axiom["Ax. 1"]}, 
		{4, 
          IMPLIES[IMPLIES[a, \ ALL[x, a]], 
            IMPLIES[AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
              NOT[ALL[x, \ IMPLIES[a, \ NOT[b]]]]]], 
          ModusPonens[1, \ 3]}, 
		{5, 
          IMPLIES[AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
            NOT[ALL[x, \ IMPLIES[a, \ NOT[b]]]]], 
          ModusPonens[2, \ 4]}, 
		{6, 
          ALL[x, \ IMPLIES[NOT[AND[a, b]], \ IMPLIES[a, NOT[b]]]], 
          Axiom["Ax. 1"]}, 
		{7, 
          IMPLIES[ALL[x, \ IMPLIES[NOT[AND[a, b]], \ IMPLIES[a, NOT[b]]]], 
            IMPLIES[ALL[x, \ NOT[AND[a, b]]], 
              ALL[x, \ IMPLIES[a, 
                  NOT[b]]]]], 
			Axiom["Ax. 3"]}, 
		{8, 
          IMPLIES[ALL[x, \ NOT[AND[a, b]]], ALL[x, \ IMPLIES[a, NOT[b]]]], 
          ModusPonens[6, \ 7]}, 
		{9, 
          IMPLIES[IMPLIES[AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
              NOT[ALL[x, \ IMPLIES[a, \ NOT[b]]]]], 
            IMPLIES[IMPLIES[ALL[x, \ NOT[AND[a, b]]], 
                ALL[x, \ IMPLIES[a, NOT[b]]]], 
					IMPLIES[
                AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
                NOT[ALL[x, NOT[AND[a, b]]]]]]], 
          Axiom["Ax. 1"]}, 
		{10, 
          IMPLIES[IMPLIES[ALL[x, \ NOT[AND[a, b]]], 
              ALL[x, \ IMPLIES[a, NOT[b]]]], 
					IMPLIES[
              AND[a, \ NOT[ALL[x, \ NOT[b]]]], NOT[ALL[x, NOT[AND[a, b]]]]]], 
          ModusPonens[5, 9]}, 
		{11, 
          IMPLIES[AND[a, \ NOT[ALL[x, \ NOT[b]]]], 
            NOT[ALL[x, NOT[AND[a, b]]]]], ModusPonens[8, 10]}
	}\)

\(generalize[var_, \ proof_]\  := 
	
      Module[{f, \ fullproof, \ fx, \ fy, \ genaxioms, \ genlines, 
          genproof, \ gennum, \ genwff, \ just, \ speline, \ speproof, 
          spenum, \ spewff, \ x, \ y}, 
		speproof\  = 
          FullProof[proof]; 
		gennum\  = 
          1; 
		genproof\  = \ {}; 
		genaxioms\  = \ {"Ax. 1", \ "Ax. 2", \ "Ax. 3", \ "Ax. 4", \ "Ax. 5", \ "Ax. 6", \ "Subset Ax.", \ "Replacement Ax."}; 
		While[
          speproof\  =!= \ {}, 
			speline\  = 
            First[speproof]; 
			speproof\  = 
            Rest[speproof]; 
			spenum\  = 
            Part[speline, \ 1]; 
			spewff\  = 
            Part[speline, \ 2]; 
			genwff\  = 
            ALL[var, \ spewff]; 
			just\  = 
            Part[speline, 3]; 
			Which[
				Head[just] === Axiom\  && 
              MemberQ[genaxioms, 
                First[just]], 
				genlines\  = \ {{gennum, genwff, 
                  just}}; 
				f[spenum]\  = 
              gennum; 
				gennum\  = 
              gennum\  + \ 1, 
				
				Head[just]\  === 
              Axiom, 
				genlines\  = \ {{gennum, \ spewff, 
                  just}, 
								{gennum\  + \ 1, 
                  IMPLIES[spewff, genwff], 
                  Axiom["Ax. 4"]}, 
								{gennum\  + \ 2, 
                  genwff, \ ModusPonens[gennum, \ gennum + 1]}}; 
				f[
                spenum]\  = \ gennum\  + \ 2; 
				gennum\  = 
              gennum\  + \ 3, 
				
				Head[just]\  === 
              ModusPonens, 
				x\  = \ First[just]; 
				y\  = 
              Last[just]; 
				fx\  = 
              Part[First[Cases[genproof, \ {f[x], \ _, \ _}, \ {1}]], 
                2]; 
				fy\  = 
              Part[First[Cases[genproof, \ {f[y], \ _, \ _}, \ {1}]], 
                2]; 
				Which[
					MatchQ[fy, ALL[var, \ _]]\  && 
                fx\  === \ ALL[var, 
                    IMPLIES[Last[fy], 
                      spewff]], 
					genlines\  = \ {{gennum, 
                    IMPLIES[fx, \ IMPLIES[fy, \ genwff]], 
                    Axiom["Ax. 3"]}, 
								{gennum\  + \ 1, 
                    IMPLIES[fy, \ genwff], 
                    ModusPonens[f[x], 
                      gennum]}, 
								{gennum\  + \ 2, genwff, 
                    ModusPonens[f[y], \ gennum\  + \ 1]}}; 
					f[
                
                spenum]\  = \ gennum\  + \ 2; 
					gennum\  = 
                gennum\  + \ 3, 
					
					MatchQ[fx, 
                  ALL[var, \ _]]\  && 
                fy\  === \ ALL[var, 
                    IMPLIES[Last[fx], 
                      spewff]], 
					genlines\  = \ {{gennum, 
                    IMPLIES[fy, \ IMPLIES[fx, \ genwff]], 
                    Axiom["Ax. 3"]}, 
								{gennum\  + \ 1, 
                    IMPLIES[fx, \ genwff], 
                    ModusPonens[f[y], 
                      gennum]}, 
								{gennum\  + \ 2, genwff, 
                    ModusPonens[f[x], \ gennum\  + \ 1]}}; 
					f[
                  spenum]\  = \ gennum\  + \ 2; 
					gennum\  = 
                gennum\  + 
                  3, 
					
					True, 
					genlines\  = \ {{gennum, \ genwff, \ ModusPonens[f[x], \ f[y]]}}; 
					f[
                  spenum]\  = \ gennum; 
					gennum\  = 
                gennum\  + 
                  1
				], \ 
				
				True, 
				genlines\  = \ {{gennum, \ genwff, \ just}}; 
				f[spenum]\  = 
              gennum; 
				gennum\  = 
              gennum\  + \ 1
			]; 
			genproof\  = 
            Join[genproof, \ genlines]
		]; 
		genproof
	]\)

a1[x, α, β] outputs a proof-list corresponding to a proof that ∀x(α -> β) -> (¬∀x ¬α -> ¬∀x ¬β) for any variable x and any pair of well-formed formulas α and β.  a2[x, α, β] outputs a proof-list corresponding to a proof that (α & ¬∀x ¬β) -> ¬∀x ¬(α & β) for any variable x, any well-formed formula β, and any well-formed formula α in which x does not occur free.  generalize[x, prf] outputs a proof-list corresponding to a proof that ∀x(α) for any variable x, provided that prf is a proof-list corresponding to a valid proof of α in which no special assumptions are made concerning the variable x.  See the generalization theorem described in section 2.4 of Enderton's A Mathematical Introduction to Logic for details.

\(\(universe\  = \ 
{{1, 
            ALL["u", 
              NOT[ALL["r", 
                  NOT[ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]]]]]], 
            Axiom["Subset Ax."]}, {2, 
            ALL["u", 
              IMPLIES[NOT[
                  ALL["r", 
                    NOT[ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]]]], 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]]], 
            Axiom["Ax. 1"]}, {3, 
            IMPLIES[ALL["u", 
                NOT[ALL["r", 
                    NOT[ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]]]]], 
              ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]]], 
            Algorithm[distribute, {2}]}, {4, 
            ALL["u", 
              IMPLIES[ALL["x", MEMBER["x", "u"]], 
                AND[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]]]]]]], 
            ModusPonens[1, 3]}, {5, 
            ALL["u", 
              IMPLIES[AND[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]]]]], 
                NOT[ALL["r", 
                    NOT[AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]]]]]]], 
            Algorithm[
              generalize["u", 
                  a2["r", ALL["x", MEMBER["x", "u"]], 
                    ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]]]] &, {}]}, {6, 
            ALL["u", 
              IMPLIES[IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]], 
                IMPLIES[
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      NOT[ALL["r", 
                          NOT[ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]], 
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]]], 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]]]]]], 
            Axiom["Ax. 1"]}, {7, 
            IMPLIES[ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]], 
              ALL["u", 
                IMPLIES[
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      NOT[ALL["r", 
                          NOT[ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]], 
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]]], 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]]]]]], 
            Algorithm[distribute, {6}]}, {8, 
            ALL["u", 
              IMPLIES[IMPLIES[
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]], 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]]], 
            ModusPonens[4, 7]}, {9, 
            IMPLIES[ALL["u", 
                IMPLIES[
                  AND[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]], 
              ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]]], 
            Algorithm[distribute, {8}]}, {10, 
            ALL["u", 
              IMPLIES[ALL["x", MEMBER["x", "u"]], 
                NOT[ALL["r", 
                    NOT[AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]]]]]]], 
            ModusPonens[5, 9]}, {11, 
            ALL["u", 
              ALL["r", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  MEMBER["r", "u"]]]], Axiom["Ax. 2"]}, {12, 
            ALL["u", 
              ALL["r", 
                IMPLIES[
                  ALL["a", 
                    IFF[MEMBER["a", "r"], 
                      AND[MEMBER["a", "u"], 
                        NOT[MEMBER["a", "a"]]]]], 
                  IFF[MEMBER["r", "r"], 
                    AND[MEMBER["r", "u"], 
                      NOT[MEMBER["r", "r"]]]]]]], 
            Axiom["Ax. 2"]}, {13, 
            ALL["u", 
              ALL["r", 
                IMPLIES[
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    MEMBER["r", "u"]], 
                  IMPLIES[
                    IMPLIES[
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]], 
                      IFF[MEMBER["r", "r"], 
                        AND[MEMBER["r", "u"], 
                          NOT[MEMBER["r", "r"]]]]], 
                    IMPLIES[
                      AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]], 
                      IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]]]]], 
            Axiom["Ax. 1"]}, {14, 
            ALL["u", 
              IMPLIES[ALL["r", 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    MEMBER["r", "u"]]], 
                ALL["r", 
                  IMPLIES[
                    IMPLIES[
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]], 
                      IFF[MEMBER["r", "r"], 
                        AND[MEMBER["r", "u"], 
                          NOT[MEMBER["r", "r"]]]]], 
                    IMPLIES[
                      AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]], 
                      IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]]]]], 
            Algorithm[
              generalize["u", distribute[Last[#1]]] &, {13}]}, {15, 
            IMPLIES[ALL["u", 
                ALL["r", 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    MEMBER["r", "u"]]]], 
              ALL["u", 
                ALL["r", 
                  IMPLIES[
                    IMPLIES[
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]], 
                      IFF[MEMBER["r", "r"], 
                        AND[MEMBER["r", "u"], 
                          NOT[MEMBER["r", "r"]]]]], 
                    IMPLIES[
                      AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]], 
                      IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]]]]], 
            Algorithm[distribute, {14}]}, {16, 
            ALL["u", 
              ALL["r", 
                IMPLIES[
                  IMPLIES[
                    ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]], 
                    IFF[MEMBER["r", "r"], 
                      AND[MEMBER["r", "u"], 
                        NOT[MEMBER["r", "r"]]]]], 
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]]]], 
            ModusPonens[11, 15]}, {17, 
            ALL["u", 
              IMPLIES[ALL["r", 
                  IMPLIES[
                    ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]], 
                    IFF[MEMBER["r", "r"], 
                      AND[MEMBER["r", "u"], 
                        NOT[MEMBER["r", "r"]]]]]], 
                ALL["r", 
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]]]], 
            Algorithm[
              generalize["u", distribute[Last[#1]]] &, {16}]}, {18, 
            IMPLIES[ALL["u", 
                ALL["r", 
                  IMPLIES[
                    ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]], 
                    IFF[MEMBER["r", "r"], 
                      AND[MEMBER["r", "u"], 
                        NOT[MEMBER["r", "r"]]]]]]], 
              ALL["u", 
                ALL["r", 
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]]]], 
            Algorithm[distribute, {17}]}, {19, 
            ALL["u", 
              ALL["r", 
                IMPLIES[
                  AND[ALL["x", MEMBER["x", "u"]], 
                    ALL["a", 
                      IFF[MEMBER["a", "r"], 
                        AND[MEMBER["a", "u"], 
                          NOT[MEMBER["a", "a"]]]]]], 
                  IFF[MEMBER["r", "r"], 
                    NOT[MEMBER["r", "r"]]]]]], 
            ModusPonens[12, 18]}, {20, 
            ALL["u", 
              IMPLIES[ALL["r", 
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]], 
                IMPLIES[
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]]], 
            Algorithm[
              generalize["u", 
                  a1["r", 
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]] &, {}]}, {21, 
            IMPLIES[ALL["u", 
                ALL["r", 
                  IMPLIES[
                    AND[ALL["x", MEMBER["x", "u"]], 
                      ALL["a", 
                        IFF[MEMBER["a", "r"], 
                          AND[MEMBER["a", "u"], 
                            NOT[MEMBER["a", "a"]]]]]], 
                    IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]]], 
              ALL["u", 
                IMPLIES[
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]]], 
            Algorithm[distribute, {20}]}, {22, 
            ALL["u", 
              IMPLIES[NOT[
                  ALL["r", 
                    NOT[AND[ALL["x", MEMBER["x", "u"]], 
                        ALL["a", 
                          IFF[MEMBER["a", "r"], 
                            AND[MEMBER["a", "u"], 
                              NOT[MEMBER["a", "a"]]]]]]]]], 
                NOT[ALL["r", 
                    NOT[IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]]]]], 
            ModusPonens[19, 21]}, {23, 
            ALL["u", 
              IMPLIES[IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]], 
                IMPLIES[
                  IMPLIES[
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]], 
                    NOT[ALL["r", 
                        NOT[IFF[MEMBER["r", "r"], 
                            NOT[MEMBER["r", "r"]]]]]]], 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[IFF[MEMBER["r", "r"], 
                            NOT[MEMBER["r", "r"]]]]]]]]]], 
            Axiom["Ax. 1"]}, {24, 
            IMPLIES[ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]]]], 
              ALL["u", 
                IMPLIES[
                  IMPLIES[
                    NOT[ALL["r", 
                        NOT[AND[ALL["x", MEMBER["x", "u"]], 
                            ALL["a", 
                              IFF[MEMBER["a", "r"], 
                                AND[MEMBER["a", "u"], 
                                  NOT[MEMBER["a", "a"]]]]]]]]], 
                    NOT[ALL["r", 
                        NOT[IFF[MEMBER["r", "r"], 
                            NOT[MEMBER["r", "r"]]]]]]], 
                  IMPLIES[ALL["x", MEMBER["x", "u"]], 
                    NOT[ALL["r", 
                        NOT[IFF[MEMBER["r", "r"], 
                            NOT[MEMBER["r", "r"]]]]]]]]]], 
            Algorithm[distribute, {23}]}, {25, 
            ALL["u", 
              IMPLIES[IMPLIES[
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]], 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]]], 
            ModusPonens[10, 24]}, {26, 
            IMPLIES[ALL["u", 
                IMPLIES[
                  NOT[ALL["r", 
                      NOT[AND[ALL["x", MEMBER["x", "u"]], 
                          ALL["a", 
                            IFF[MEMBER["a", "r"], 
                              AND[MEMBER["a", "u"], 
                                NOT[MEMBER["a", "a"]]]]]]]]], 
                  NOT[
                    ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]], 
              ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]]], 
            Algorithm[distribute, {25}]}, {27, 
            ALL["u", 
              IMPLIES[ALL["x", MEMBER["x", "u"]], 
                NOT[ALL["r", 
                    NOT[IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]]]]], 
            ModusPonens[22, 26]}, {28, 
            ALL["u", 
              ALL["r", 
                NOT[IFF[MEMBER["r", "r"], 
                    NOT[MEMBER["r", "r"]]]]]], 
            Axiom["Ax. 1"]}, {29, 
            ALL["u", 
              IMPLIES[IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]], 
                IMPLIES[
                  ALL["r", 
                    NOT[IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]], 
                  NOT[ALL["x", MEMBER["x", "u"]]]]]], 
            Axiom["Ax. 1"]}, {30, 
            IMPLIES[ALL["u", 
                IMPLIES[ALL["x", MEMBER["x", "u"]], 
                  NOT[ALL["r", 
                      NOT[IFF[MEMBER["r", "r"], 
                          NOT[MEMBER["r", "r"]]]]]]]], 
              ALL["u", 
                IMPLIES[
                  ALL["r", 
                    NOT[IFF[MEMBER["r", "r"], 
                        NOT[MEMBER["r", "r"]]]]], 
                  NOT[ALL["x", MEMBER["x", "u"]]]]]], 
            Algorithm[distribute, {29}]}, {31, 
            ALL["u", 
              IMPLIES[ALL["r", 
                  NOT[IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]], 
                NOT[ALL["x", MEMBER["x", "u"]]]]], 
            ModusPonens[27, 30]}, {32, 
            IMPLIES[ALL["u", 
                ALL["r", 
                  NOT[IFF[MEMBER["r", "r"], 
                      NOT[MEMBER["r", "r"]]]]]], 
              ALL["u", NOT[ALL["x", MEMBER["x", "u"]]]]], 
            Algorithm[distribute, {31}]}, {33, 
            ALL["u", NOT[ALL["x", MEMBER["x", "u"]]]], 
            ModusPonens[28, 32]}, {34, 
            IMPLIES[ALL["u", 
                NOT[ALL["x", MEMBER["x", "u"]]]], 
              NOT[NOT[ALL["u", 
                    NOT[ALL["x", MEMBER["x", "u"]]]]]]], 
            Axiom["Ax. 1"]}, {35, 
            NOT[
              NOT[ALL["u", 
                  NOT[ALL["x", MEMBER["x", "u"]]]]]], 
            ModusPonens[33, 34]}};\)\)

CheckProof[universe]

The corresponding fully formal proof is more than twice as long.

CheckProof[FullProof[universe]]

6 Modifying the SetTheory.m Package

Modifying the Well-Formed Formulas

Suppose that in addition to the usual inclusive-or OR, you wish to include the exclusive-or XOR in well-formed formulas.  The SetTheory.m package divides the heads of the various subexpressions of well-formed formulas into three categories: $AtomicHeads, $Connectives, and $TermHeads.  The exclusive-or is a logical connective, so it should be added to the list $Connectives.

$Connectives

The list $Connectives is composed of pairs {x, y}.  Each x is a logical connective function, and each y is a truth-valued function which defines the truth table for its corresponding x.  Mathematica's built-in function Xor defines the truth table for the exclusive-or, so the pair {XOR, Xor} should be appended to $Connectives if you wish to include XOR in well-formed formulas.

Unprotect[$Connectives]

$Connectives  =  Append[$Connectives,  {XOR,  Xor}]

Protect[$Connectives]

$Connectives

XOR can now be used in well-formed formulas.

\(xorproof\  ** 
1\  ** 

      NOT[XOR[EQUAL["a", "b"], \ EQUAL["a", "b"]]]\  ** 

      Axiom["Ax. 1"]\)

CheckProof[xorproof,  DisplayProof -> False]

If, instead of a logical connective, you wish to add a new predicate parameter or function symbol, then simply append that function to the list $AtomicHeads or $TermHeads, respectively.

$AtomicHeads

$TermHeads

Note that ALL is not a member of $AtomicHeads, $Connectives, or $TermHeads, but is a member of $WffHeads.

$WffHeads

ALL is a quantifier symbol.  New quantifier symbols cannot easily be added to the SetTheory.m package.  See the next subsection, below, for alternatives.

Although XOR can now be used in well-formed formulas, you must be careful.  Many algorithms in the SetTheory.m package may mistake a not-well-formed formula involving XOR as well-formed because XOR does not abort when it has improper arguments.  For example, both OR["x"] and XOR["x"] are not-well-formed, but only OR["x"] aborts.

OR["x"]

XOR["x"]

XOR should be defined so that it aborts whenever it has the wrong number of arguments or the wrong type of arguments.  The arguments of any function in a well-formed formula should either be terms or well-formed formulas.  Use the function TermQ to determine whether or not an argument is a term, and use the function WffQ to determine whether or not an argument is a well-formed formula.  When defining a new function, it is instructive to look at the definitions for a similar function—in this case, OR.

?? OR

XOR should be defined as follows.

\(XOR[]\  := \ \((Message[General::nwff, 
          XOR]; \ 
		Abort[])\)\)

\(XOR[
        a_]\  := \ \((Message[General::nwff, 
          XOR]; 
		Abort[])\)\)

\(XOR[a_\  /; \ \(! WffQ[a]\), 
        b_]\  := \ \((Message[General::nwff, 
          XOR]; 
		Abort[])\)\)

\(XOR[a_, 
        b_\  /; \ \(! WffQ[b]\)]\  := \ \((Message[General::nwff, 
          XOR]; 
		Abort[])\)\)

\(XOR[a_, \ b_, 
        c__]\  := \ \((Message[General::nwff, 
          XOR]; 
		Abort[])\)\)

Now XOR aborts when it has improper arguments, and thus can safely be used in well-formed formulas.

XOR["x"]

Modifying the Symbolic Display of Well-Formed Formulas

In the previous subsection, above, a new function XOR was introduced to well-formed formulas.  The SetTheory.m package was not given instructions for the symbolic output of XOR, though.

CheckProof[xorproof]

You can suppress the symbolic output of well-formed formulas by specifying the option SymbolicForm -> False for CheckProof or DisplayProof.

CheckProof[xorproof,  SymbolicForm  ->  False]

DisplayProof[xorproof,  SymbolicForm  ->  False]

CheckProof and DisplayProof prepare a well-formed formula wff for output with the expression Flatten[ReplaceRepeated[{wff}, $TranslationList]].  Under typical conditions, this expression outputs a list of strings which are then concatenated to form the output string which is displayed.  $TranslationList is a list of rules which determine how a well-formed formula is translated into symbolic output.  Normally, the functions in $TermHeads and $WffHeads do not accept arguments which are patterns.  While working with $TranslationList, you may require that some of these functions accept patterns for arguments.  Set $AllowPatterns to True.  When $AllowPatterns is True, the functions in $TermHeads and $WffHeads will accept arguments whose heads are members of $PatternsHeads.

Unprotect[$AllowPatterns]

$AllowPatterns  =  True

Protect[$AllowPatterns]

$TranslationList  //  InputForm

Rules for translating new functions, such as XOR, can be added to $TranslationList.

Unprotect[$TranslationList]

\(\($TranslationList\  = \ 
	
        Join[\ $TranslationList, 
		{XOR[
                x_\  /; \ MemberQ[{ALL, \ EQUAL, \ MEMBER, \ NOT, \ SUBSET, 
                      XOR}, \ Head[x]], 
                y_\  /; \ MemberQ[{ALL, \ EQUAL, \ MEMBER, \ NOT, \ SUBSET, 
                      XOR}, \ Head[
                      y]]]\  -> \ {x, \ " ", \ "xor", \ " ", 
                y}, 
			
			XOR[
                x_\  /; \ MemberQ[{ALL, \ EQUAL, \ MEMBER, \ NOT, \ SUBSET, 
                      XOR}, \ Head[x]], 
                y_]\  -> 
				{x, \ " ", \ "xor", \ " ", \ "(", \ y, \ ")"}, 
			
			XOR[x_, 
                y_\  /; \ MemberQ[{ALL, \ EQUAL, \ MEMBER, \ NOT, \ SUBSET, 
                      XOR}, \ Head[y]]]\  -> 
				{"(", 
                x, \ ")", \ " ", \ "xor", \ " ", 
                y}, 
			
			XOR[x_, \ y_]\  -> 
				{"(", 
                x, \ ")", \ " ", \ "xor", \ " ", \ "(", 
                y, \ ")"}
		}
	];\)\)

Protect[$TranslationList]

Unprotect[$AllowPatterns]

$AllowPatterns  =  False

Protect[$AllowPatterns]

Note that the order of the rules in $TranslationList is important because rules at the beginning of the list are used before rules at the end.

CheckProof[xorproof]

New quantifier symbols should not be added to the SetTheory.m package without rewriting some of the logical axioms.  A more workable solution is to use the $TranslationList to translate well-formed formulas without a new quantifier symbol into well-formed formulas with that quantifier symbol.  For example, consider the existential quantifier ∃.  Any well-formed formula of the form ∃x(α) is logically equivalent to ¬∀x ¬α, where x is any variable and α ia any well-formed formula.  So, $TranslationList can be modified to translate any formula of the form NOT[ALL[ x, NOT[α]]] into ∃x(α).

Unprotect[$AllowPatterns]

$AllowPatterns  =  True

Protect[$AllowPatterns]

Unprotect[$TranslationList]

\(\($TranslationList\  = \ 
	
        Join[\ 
		{NOT[
                ALL[\ x_, 
                  NOT[\ y_\  /; 
                      MemberQ[{ALL, \ EQUAL, \ MEMBER, \ NOT, \ SUBSET}, 
                        Head[y]]]]]\  -> 
				{"∃", 
                x, \ " ", \ y}, 
			
			NOT[
                ALL[x_, \ NOT[y_]]]\  -> 
				{"∃", 
                x, \ "(", 
                y, \ ")"}
		}, 
		$TranslationList
	];\)\)

Protect[$TranslationList]

Unprotect[$AllowPatterns]

$AllowPatterns  =  False

Protect[$AllowPatterns]

The existential quantifier ∃ now appears in proofs such as that corresponding to simpleproof from section 4, above.

CheckProof[simpleproof]

Modifying the Axioms

The name of each axiom which is admissible in a valid proof is stored as a string in the list $AxiomList.

$AxiomList

To make an axiom inadmissible in any valid proof, simply delete the name of that axiom from $AxiomList.

\(intersectionproof\  ** 
1\  ** 

      ALL["x", 
        ALL["y", 
          IFF[EQUAL["x", \ INTERSECTION["y"]], 
            ALL["a", 
              IFF[MEMBER["a", "x"], 
                ALL["b", 
                  IMPLIES[MEMBER["b", "y"], 
                    MEMBER["a", "b"]]]]]]]]\  ** 

      Axiom["Intersection Def."]\)

CheckProof[intersectionproof]

Unprotect[$AxiomList]

$AxiomList  = 
      DeleteCases[$AxiomList,  "Intersection Def."]

Protect[$AxiomList]

CheckProof[intersectionproof]

When a well-formed formula wff is justified by Axiom[axm] in a proof-list prf, CheckProof[prf] sets $AllowPatterns to True and evaluates AxiomQ[axm, wff].  If AxiomQ[axm, wff] is True, then wff is an instance of axiom axm.  It is important that $AllowPatterns be set to True so that AxiomQ can use pattern-matching functions such as MatchQ.  To add a new axiom naxm to the SetTheory.m package, define AxiomQ[naxm, wff_] and append naxm to $AxiomList.

Unprotect[$AllowPatterns,  $AxiomList,  AxiomQ]

$AllowPatterns  =  True

Protect[$AllowPatterns]

\(\(\(AxiomQ["New Intersection Def.", \ wff_]\  := 
	
        MatchQ[wff, 
		ALL[
              x_, 
			ALL[
                y_, 
				IFF[
					EQUAL[x_, 
                    INTERSECTION[
                      y_]], 
					AND[
						IMPLIES[
							EQUAL[y_, \ EMPTYSET[]], 
							EQUAL[x_, 
                        EMPTYSET[]]
						], 
						IMPLIES[
							NOT[
								EQUAL[y_, 
                          EMPTYSET[]]
							], 
							ALL[
                        a_, 
								IFF[
									MEMBER[
                            a_, \ x_], 
									ALL[
                            b_, 
										IMPLIES[
											MEMBER[b_, \ y_], 
											MEMBER[a_, 
                                b_]
										]
									]
								]
							]
						]
					]
				]
			]
		]\  /; 
            StringQ[x]\  && \ StringQ[y]\  && \ StringQ[a]\  && 
              StringQ[b]\  && \ x =!= y =!= a\  && 
              b =!= y =!= a
	];\)\(
\)\)\)

$AxiomList  = 
      Append[$AxiomList,  "New Intersection Def."]

Unprotect[$AllowPatterns]

$AllowPatterns  =  False

Protect[$AllowPatterns,  $AxiomList,  AxiomQ]

The new intersection definition defines ⋂⌀ to be ⌀.

\(newintersectionproof\  ** 
1\  ** 

      ALL["y", 
        ALL["z", 
          IFF[EQUAL["y", \ INTERSECTION["z"]], 
            AND[IMPLIES[EQUAL["z", \ EMPTYSET[]], 
                EQUAL["y", \ EMPTYSET[]]], 
              IMPLIES[NOT[EQUAL["z", \ EMPTYSET[]]], 
                ALL["a", 
                  IFF[MEMBER["a", \ "y"], 
                    ALL["b", 
                      IMPLIES[MEMBER["b", \ "z"], 
                        MEMBER["a", \ "b"]]]]]]]]]] ** 

      Axiom["New Intersection Def."]\)

CheckProof[newintersectionproof]