(*:Name: SetTheory *) (*:Title: Formal Proofs in Axiomatic Set Theory *) (*:Author: Matthew P. Szudzik *) (*:E-Mail Address: m.szudzik@member.ams.org *) (*:Summary: This 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. *) (*:Package Version: 1.1 *) (*:Mathematica Version: 4.0 *) (*:History: Version 1.0 created in July 1998 by Matthew P. Szudzik Version 1.1 updated for Mathematica 4.0 in November 1999 by Matthew P. Szudzik *) (*:Warnings: This package redefines NonCommutativeMultiply *) BeginPackage["SetTheory`"]; $AllowPatterns::usage = "When $AllowPatterns is set to True, WffQ[x] and TermQ[x] will give True if \ the head of x is a member of $PatternHeads. Set $AllowPatterns to True if \ you want one of the functions in $TermHeads or $WffHeads to accept patterns \ as inputs."; $AtomicHeads::usage = "$AtomicHeads is a list of the heads of all atomic well-formed formulas. \ Any member of $AtomicHeads is automatically a member of $WffHeads. In a \ well-formed formula, the arguments of any of the members of $AtomicHeads \ should have heads which are members of $TermHeads."; $AxiomList::usage = "$AxiomList is a list of strings, each being the name of an axiom. \ CheckProof will not recognize an axiom unless its name is a member of \ $AxiomList."; $Connectives::usage = "$Connectives is a list of pairs {x, y}. All x are interpreted as the \ heads of logical connective functions for use in well-formed formulas. All x \ are automatically members of $WffHeads. In a well-formed formula, the \ arguments of any of the x should have heads which are members of $WffHeads. \ Each y is the head of the truth-valued function which defines the \ corresponding x's truth table."; $LineBreakStrings::usage = "$LineBreakStrings is a list of lists. Each list in $LineBreakStrings \ contains strings immediately after which a line-break is allowed to occur in \ strings which are displayed with CheckProof or DisplayProof. Given a string \ which must be of a length less than or equal to that dictated by \ $MaxColumnWidths, CheckProof and DisplayProof consult the initial list in \ $LineBreakStrings. If the line-breaks allowed by that list are insufficient \ to reduce the string to a proper length, then the next list in \ $LineBreakStrings is consulted, and so on."; $MaxColumnWidths::usage = "$MaxColumnWidths is a list of the form {num, wff, jst}, where num is the \ maximum number of characters allowed in the line number column of a proof, \ wff is the maximum number of characters allowed in the well-formed formula \ column of a proof, and jst is the maximum number of characters allowed in the \ justification column of a proof."; $JustificationHeads::usage = "$JustificationHeads is a list of the heads of expressions which are \ allowed to justify a well-formed formula in a line of a proof-list."; $PatternHeads::usage = "$PatternHeads is a list of those heads of the arguments of the members of \ $TermHeads and $WffHeads which are allowed when $AllowPatterns is True."; $TermHeads::usage = "$TermHeads is a list of the heads of all terms which can appear in a \ well-formed formula. In a well-formed formula, for each argument x of a \ member of $TermHeads, TermQ[x] should be True."; $TranslationList::usage = "$TranslationList is a list of rules of the form (pat -> chars) or (pat :> \ chars), where pat is a pattern which can match part of a well-formed formula \ and chars is a list of characters and/or expressions which represent the part \ matching pat for the purposes of display by CheckProof and DisplayProof when \ SymbolicForm -> True. Given a well-formed formula wff, CheckProof and \ DisplayProof use Flatten[ReplaceRepeated[wff, $TranslationList]] to determine \ how wff is displayed. Note that $AllowPatterns should be set to True before \ $TranslationList is called."; $WffHeads::usage = "$WffHeads is a list of the heads of all well-formed formulas. In a \ well-formed formula, for each argument x of a member of $WffHeads, TermQ[x] \ or WffQ[x] should be True. The members of $WffHeads are determined by \ $AtomicHeads and $Connectives."; AddLine::usage = "AddLine[sym, num, wff, jst] appends {num, wff, jst} to sym, where sym is a \ symbol which stands for a valid proof-list. num must be a whole number (i.e. \ a positive integer), WffQ[wff] must be True, and jst must have a head which \ is a member of $JustificationHeads. Any line numbers which jst refers to \ must be less than num. After AddLine is called, the symbol sym will be \ stored as ProofName[], and sym may be omitted from input to AddLine if \ ProofName[] is intended as sym. Furthermore, num may be omitted if sym is \ omitted and num is LastLine[prf] + 1. AddLine[sym, num, wff, jst] may be \ entered in infix form as sym ** num ** wff ** jst."; Algorithm::usage = "{mnum, mwff, Algorithm[f, {num1, num2, ..., numn}]} is a valid line of a \ proof when f[wff1, wff2, ..., wffn] is a proof of mwff in which each of the \ wffi is allowed to be justified by Given[] and is the formula which appears \ as line numi of the main proof, for each i. Each of the numi must be less \ than mnum."; ALL::usage = "ALL[x, wff] is the universal quantifier in well-formed formulas when \ Head[x] is String and WffQ[wff] is True, unless $AllowPatterns is True, in \ which case Head[x] may also be a member of $PatternHeads. ALL is a member of \ $WffHeads."; AND::usage = "AND[x, y] is a logical connective in well-formed formulas when WffQ[x] and \ WffQ[y] are True. The truth table for AND is given by the truth-valued \ function And. {AND, And} is a member of $Connectives."; Axiom::usage = "{num, wff, Axiom[axm]} is a valid line of a proof when axm is a member of \ $AxiomList and AxiomQ[axm, wff] is True."; AxiomQ::usage = "AxiomQ[axm, wff] is True if and only if the well-formed formula wff is an \ instance of the axiom named by the string axm. Note that AxiomQ[axm, wff] \ may attempt to perform a pattern-matching operation on wff, and AxiomQ[axm, \ wff] may abort unless $AllowPatterns is True."; CheckProof::usage = "CheckProof[prf, options] will display the proof given by the proof-list \ prf followed by \"Q.E.D.\", if and only if it is a valid proof. CheckProof \ takes the options DisplayProof, GivensList, and SymbolicForm. By default, \ DisplayProof -> True, GivensList -> {}, and SymbolicForm -> True. If \ DisplayProof -> False, then CheckProof will output True if and only if the \ proof is valid. If GivensList -> lst and lst is a list of well-formed \ formulas, then those formulas may be justified by Given[] in prf. If \ SymbolicForm -> False, then the $TranslationList will not be used to \ represent the well-formed formulas, and they will be displayed as they were \ input."; DisplayProof::usage = "DisplayProof[prf, options] simply displays the proof given by the \ proof-list prf. DisplayProof takes the option SymbolicForm. By default, \ SymbolicForm -> True. If SymbolicForm -> False, then the $TranslationList \ will not be used to represent the well-formed formulas, and they will be \ displayed as they were input.\n\nDisplayProof is also an option for \ CheckProof. By default, DisplayProof -> True. If DisplayProof -> False, \ then CheckProof[prf, DisplayProof -> False] will output True if prf is the \ proof-list of a valid proof."; EMPTYSET::usage = "EMPTYSET[] is the term for the empty set in well-formed formulas. \ EMPTYSET is a member of $TermHeads."; EQUAL::usage = "EQUAL[x, y] is the atomic formula for equality in well-formed formulas \ when TermQ[x] and TermQ[y] are True. EQUAL is a member of $AtomicHeads."; FullProof::usage = "FullProof[prf] outputs a proof which is equivalent to the proof prf, but \ in which no formulas are justified with Algorithm."; Given::usage = "{num, wff, Given[]} is a valid line of a proof when GivensList -> lst and \ wff is a member of the list lst."; GivensList::usage = "GivensList is an option for CheckProof. By default, GivensList -> {}. If \ GivensList -> lst and lst is a list of well-formed formulas, then those \ formulas may be justified by Given[]."; Iff::usage = "Iff[x, y] is the truth-valued function equivalent to And[Implies[x, y], \ Implies[y, x]]."; IFF::usage = "IFF[x, y] is a logical connective in well-formed formulas when WffQ[x] and \ WffQ[y] are True. The truth table for IFF is given by the truth-valued \ function Iff. {IFF, Iff} is a member of $Connectives."; IMPLIES::usage = "IMPLIES[x, y] is a logical connective in well-formed formulas when WffQ[x] \ and WffQ[y] are True. The truth table for IMPLIES is given by the \ truth-valued function Implies. {IMPLIES, Implies} is a member of \ $Connectives."; INTERSECTION::usage = "INTERSECTION[x] is the term for the intersection of a set x in well-formed \ formulas when TermQ[x] is True. INTERSECTION is a member of $TermHeads."; LastLine::usage = "LastLine[prf] gives the greatest line number in the proof-list prf."; MEMBER::usage = "MEMBER[x, y] is the atomic formula for set membership in well-formed \ formulas when TermQ[x] and TermQ[y] are True. MEMBER is a member of \ $AtomicHeads."; ModusPonens::usage = "{num, g, ModusPonens[x, y]} is a valid line of a proof when x and y are \ the line numbers of the well-formed formulas f and IMPLIES[f, g], for any \ well-formed formula f. x and y must be less than num. The order of the \ arguments x and y is unimportant."; NonCommutativeMultiply::usage = "NonCommutativeMultiply[args] is defined as AddLine[args] for all arguments \ args."; NOT::usage = "NOT[x] is a logical connective in well-formed formulas when WffQ[x] is \ True. The truth table for NOT is given by the truth-valued function Not. \ {NOT, Not} is a member of $Connectives."; OR::usage = "OR[x, y] is a logical connective in well-formed formulas when WffQ[x] and \ WffQ[y] are True. The truth table for OR is given by the truth-valued \ function Or. {OR, Or} is a member of $Connectives."; POWERSET::usage = "POWERSET[x] is the term for the power set of a set x in well-formed \ formulas when TermQ[x] is True. POWERSET is a member of $TermHeads."; ProofName::usage = "ProofName[] is HoldForm[sym], where sym is a symbol for the last \ proof-list to be called by AddLine or RemoveLine."; RemoveLine::usage = "RemoveLine[sym, num] removes line num from sym, where sym is a symbol \ which stands for a valid proof-list. num must be a whole number (i.e. a \ positive integer). After RemoveLine is called, the symbol sym will be stored \ as ProofName[], and sym may be omitted from input to RemoveLine if \ ProofName[] is intended as sym."; RenumberProof::usage = "RenumberProof[prf, x, dx] outputs a proof equivalent to the valid proof \ prf, whose first line is number x, and whose nth line is number x + (n-1) \ dx."; SET::usage = "SET[x1, x2, ..., xn] is the term for the set with members x1, x2, ..., xn \ in well-formed formulas when TermQ[xi] is True for each i. SET is a member \ of $TermHeads."; SUBSET::usage = "SUBSET[x, y] is the atomic formula for set inclusion in well-formed \ formulas when TermQ[x] and TermQ[y] are True. SUBSET is a member of \ $TermHeads."; SymbolicForm::usage = "SymbolicForm is an option for CheckProof and DisplayProof. By default, \ SymbolicForm -> True. If SymbolicForm -> False, then the $TranslationList \ will not be used to represent the well-formed formulas, and they will be \ displayed as they were input."; TermQ::usage = "TermQ[x] is True if the head of x is a member of $TermHeads and False if \ it is not, unless $AllowPatterns is True, in which case TermQ[x] is also True \ if the head of x is a member of $PatternHeads."; UNION::usage = "UNION[x] is the term for the union of a set x in well-formed formulas when \ TermQ[x] is True. UNION is a member of $TermHeads."; WffQ::usage = "WffQ[x] is True if the head of x is a member of $WffHeads and False if it \ is not, unless $AllowPatterns is True, in which case WffQ[x] is also True if \ the head of x is a member of $PatternHeads."; Unprotect[$AllowPatterns, $AtomicHeads, $AxiomList, $Connectives, $LineBreakStrings, $MaxColumnWidths, $JustificationHeads, $PatternHeads, $TermHeads, $TranslationList, $WffHeads, AddLine, Algorithm, ALL, AND, Axiom, AxiomQ, CheckProof, DisplayProof, EMPTYSET, EQUAL, FullProof, Given, GivensList, Iff, IFF, IMPLIES, INTERSECTION, LastLine, MEMBER, ModusPonens, NonCommutativeMultiply, NOT, OR, POWERSET, ProofName, RemoveLine, RenumberProof, SET, SUBSET, SymbolicForm, TermQ, UNION, WffQ]; Begin["`Private`"]; (* Section 1: Well-Formed Formulas *) (* Section 1.1: Definitions *) $AllowPatterns = False; $AtomicHeads = {EQUAL, MEMBER, SUBSET}; $Connectives = {{AND, And}, {IFF, Iff}, {IMPLIES, Implies}, {NOT, Not}, {OR,Or}}; $Connectives::incorrect = "$Connectives has incorrect form."; $LineBreakStrings = {{"& ", "\[LeftRightArrow] ", "\[RightArrow] ", "or "}, {"=", "\[Element]", "\[SubsetEqual]"}, {" ","\[Diameter]"}, { "[", "(", "{"}, {".", ",", "\[Intersection]", "\[Union]", "\[ScriptCapitalP]"}}; $LineBreakStrings::incorrect = "$LineBreakStrings has incorrect form."; $MaxColumnWidths = {3, 51, 20}; $MaxColumnWidths::incorrect = "$MaxColumnWidths has incorrect form."; $PatternHeads = {Alternatives, Blank, Condition, HoldPattern, List, Optional, Pattern, Verbatim}; $TermHeads = {EMPTYSET, INTERSECTION, POWERSET, SET, String,UNION}; $TranslationList = { ALL[x_, y_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[y]]] -> {"\[ForAll]", x, " ", y}, ALL[x_, y_] -> {"\[ForAll]", x, "(", y, ")"}, AND[x_ /; MemberQ[{ALL, AND, EQUAL, MEMBER, NOT, SUBSET}, Head[x]], y_ /; MemberQ[{ALL, AND, EQUAL, MEMBER, NOT, SUBSET}, Head[y]]] -> {x, " ", "&", " ", y}, AND[x_ /; MemberQ[{ALL, AND, EQUAL, MEMBER, NOT, SUBSET}, Head[x]], y_] -> {x, " ", "&", " ", "(", y, ")"}, AND[x_, y_ /; MemberQ[{ALL, AND, EQUAL, MEMBER, NOT, SUBSET}, Head[y]]] -> {"(", x, ")", " ", "&", " ", y}, AND[x_, y_] -> {"(", x, ")", " ", "&", " ", "(", y, ")"}, EMPTYSET[] -> {"\[Diameter]"}, EQUAL[x_, y_] -> {x, "=", y}, IFF[x_ /; MemberQ[{ALL, EQUAL, IFF, MEMBER, NOT, SUBSET}, Head[x]], y_ /; MemberQ[{ALL, EQUAL, IFF, MEMBER, NOT, SUBSET}, Head[y]]] -> {x, " ", "\[LeftRightArrow]", " ", y}, IFF[x_ /; MemberQ[{ALL, EQUAL, IFF, MEMBER, NOT, SUBSET}, Head[x]], y_] -> {x, " ", "\[LeftRightArrow]", " ", "(", y, ")"}, IFF[x_, y_ /; MemberQ[{ALL, EQUAL, IFF, MEMBER, NOT, SUBSET}, Head[y]]] -> {"(", x, ")", " ", "\[LeftRightArrow]", " ", y}, IFF[x_, y_] -> {"(", x, ")", " ", "\[LeftRightArrow]", " ", "(", y, ")"}, IMPLIES[x_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[x]], y_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[y]]]-> {x, " ", "\[RightArrow]", " ", y}, IMPLIES[x_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[x]], y_] -> {x, " ", "\[RightArrow]", " ", "(", y, ")"}, IMPLIES[x_, y_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[y]]] -> {"(", x, ")", " ", "\[RightArrow]", " ", y}, IMPLIES[x_, y_] -> {"(", x, ")", " ", "\[RightArrow]", " ", "(", y, ")"}, INTERSECTION[x_] -> {"\[Intersection]", x}, MEMBER[x_, y_] -> {x, "\[Element]", y}, NOT[x_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, SUBSET}, Head[x]]] -> {"\[Not]", x}, NOT[x_] -> {"\[Not]", "(", x, ")"}, OR[x_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, OR, SUBSET}, Head[x]], y_ /; MemberQ[{ALL, EQUAL, MEMBER, OR, SUBSET}, Head[y]]] -> {x, " ", "or", " ", y}, OR[x_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, OR, SUBSET}, Head[x]], y_] -> {x, " ", "or", " ", "(", y, ")"}, OR[x_, y_ /; MemberQ[{ALL, EQUAL, MEMBER, NOT, OR, SUBSET}, Head[y]]] -> {"(", x, ")", " ", "or", " ", y}, OR[x_, y_] -> {"(", x, ")", " ", "or", " ", "(", y, ")"}, POWERSET[x_] -> {"\[ScriptCapitalP]", x}, SET[x__] :> Join[{"{"}, Drop[Flatten[ Map[({#, ",", " "})&, {x}]], -2], {"}"}], SUBSET[x_, y_] -> {x, "\[SubsetEqual]", y}, UNION[x_] -> {"\[Union]", x} }; $TranslationList::incorrect = "$TranslationList has incorrect form."; $WffHeads := If[ Apply[And, Map[(Head[#]===List && Length[#]=== 2)&, $Connectives]], Union[{ALL}, $AtomicHeads, first[transpose[$Connectives]]], Message[$Connectives::incorrect]; Abort[]]; General::nwff = "A not-well-formed formula has been encountered. `1` has improper \ arguments."; Iff::arguments = "Iff has improper arguments."; TermQ::arguments = "TermQ has improper arguments."; WffQ::arguments = "WffQ has improper arguments."; (* Section 1.2: Local Functions *) first[{}] := {}; first[x_] := First[x]; last[{}] := {}; last[x_] := Last[x]; logicQ[x_] := If[x===True || x===False, True, False]; transpose[{}] := {}; transpose[x_] := Transpose[x]; (* Section 1.3: Exported Functions *) ALL[] := (Message[General::nwff, ALL]; Abort[]); ALL[x_] := (Message[General::nwff, ALL]; Abort[]); ALL[x_ /; !(Head[x]===String || (MemberQ[$PatternHeads,Head[x]] && $AllowPatterns===True)), a_] := (Message[General::nwff, ALL]; Abort[]); ALL[x_, a_ /; !WffQ[a]] := (Message[General::nwff, ALL]; Abort[]); ALL[x_, a_, c__] := (Message[General::nwff, ALL]; Abort[]); AND[] := (Message[General::nwff, AND]; Abort[]); AND[a_] := (Message[General::nwff, AND]; Abort[]); AND[a_ /; !WffQ[a], b_] := (Message[General::nwff, AND]; Abort[]); AND[a_, b_ /; !WffQ[b]] := (Message[General::nwff, AND]; Abort[]); AND[a_, b_, c__] := (Message[General::nwff, AND]; Abort[]); EMPTYSET[x__] := (Message[General::nwff, EMPTYSET]; Abort[]); EQUAL[] := (Message[General::nwff,EQUAL]; Abort[]); EQUAL[a_] := (Message[General::nwff,EQUAL]; Abort[]); EQUAL[a_ /; !TermQ[a], b_] := (Message[General::nwff,EQUAL]; Abort[]); EQUAL[a_, b_ /; !TermQ[b]] := (Message[General::nwff,EQUAL]; Abort[]); EQUAL[a_, b_, c__] := (Message[General::nwff,EQUAL]; Abort[]); Iff[a_, b_] := Implies[a,b] && Implies[b,a]; Iff[x___] := (Message[Iff::arguments]; Abort[]); IFF[] := (Message[General::nwff,IFF]; Abort[]); IFF[a_] := (Message[General::nwff,IFF]; Abort[]); IFF[a_ /; !WffQ[a], b_] := (Message[General::nwff,IFF]; Abort[]); IFF[a_, b_ /; !WffQ[b]] := (Message[General::nwff,IFF]; Abort[]); IFF[a_, b_, c__] := (Message[General::nwff,IFF]; Abort[]); IMPLIES[] := (Message[General::nwff,IMPLIES]; Abort[]); IMPLIES[a_] := (Message[General::nwff,IMPLIES]; Abort[]); IMPLIES[a_ /; !WffQ[a], b_] := (Message[General::nwff,IMPLIES]; Abort[]); IMPLIES[a_, b_ /; !WffQ[b]] := (Message[General::nwff,IMPLIES]; Abort[]); IMPLIES[a_, b_, c__] := (Message[General::nwff,IMPLIES]; Abort[]); INTERSECTION[] := (Message[General::nwff,INTERSECTION]; Abort[]); INTERSECTION[a_ /; !TermQ[a]] := (Message[General::nwff,INTERSECTION]; Abort[]); INTERSECTION[a_, b__] := (Message[General::nwff,INTERSECTION]; Abort[]); MEMBER[ ] := (Message[General::nwff,MEMBER]; Abort[]); MEMBER[ a_] := (Message[General::nwff,MEMBER]; Abort[]); MEMBER[ a_ /; !TermQ[a], b_] := (Message[General::nwff,MEMBER]; Abort[]); MEMBER[ a_, b_ /; !TermQ[b]] := (Message[General::nwff,MEMBER]; Abort[]); MEMBER[a_, b_, c__] := (Message[General::nwff,MEMBER]; Abort[]); NOT[] := (Message[General::nwff,NOT]; Abort[]); NOT[a_ /; !WffQ[a]] := (Message[General::nwff,NOT]; Abort[]); NOT[a_, c__] := (Message[General::nwff,NOT]; Abort[]); OR[] := (Message[General::nwff,OR]; Abort[]); OR[a_] := (Message[General::nwff,OR]; Abort[]); OR[a_ /; !WffQ[a], b_] := (Message[General::nwff,OR]; Abort[]); OR[a_, b_ /; !WffQ[b]] := (Message[General::nwff,OR]; Abort[]); OR[a_, b_, c__] := (Message[General::nwff,OR]; Abort[]); POWERSET[] := (Message[General::nwff,POWERSET]; Abort[]); POWERSET[a_ /; !TermQ[a]] := (Message[General::nwff,POWERSET]; Abort[]); POWERSET[a_, b__] := (Message[General::nwff,POWERSET]; Abort[]); SET[] := (Message[General::nwff,SET]; Abort[]); SET[a__ /; ! Apply[ And, Map[TermQ, {a}]]] := (Message[General::nwff,SET]; Abort[]); SUBSET[] := (Message[General::nwff,SUBSET]; Abort[]); SUBSET[a_] := (Message[General::nwff,SUBSET]; Abort[]); SUBSET[a_ /; !TermQ[a], b_] := (Message[General::nwff,SUBSET]; Abort[]); SUBSET[a_, b_ /; !TermQ[b]] := (Message[General::nwff,SUBSET]; Abort[]); SUBSET[a_, b_, c__] := (Message[General::nwff,SUBSET]; Abort[]); TermQ[ e_] := If[MemberQ[$PatternHeads,Head[e]] && $AllowPatterns === True, True, MemberQ[ $TermHeads, Head[e]] ]; TermQ[e___] := (Message[TermQ::arguments]; Abort[]); UNION[] := (Message[General::nwff,UNION]; Abort[]); UNION[a_ /; !TermQ[a]] := (Message[General::nwff,UNION]; Abort[]); UNION[a_, b__] := (Message[General::nwff,UNION]; Abort[]); WffQ[ e_] := If[MemberQ[$PatternHeads,Head[e]] && $AllowPatterns === True, True, MemberQ[ $WffHeads, Head[e]] ]; WffQ[e___] := (Message[WffQ::arguments]; Abort[]); (* Section 2: Justifications *) (* Section 2.1: Definitions *) $AxiomList = {"Ax. 1", "Ax. 2", "Ax. 3", "Ax. 4", "Ax. 5", "Ax. 6", "Empty Set Def.", "Intersection Def.", "Power Set Def.", "Set Def.", "Subset Def.", "Union Def.", "Choice Ax.", "Empty Set Ax.", "Extensionality Ax.", "Infinity Ax.", "Pairing Ax.", "Power Set Ax.", "Regularity Ax.", "Replacement Ax.", "Subset Ax.", "Union Ax."}; $AxiomList::missing = "The element `1` could not be found in the list $AxiomList."; $JustificationHeads = {Algorithm, Axiom, Given, ModusPonens}; Algorithm::arguments = "Algorithm has improper arguments."; Axiom::arguments = "Axiom has improper arguments."; Given::arguments = "Given has improper arguments."; ModusPonens::arguments = "ModusPonens has improper arguments."; (* Section 2.2: Local Functions *) wholeQ[x_] := (Head[x] === Integer) && (x > 0); (* Section 2.3: Exported Functions *) Algorithm[] := (Message[Algorithm::arguments]; Abort[]); Algorithm[f_] := (Message[Algorithm::arguments]; Abort[]); Algorithm[f_, x_ /; !(Head[x]===List && Apply[And,Map[wholeQ, x]])] := (Message[Algorithm::arguments]; Abort[]); Algorithm[f_, x_, y__] := (Message[Algorithm::arguments]; Abort[]); Axiom[] := (Message[Axiom::arguments]; Abort[]); Axiom[x_ /; Head[x] =!= String] := (Message[Axiom::arguments]; Abort[]); Axiom[x_, y__] := (Message[Axiom::arguments]; Abort[]); Given[x__] := (Message[Given::arguments]; Abort[]); ModusPonens[] := (Message[ModusPonens::arguments]; Abort[]); ModusPonens[x_] := (Message[ModusPonens::arguments]; Abort[]); ModusPonens[x_ /;!wholeQ[x] , y_] := (Message[ModusPonens::arguments]; Abort[]); ModusPonens[x_, y_/;!wholeQ[y]] := (Message[ModusPonens::arguments]; Abort[]); ModusPonens[x_, y_, z__] := (Message[ModusPonens::arguments]; Abort[]); (* Section 3: Manipulation of Proofs *) (* Section 3.1: Definitions *) AddLine::arguments = "AddLine has improper arguments."; DisplayProof::arguments = "DisplayProof has improper arguments."; DisplayProof::options = "The options for DisplayProof have improper values."; Options[DisplayProof] = {SymbolicForm->True}; FullProof::abort = "FullProof has been aborted."; FullProof::algorithm = "`2` is not justified by the algorithm."; FullProof::arguments = "FullProof has improper arguments."; FullProof::noline = "A line which does not exist is called as justification."; General::badline = "`1` is not a properly formatted line of a proof."; General::duplicates = "Multiple lines of the proof are labeled as number `1`."; General::noline = "The proof has no line `1`."; General::prooflist = "A proof must be input as a list of lines. `1` is not a list."; General::proofsymbol = "`1` requires that `2` be a symbol which stands for a proof-list."; General::protectedproof = "Symbol `1` is protected. Either choose a different name for the proof or \ unprotect `1`."; LastLine::arguments = "LastLine has improper arguments."; ProofName::arguments = "ProofName has improper arguments."; RemoveLine::arguments = "RemoveLine has improper arguments."; RenumberProof::arguments = "RenumberProof has improper arguments."; (* Section 3.2: Local Functions *) broken[ string_, length_] := GridBox[Map[(List[ToBoxes[#]])&, Flatten[linebreak[string, length, $LineBreakStrings]]], ColumnAlignments -> Left]; checksymbol[x_, f_] := Which[ ! MatchQ[Hold[x], Hold[_Symbol]], Message[General::proofsymbol, f, HoldForm[x]]; Abort[], MemberQ[Attributes[x], Protected], Message[General::protectedproof, HoldForm[x]]; Abort[] ]; SetAttributes[checksymbol, HoldFirst]; displayproof[proof_List, symbolicform_ /; logicQ[symbolicform]] := Module[ {out}, validprooflist[proof]; If[ ! MatchQ[$MaxColumnWidths, {a_ /; wholeQ[a], b_ /; wholeQ[b], c_ /; wholeQ[c]}], Message[$MaxColumnWidths::incorrect]; Abort[] ]; If[symbolicform, out = Apply[{tostring[#1], tosymbolic[#2], justify[#3]}&, proof, {1}], out = Apply[{tostring[#1], tostring[#2], justify[#3]}&, proof, {1}] ]; out = Map[(MapThread[broken, {#, $MaxColumnWidths}])&,out]; out = Join[out, {{"","",""}}]; out = GridBox[out, ColumnAlignments->{Right, Left, Left}, RowAlignments->Top, ColumnSpacings->3, RowSpacings->2]; out = StyleBox[out, AutoSpacing -> False]; DisplayForm[out] ]; displayproof[x___] := (Message[DisplayProof::options]; Abort[]); justify[just_] := Which[ Head[just]===Axiom, First[just], Head[just]===ModusPonens, StringJoin["M.P. ", tostring[First[just]], ", ", tostring[Last[just]]], Head[just]===Given, "Given", True, tostring[just] ]; lastproof[name_] := ( Unprotect[AddLine]; (AddLine[wff_, just_] := ( validprooflist[name]; AddLine[name, LastLine[name] + 1, wff,just] ) ); (AddLine[num_, wff_, just_] := AddLine[name, num, wff, just]); Protect[AddLine]; Unprotect[RemoveLine]; (RemoveLine[num_] := RemoveLine[name, num]); Protect[RemoveLine]; Unprotect[ProofName]; (ProofName[] := HoldForm[name]); Protect[ProofName] ); SetAttributes[lastproof, HoldFirst]; linebreak[ string_, length_, chars_] := Module[{pieces}, If[ ! MatchQ[$LineBreakStrings, {x___List} /; MatchQ[Flatten[{x}, 1], {___String}]], Message[$LineBreakStrings::incorrect]; Abort[] ]; Which[ StringLength[string] <= length, {string}, chars === {}, {StringTake[string, length], linebreak[StringDrop[string, length], length, $LineBreakStrings]}, pieces = last[transpose[ stringposition[string, First[chars]]]]; pieces = Select[ pieces, (# <= length)&]; pieces === {}, linebreak[string, length, Rest[chars]], True, {StringTake[string, Max[pieces]], linebreak[StringDrop[string, Max[pieces]], length, $LineBreakStrings]} ] ]; lineQ[x_List] := Module[{just, num, wff}, Length[x] === 3 && (num = Part[x, 1]; wff = Part[x, 2]; just = Part[x, 3]; wholeQ[num]) && WffQ[wff] && MemberQ[$JustificationHeads, Head[just]] && If[Head[just]===ModusPonens, (First[just] < num) && (Last[just] < num), True] && If[Head[just] === Algorithm, Apply[ And, Map[ Positive, num - Last[just]]], True] ]; lineQ[x_] := False; max[{}] := 0; max[x_List] := Max[x]; pass[f_, just_] := Which[ Head[just] === ModusPonens, Map[f, just], Head[just] === Algorithm, Algorithm[First[just], Map[f, Last[just]]], True, just ]; stringposition[x_, {}] := StringPosition[x, {""}]; stringposition[x___] := StringPosition[x]; tostring[x_] := ToString[x, FormatType->InputForm]; tosymbolic[wff_] := Module[{l1,l2, l3}, CheckAbort[ Unprotect[$AllowPatterns]; $AllowPatterns = True; If[ !MatchQ[$TranslationList, x_List /; Apply[ And, Map[(Head[#]===Rule || Head[#] === RuleDelayed)&, x]] ], Message[$TranslationList::incorrect]; Abort[]]; l1 = ReplaceRepeated[{wff}, $TranslationList]; l2 = Flatten[l1]; l3 = Map[If[Head[#]===String, #, tostring[#]]&,l2]; $AllowPatterns = False; Protect[$AllowPatterns], Unprotect[$AllowPatterns]; $AllowPatterns = False; Protect[$AllowPatterns]; Abort[] ]; StringJoin[l3] ]; validprooflist[x_] := Module[{t, u, v, w}, Which[ Head[x] =!= List, Message[General::prooflist, HoldForm[x]]; Abort[], t = Map[lineQ, x]; ! Apply[And,t], Message[General::badline, Part[x,Min[Flatten[Position[t, False]]]]]; Abort[], u = first[transpose[x]]; v = Union[u]; w = Sort[u]; v=!=w, Message[General::duplicates, Min[Flatten[Cases[Split[w], {_, __}]]] ]; Abort[] ] ]; SetAttributes[validprooflist, HoldFirst]; (* Section 3.3: Exported Functions *) NonCommutativeMultiply[ x___] := AddLine[x]; ClearAttributes[NonCommutativeMultiply, Attributes[NonCommutativeMultiply]]; SetAttributes[NonCommutativeMultiply, HoldFirst]; AddLine[ wff_, just_] := (Message[General::protectedproof, HoldForm[Null]]; Abort[]); AddLine[num_,wff_, just_] := (Message[General::protectedproof, HoldForm[Null]]; Abort[]); AddLine[ x___] := (Message[AddLine::arguments]; Abort[]); AddLine[ name_, num_/; wholeQ[num], wff_/; WffQ[wff], just_/; MemberQ[$JustificationHeads, Head[just]]] := ( checksymbol[name, AddLine]; If[Head[name] === Symbol, name = {} ]; validprooflist[name]; If[! lineQ[{num, wff, just}], Message[Addline::arguments]; Abort[] ]; name = Union[DeleteCases[name, {num, _, _}, {1}], {{num, wff, just}}]; lastproof[name]; name ); SetAttributes[AddLine, HoldFirst]; DisplayProof[proof_List, options___Rule] := displayproof[proof, SymbolicForm /. {options} /. Options[DisplayProof]]; DisplayProof[x___] := (Message[DisplayProof::arguments]; Abort[]); FullProof[proof_List] := Module[{givens, inputs, just, line, mainproof, num, spacing, subproof, wff}, validprooflist[proof]; CheckAbort[ Unprotect[$AllowPatterns]; mainproof = RenumberProof[proof, 1, 1]; line= first[Cases[mainproof, {_,_,_Algorithm}, {1}]]; While[line=!={}, num = First[line]; wff = Part[line, 2]; just = Last[line]; inputs = Map[(Cases[mainproof, {#, x_, _} -> x, {1}])&, Last[just]]; If[MemberQ[inputs, {}], Message[FullProof::noline]; Abort[] ]; inputs = Flatten[inputs]; $AllowPatterns = True; subproof = Apply[First[just], inputs]; Unprotect[$AllowPatterns]; $AllowPatterns = False; validprooflist[subproof]; If[subproof === {}, Message[FullProof::algorithm,wff]; Abort[] ]; spacing = Length[subproof] + 1; mainproof = RenumberProof[mainproof, spacing, spacing]; mainproof = DeleteCases[mainproof, {spacing*num, _, _}, {1}]; subproof = RenumberProof[subproof, spacing*num + 1, 1]; givens = Map[(Cases[subproof, {x_, #, Given[]}->x, {1}])&, inputs]; subproof = DeleteCases[subproof, {_, x_ /; MemberQ[inputs, x], Given[]}, {1}]; mainproof = Join[mainproof, subproof]; Module[{f}, f[spacing*num] = spacing*(num + 1) - 1 ; MapThread[(f[x_ /; MemberQ[#1,x]]= #2)&, {givens, spacing*Last[just]}]; f[x_] = x; mainproof = transpose[mainproof]; mainproof = ReplacePart[mainproof,Map[(pass[f, #])&, last[mainproof]], 3] ]; mainproof = transpose[mainproof]; mainproof = RenumberProof[mainproof, 1, 1]; line= first[Cases[mainproof, {_,_,_Algorithm}, {1}]] ]; Protect[$AllowPatterns]; mainproof, Unprotect[$AllowPatterns]; $AllowPatterns = False; Protect[$AllowPatterns]; Message[FullProof::abort]; Abort[] ] ]; FullProof[x___] := (Message[FullProof::arguments]; Abort[]); ProofName[] := HoldForm[Null]; ProofName[x__] := (Message[ProofName::arguments]; Abort[]); LastLine[ x_List] := (validprooflist[x]; max[first[transpose[x]]]); LastLine[x___] := (Message[LastLine::arguments]; Abort[]); RemoveLine[num_] := (Message[General::protectedproof, HoldForm[Null]]; Abort[]); RemoveLine[x___] := (Message[RemoveLine::arguments]; Abort[]); RemoveLine[name_ , num_ /; wholeQ[num]] := ( checksymbol[name,RemoveLine]; If[Head[name] === Symbol, name = {} ]; validprooflist[name]; If[MemberQ[name, {num, _, _}], name = Sort[DeleteCases[name, {num, _, _}, {1}]], Message[General::noline, num] ]; lastproof[name]; name ); SetAttributes[RemoveLine, HoldFirst]; RenumberProof[x___] := (Message[RenumberProof::arguments]; Abort[]); RenumberProof[{}, start_ /; wholeQ[start], numstep_ /; wholeQ[numstep]] := {}; RenumberProof[proof_List, start_ /; wholeQ[start], numstep_ /; wholeQ[numstep]] := Module[{f,newjusts, newnums, nums, trans}, validprooflist[proof]; trans = Transpose[Sort[proof]]; nums = First[trans]; newnums = Range[start, start + numstep * (Length[nums] - 1), numstep]; MapThread[(f[#1]=#2)&, {nums, newnums}]; f[x_] := (Message[General::noline, x]; Abort[]); newjusts = Map[(pass[f,#])&, Last[trans]]; trans = ReplacePart[trans, newnums, 1]; trans = ReplacePart[trans, newjusts, 3]; Transpose[trans] ]; (* Section 4: Checking Proofs *) (* Section 4.1: Definitions *) $AllowPatterns::warning = "$AllowPatterns is not set to False. Some not-well-formed formulas may be \ misinterpreted as well-formed."; Algorithm::abort = "`1` has been aborted."; CheckProof::abort = "CheckProof has been aborted."; CheckProof::arguments = "CheckProof has improper arguments."; CheckProof::error = "An unexpected error has occurred during the evaluation of CheckProof."; CheckProof::invalid = "Line `1` of the proof is invalid."; CheckProof::options = "The options for CheckProof have improper values."; Options[CheckProof] = {DisplayProof->True, GivensList->{}, SymbolicForm->True}; (* Section 4.2: Local Functions *) algorithmQ[linesout_, just_, wff_] := Module[{proof, inputs, out, truth}, CheckAbort[ Which[ inputs = Map[(Cases[linesout, {#, g_, _} -> g, {1}])&, Last[just]]; inputs = Flatten[inputs]; Length[inputs]=!=Length[Last[just]], out = False, proof = Sort[Apply[First[just], inputs]]; Unprotect[$AllowPatterns]; $AllowPatterns = False; truth = CheckProof[proof, DisplayProof -> False, GivensList -> inputs]; !truth, out = False, ! MatchQ[last[proof], {_, wff, notgiven_} /; Head[notgiven]=!=Given], out = False, True, out =True ]; Unprotect[$AllowPatterns]; $AllowPatterns = True; out, Message[Algorithm::abort, just]; Abort[] ] ]; assume[givens_, symbolicform_] := Module[{formulas, n}, If[symbolicform, formulas = Map[tosymbolic, givens], formulas = Map[tostring, givens] ]; n = Length[formulas]; If[ n > 2, formulas = Flatten[Map[({#, ", "})&, formulas]]; formulas = formulas /. {a__, b_, ", ", c_, ", "} -> {a,b,c} ]; If[ n > 1, formulas = Insert[formulas, " and ", -2] ]; formulas = Join[{"Q.E.D. (assuming "}, formulas, {")"}]; broken[ StringJoin[formulas],Apply[Plus, $MaxColumnWidths] + 6] ]; checkproof[proof_, displayproof_ /; logicQ[displayproof], givens_List /; Apply[ And, Map[WffQ, givens]], symbolicform_ /; logicQ[symbolicform]] := Module[{axiom, currentline, just, linesin, linesout, num, out, qed, wff}, If[$AllowPatterns =!= False, Message[$AllowPatterns::warning]]; If[ proof==={}, Message[CheckProof::arguments]; Abort[] ]; validprooflist[proof]; linesin = Sort[proof]; linesout = {}; CheckAbort[ Unprotect[$AllowPatterns]; $AllowPatterns = True; qed = ""; While[ linesin =!= {}, currentline = First[linesin]; num = First[currentline]; wff = Part[currentline, 2]; just = Last[currentline]; If[ !wholeQ[num], Message[CheckProof::error]; Abort[]]; If[!MemberQ[$WffHeads,Head[wff]], Message[CheckProof::error]; Abort[]]; If[!MemberQ[$JustificationHeads, Head[just]], Message[CheckProof::error]; Abort[]]; Which[ Head[just]===Axiom, axiom = First[just]; If[!MatchQ[$AxiomList, {___, axiom, ___}], Message[$AxiomList::missing, axiom]; Message[CheckProof::invalid, num]; Abort[] ]; If[AxiomQ[axiom, wff]=!= True, Message[CheckProof::invalid, num]; Abort[]], Head[just]===Algorithm, If[! algorithmQ[linesout, just, wff], Message[CheckProof::invalid, num]; Abort[]], Head[just]===Given, If[!MemberQ[givens, wff], Message[CheckProof::invalid, num]; Abort[]], Head[just]===ModusPonens, If[!modusponensQ[linesout, Apply[List, just], wff], Message[CheckProof::invalid, num]; Abort[]], True, Message[CheckProof::error]; Abort[] ]; linesout = Append[linesout, currentline]; linesin = Drop[linesin, 1] ]; qed = "Q.E.D.", Message[CheckProof::abort] ]; Unprotect[$AllowPatterns]; $AllowPatterns = False; Protect[$AllowPatterns]; If[displayproof, If[ qed =!= "" & givens=!={}, qed= assume[givens, symbolicform] ]; out = DisplayProof[linesout, SymbolicForm->symbolicform]; out = Part[out, 1, 1]; out = GridBox[{{out}, {qed}}, ColumnAlignments -> Left]; out = StyleBox[out, AutoSpacing->False]; DisplayForm[out], If[qed==="", False,True] ] ]; checkproof[x___] := (Message[CheckProof::options]; Abort[]); free[x_String, wff_] := Which[ Head[wff]===ALL && First[wff]===x, {}, wff===x, x, Head[wff]===String, {}, True, Map[ free[x, #]&, Apply[List,wff]] ]; freeQ[x_String, wff_] := If[Union[Flatten[free[x,wff]]]==={x}, True, False]; modusponensQ[linesout_, {x_, y_}, wff_] := Module[{fx, fy}, If[MemberQ[first[transpose[linesout]], x] && MemberQ[first[transpose[linesout]], y], fx = Part[First[Cases[linesout, {x, _, _}, {1}]],2]; fy = Part[First[Cases[linesout, {y, _, _}, {1}]], 2]; fx === IMPLIES[fy, wff] || fy === IMPLIES[fx, wff], False] ]; removealls[wff_] := Module[{x}, x = wff; While[ Head[x]=== ALL, x = Part[x,2]]; x ]; replace[wff_, x_, t_] := ReplacePart[wff, t, Position[ free[x, wff], x]]; sub[x_, t_, wff_] := Which[ MemberQ[$AtomicHeads,Head[wff]], {True}, Head[wff] === ALL, Which[ !freeQ[x,wff], {True}, FreeQ[t,First[wff]], sub[x, t, Last[wff]], True, {False} ], True, Map[ sub[x, t, #]&, Apply[List,wff]] ]; subQ[x_,t_,wff_] := Apply[And,Flatten[sub[x, t, wff]]]; truthlist[n_] := Module[{i, l1, l2}, l1 = Table[i, {i, 0, 2^n - 1}]; l2 = Map[IntegerDigits[#,2,n]&, l1]; l2 /. {1 -> True, 0 -> False} ]; (* Section 4.3: Exported Functions *) AxiomQ["Ax. 1", wff_] := Module[{f, g, formula, logicalfunctions, logicalheads, propositions, rules, truthtable}, logicalheads = first[transpose[$Connectives]]; logicalfunctions = last[transpose[$Connectives]]; propositions = {}; f[x_] := Which[ MemberQ[logicalheads, Head[x]], Apply[ First[Extract[logicalfunctions, Position[logicalheads, Head[x]]]], x], MemberQ[logicalfunctions, Head[x]], Map[f, x], True, If[!MemberQ[propositions, x], propositions = Append[propositions,x] ]; x ]; formula = FixedPoint[f, removealls[wff]]; g[x_] := MapThread[Rule,{propositions, x}]; rules = Map[g, truthlist[Length[propositions]]]; truthtable = Map[(formula /. #)&, rules]; If[ Union[truthtable]==={True}, True, False] ]; AxiomQ["Ax. 2", wff_] := MatchQ[removealls[wff], IMPLIES[ALL[x_, a_], b_] /; MatchQ[b, replace[a, x, t_] /; subQ[x,t,a] ] ]; AxiomQ["Ax. 3", wff_] := MatchQ[removealls[wff], IMPLIES[ ALL[x_, IMPLIES[a_,b_]], IMPLIES[ALL[x_,a_], ALL[x_, b_]] ] ]; AxiomQ["Ax. 4", wff_] := MatchQ[removealls[wff], IMPLIES[a_, ALL[x_,a_]] /; !freeQ[x,a] ]; AxiomQ["Ax. 5", wff_] := MatchQ[removealls[wff], EQUAL[x_String,x_String]]; AxiomQ["Ax. 6", wff_] := MatchQ[removealls[wff], IMPLIES[EQUAL[x_String,y_String],IMPLIES[a_, b_]] /; MemberQ[$AtomicHeads, Head[a]] && MemberQ[$AtomicHeads, Head[b]] && MatchQ[b, a /. x -> _] && MatchQ[a, b /. y -> _] ]; AxiomQ["Empty Set Def.", wff_] := MatchQ[wff, ALL[x_, IFF[ EQUAL[x_,EMPTYSET[]], ALL[a_, NOT[MEMBER[a_,x_]]] ] ] /; StringQ[x] && StringQ[a] && x=!=a ]; AxiomQ["Intersection Def.", wff_] := MatchQ[wff, ALL[x_, ALL[y_, IFF[ EQUAL[x_, INTERSECTION[y_]], 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 ]; AxiomQ["Power Set Def.", wff_] := MatchQ[wff, ALL[x_, ALL[y_, IFF[ EQUAL[ x_, POWERSET[y_]], ALL[a_, IFF[ MEMBER[a_,x_], SUBSET[a_,y_] ] ] ] ] ] /; StringQ[x] && StringQ[y] && StringQ[a] && x=!=y=!=a ]; AxiomQ["Set Def.", wff_] := Module[{formula, variables, x, yn}, Which[ !MatchQ[wff, ALL[_, ALL[_, _]]], False, formula = wff; variables = {}; While[Head[formula]===ALL, variables = Append[variables, First[formula]]; formula = Last[formula] ]; ! MatchQ[variables, {y__String} /;UnsameQ[y]], False, x = First[variables]; variables = Rest[variables]; True, MatchQ[formula, IFF[ EQUAL[x,Apply[SET, variables]], ALL[a_, IFF[ MEMBER[a_, x], ors_ ] ] ] /; StringQ[a] && (! MemberQ[Prepend[variables, x],a]) && Flatten[ReplaceRepeated[{ors}, OR[u_,v_] -> {u, v}]]=== Map[(EQUAL[a, #])&, variables] ] ] ]; AxiomQ["Subset Def.", wff_] := MatchQ[ wff, ALL[x_, ALL[y_, IFF[ SUBSET[x_, y_], ALL[a_, IMPLIES[MEMBER[a_,x_], MEMBER[a_,y_]]] ] ] ] /; StringQ[x] && StringQ[y] && StringQ[a] && x=!=y=!=a ]; AxiomQ["Union Def.", wff_] := MatchQ[wff, ALL[x_, ALL[y_, IFF[ EQUAL[x_, UNION[y_]], ALL[a_, IFF[ MEMBER[a_,x_], NOT[ ALL[b_, NOT[ AND[ MEMBER[b_,y_], MEMBER[a_,b_] ] ] ] ] ] ] ] ] ] /; StringQ[x] && StringQ[y] && StringQ[a] && StringQ[b] && x=!=y=!=a && b=!=y=!=a ]; AxiomQ["Choice Ax.", wff_] := MatchQ[ wff, ALL[x_, IMPLIES[ AND[ ALL[a_, IMPLIES[ MEMBER[a_,x_], NOT[EQUAL[a_,EMPTYSET[]]] ] ], ALL[b_, ALL[c_, IMPLIES[ Alternatives[ AND[ MEMBER[b_,x_], AND[ MEMBER[c_,x_], NOT[EQUAL[b_,c_]] ] ] , AND[ AND[ MEMBER[b_, x_], MEMBER[c_, x_] ], NOT[EQUAL[b_,c_]] ] ], EQUAL[INTERSECTION[SET[b_,c_]], EMPTYSET[]] ] ] ] ], NOT[ ALL[s_, NOT[ ALL[d_, IMPLIES[ MEMBER[d_,x_], NOT[ ALL[e_, NOT[ EQUAL[INTERSECTION[SET[s_,d_]],SET[e_]] ] ] ] ] ] ] ] ] ] ] /; StringQ[x] && StringQ[a] && StringQ[b] && StringQ[c] && StringQ[d] && StringQ[e] && StringQ[s] && x=!=a && x=!=b=!=c&& x=!=s=!=d && e=!=s=!=d ]; AxiomQ["Empty Set Ax.", wff_] := MatchQ[wff, NOT[ ALL[s_, NOT[ EQUAL[s_, EMPTYSET[]] ] ] ] /; StringQ[s] ]; AxiomQ["Extensionality Ax.", wff_] := MatchQ[ wff, ALL[x_, ALL[y_, IMPLIES[ ALL[a_, IFF[ MEMBER[a_,x_], MEMBER[a_,y_] ] ], EQUAL[x_,y_] ] ] ] /; StringQ[x] && StringQ[y] && StringQ[a] &&x=!=y=!=a ]; AxiomQ["Infinity Ax.", wff_] := MatchQ[wff, NOT[ ALL[s_, NOT[ AND[ MEMBER[EMPTYSET[],s_], ALL[a_, IMPLIES[ MEMBER[a_,s_], MEMBER[SET[a_],s_] ] ] ] ] ] ] /; StringQ[s] && StringQ[a] && s=!=a ]; AxiomQ["Pairing Ax.", wff_] := MatchQ[wff, ALL[x_, ALL[y_, NOT[ ALL[s_, NOT[ EQUAL[s_, SET[x_,y_]] ] ] ] ] ] /; StringQ[x] && StringQ[y] && StringQ[s] && x=!=y=!=s ]; AxiomQ["Power Set Ax.", wff_] := MatchQ[wff, ALL[x_, NOT[ ALL[s_, NOT[ EQUAL[s_, POWERSET[x_]] ] ] ] ] /; StringQ[x] && StringQ[s] && x=!=s ]; AxiomQ["Regularity Ax.", wff_] := MatchQ[ wff, ALL[x_, IMPLIES[ NOT[ EQUAL[x_,EMPTYSET[]] ], NOT[ ALL[s_, NOT[ AND[ MEMBER[s_,x_], EQUAL[INTERSECTION[SET[s_,x_]], EMPTYSET[]] ] ] ] ] ] ] /; StringQ[x] && StringQ[s] && x=!=s ]; AxiomQ["Replacement Ax.", wff_] := Module[{formula, variables, x}, Which[ !MatchQ[wff, ALL[_, _]], False, formula = wff; variables = {}; While[Head[formula]===ALL, variables = Append[variables, First[formula]]; formula = Last[formula] ]; ! MatchQ[variables, {__String}], False, True, x = Last[variables]; MatchQ[ formula, IMPLIES[ ALL[a_, IMPLIES[ MEMBER[a_,x], ALL[b_, ALL[c_, IMPLIES[ AND[ f_, g_ ], EQUAL[b_,c_] ] ] ] ] ], NOT[ ALL[s_, NOT[ ALL[d_, IFF[ MEMBER[d_,s_], NOT[ ALL[e_, NOT[ AND[ MEMBER[e_,x], h_ ] ] ] ] ] ] ] ] ] ] /; StringQ[a] && StringQ[b] && StringQ[c] && StringQ[d] && StringQ[e] && StringQ[s] && a=!=b=!=c && a=!=x && s=!=d=!=x && e=!=d=!=x && WffQ[f] && WffQ[g] && WffQ[h] && Implies[e=!=s, !freeQ[s, h]] && subQ[e,a,h] && subQ[d, b, h] && subQ[b, c, f] && subQ[a, e, g] && subQ[c, d, g] && f=== replace[replace[h, e, a], d, b] && g === replace[f, b, c] && h === replace[ replace[g, a, e], c, d] ] ] ]; AxiomQ["Subset Ax.", wff_] := Module[{formula, variables, x}, Which[ !MatchQ[wff, ALL[_, _]], False, formula = wff; variables = {}; While[Head[formula]===ALL, variables = Append[variables, First[formula]]; formula = Last[formula] ]; ! MatchQ[variables, {__String}], False, True, x = Last[variables]; MatchQ[ formula, NOT[ ALL[ s_, NOT[ ALL[a_, IFF[ MEMBER[a_,s_], AND[ MEMBER[a_,x], f_ ] ] ] ] ] ] /; StringQ[s] && StringQ[a] && WffQ[f] && (! freeQ[s, f]) && x=!= s=!=a ] ] ]; AxiomQ["Union Ax.", wff_] := MatchQ[wff, ALL[ x_, NOT[ ALL[s_, NOT[ EQUAL[s_, UNION[x_]] ] ] ] ] /; StringQ[x] && StringQ[s]&& x=!=s ]; CheckProof[proof_, options___Rule] := checkproof[proof, DisplayProof /. {options} /. Options[CheckProof], GivensList /. {options} /. Options[CheckProof], SymbolicForm /. {options} /. Options[CheckProof]]; CheckProof[x___] := (Message[CheckProof::arguments]; Abort[]); End[]; Protect[$AllowPatterns, $AtomicHeads, $AxiomList, $Connectives, $LineBreakStrings, $MaxColumnWidths, $JustificationHeads, $PatternHeads, $TermHeads, $TranslationList, $WffHeads, AddLine, Algorithm, ALL, AND, Axiom, AxiomQ, CheckProof, DisplayProof, EMPTYSET, EQUAL, FullProof, Given, GivensList, Iff, IFF, IMPLIES, INTERSECTION, LastLine, MEMBER, ModusPonens, NonCommutativeMultiply, NOT, OR, POWERSET, ProofName, RemoveLine, RenumberProof, SET, SUBSET, SymbolicForm, TermQ, UNION, WffQ]; EndPackage[]