TOC of Theorem List - bfol.mm Proof Explorer

Table of Contents Summary

PART 1  Chapter 0: Primitives
      1.1  Definition of Term
      1.2  Definition of WFF
      1.3  First Order Logic Axioms
PART 2  Chapter 1: Propositional Calculus (Primitive Connectives)
      2.1  Logical Implication
      2.2  Logical Negation
PART 3  Chapter 2: Propositional Calculus (Defined Connectives)
      3.1  Development.
      3.2  Logical Equivalence
      3.3  Logical Conjunction
      3.4  Logical Disjunction
      3.5  True and False Constants.
PART 4  Chapter 3: Propositional Calculus (Natural Deduction)
      4.1  Define Conjunction Tuples.
      4.2  Natural Deduction for Propositional Calculus.
      4.3  Revisiting Chapter 1.
      4.4  Revisiting Chapter 2.
PART 5  Chapter 4: Propositional Calculus (continued)
      5.1  More Useful Rules.
      5.2  Logical Equivalencies.
      5.3  Peirce's Law.
      5.4  Appendix: Miscellaneous Utility Rules.
PART 6  Chapter 5: Predicate Calculus (FOL Axioms)
      6.1  Consequences of ax-GEN and ax-L4.
      6.2  Consequences of ax-L5.
      6.3  Consequences of Axioms Involving Equality ( ax-L6 - ax-L9 ).
      6.4  Implicit Variable Substitution and Law of Specialization.
      6.5  Quantifier Collection Laws.
PART 7  Chapter 6: Predicate Calculus (Definitions and ax-L10 - ax-L12).
      7.1  Effective Non-Freeness.
      7.2  Explicit Substitution.
      7.3  Scheme Completion Axiom ax-L12.
      7.4  Scheme Completion Axioms ax-L10 and ax-L11.
      7.5  Replacing Variable Restrictions with Non-Freeness Conditions.
      7.6  More on Proper Substitution.
      7.7  Deductive Forms.
PART 8  Chapter 7: Predicate Calculus (Natural Deduction)
      8.1  Natural Deduction for Predicate Calculus.
      8.2  Recovering Hilbert Axioms and Definitions.
      8.3  Revisiting Chapter 5.
      8.4  Examples.
PART 9  Chapter 8: Predicate Calculus (Continued)
      9.1  Revisiting Chapter 6.
      9.2  More Quantifier Laws.

Detailed Table of Contents
(* means the section header has a description)

​PART 1  Chapter 0: Primitives
      ​1.1  Definition of Term
      ​1.2  Definition of WFF
      ​1.3  First Order Logic Axioms
            1.3.1  Axioms of Propositional Calculus   ax-L1 11
            1.3.2  Axioms of Predicate Calculus   ax-GEN 15
                  1.3.2.1  Equality Axioms   ax-L6 18
            1.3.3  Substitution Axioms.   ax-L8-inl 20
                  1.3.3.1  Primitive Predicate Substitution Axioms.   ax-L8-inl 20
                  1.3.3.2  Primitive Function Substitution Axioms.   ax-L9-succ 22
            1.3.4  Scheme Completion Axioms.   ax-L10 27
​PART 2  Chapter 1: Propositional Calculus (Primitive Connectives)
      ​2.1  Logical Implication
            ​*2.1.1  Some Simple Proofs.   axL1.SH 30
            2.1.2  Some Derived Inferences.   mae-P1.1 33
            2.1.3  First Closed Form Theorems.   id-P1.4 36
            2.1.4  Proof Recipes.   rcp-FR1 39
                  ​*2.1.4.1  Application of Proof Recipes.   axL1.AC.SH 45
            2.1.5  More Implication Theorems.   imcomm-P1.6 48
      ​2.2  Logical Negation
            2.2.1  Basic Negation Laws.   poe-P1.11a 65
            2.2.2  Transposition Laws.   trnsp-P1.15a 76
            2.2.3  Classical Arguments.   pfbycont-P1.16 86
​PART 3  Chapter 2: Propositional Calculus (Defined Connectives)
      ​​*3.1  Development.
      ​3.2  Logical Equivalence
            ​*3.2.1  Motivation Theorems.   mbifwd-P2.1a 101
            ​*3.2.2  Defining Logical Equivalence.   wff-bi 104
                  3.2.2.1  Syntax Definition.   wff-bi 104
                  ​*3.2.2.2  Justification Theorem.   bijust-P2.2-L1 105
                  3.2.2.3  Formal Definition.   df-bi-D2.1 107
                  ​*3.2.2.4  Standard Form.   dfbiif-P2.3a 108
            ​*3.2.3  Fundamental Properties.   bifwd-P2.5a 111
            ​*3.2.4  Equivalence Relation Properties.   biref-P2.6a 123
            ​*3.2.5  Substitution Laws.   subneg-P2.7 127
      ​3.3  Logical Conjunction
            3.3.1  Defining Logical Conjunction.   wff-and 132
                  3.3.1.1  Syntax Definition.   wff-and 132
                  3.3.1.2  Formal Definition.   df-and-D2.2 133
            ​*3.3.2  Fundamental Properties.   simpl-P2.9a 134
            3.3.3  Importation and Exportation Laws.   import-P2.10a 140
      ​3.4  Logical Disjunction
            3.4.1  Defining Logical Disjunction.   wff-or 144
                  3.4.1.1  Syntax Definition.   wff-or 144
                  3.4.1.2  Formal Definition.   df-or-D2.3 145
            ​*3.4.2  Fundamental Properties.   orintl-P2.11a 146
            3.4.3  The Law of Excluded Middle.   exclmid-P2.12 152
      ​3.5  True and False Constants.
            3.5.1  Defining True.   wff-true 153
                  3.5.1.1  Syntax Definition.   wff-true 153
                  3.5.1.2  Justification Theorem.   truejust-P2.13 154
                  3.5.1.3  Formal Definition.   df-true-D2.4 155
            3.5.2  Fundamental Property of "True" Constant.   true-P2.14 156
            3.5.3  Defining False.   wff-false 157
                  3.5.3.1  Syntax Definition.   wff-false 157
                  3.5.3.2  Formal Definition.   df-false-D2.5 158
            3.5.4  Fundamental Property of "False" Constant.   false-P2.15 159
​PART 4  Chapter 3: Propositional Calculus (Natural Deduction)
      ​4.1  Define Conjunction Tuples.
      ​​*4.2  Natural Deduction for Propositional Calculus.
            4.2.1  Axiomatic Rules.   ndasm-P3.1 166
                  4.2.1.1  Rules for "True" and "False" Constants.   ndtruei-P3.17 182
                  ​*4.2.1.2  Separate Front Supposition (Syntactic Axioms).   rcp-NDSEP3 186
                  ​*4.2.1.3  Join Front Supposition (Syntactic Axioms).   rcp-NDJOIN3 189
            ​*4.2.2  Utility Recipes.   rcp-NDASM1of1 192
                  *4.2.2.1  Derived Rules for Stating / Re-Stating Assumptions.   rcp-NDASM1of1 192
                  ​*4.2.2.2  Derived Rules for Importing Previous Results.   rcp-NDIMP0addall 207
                  ​*4.2.2.3  Derived Rules for Negation Introduction.   rcp-NDNEGI1 218
                  ​*4.2.2.4  Derived Rule for Negation Elimination.   rcp-NDNEGE0 223
                  ​*4.2.2.5  Derived Rules for Implication Introduction.   rcp-NDIMI2 224
                  ​*4.2.2.6  Derived Rule for Implication Elimination.   rcp-NDIME0 228
                  ​*4.2.2.7  Derived Rule for Conjunction Introduction.   rcp-NDANDI0 229
                  ​*4.2.2.8  Derived Rule for Left Conjunction Elimination.   rcp-NDANDEL0 230
                  ​*4.2.2.9  Derived Rule for Right Conjunction Elimination.   rcp-NDANDER0 231
                  ​*4.2.2.10  Derived Rule for Left Disjunction Introduction.   rcp-NDORIL0 232
                  ​*4.2.2.11  Derived Rule for Right Disjunction Introduction.   rcp-NDORIR0 233
                  ​*4.2.2.12  Derived Rules for Disjunction Elimination   rcp-NDORE1 234
                  ​*4.2.2.13  Derived Rule for Biconditional Introduction.   rcp-NDBII0 239
                  ​*4.2.2.14  Derived Rule for Biconditional Forward Implication.   rcp-NDBIEF0 240
                  ​*4.2.2.15  Derived Rule for Biconditional Reverse Implication.   rcp-NDBIER0 241
            ​*4.2.3  Closed Forms of Natural Deduction Rules.   ndnegi-P3.3.CL 242
            4.2.4  A More Convenient form of Law of Excluded Middle.   ndexclmid-P3.16.AC 251
      ​4.3  Revisiting Chapter 1.
            4.3.1  Propositional Axioms L1 and L2.   axL1-P3.21 252
            4.3.2  Other Implication Laws.   mae-P3.23 257
            4.3.3  Double Negation Laws.   dnegi-P3.29 273
            4.3.4  Transposition Laws (including Axiom L3).   trnsp-P3.31a 279
            4.3.5  Other Laws Involving Negation.   mt-P3.32a 291
      ​4.4  Revisiting Chapter 2.
            4.4.1  Biconditional Equivalence Properties.   biref-P3.33a 297
            ​*4.4.2  Importation and Exportation Laws.   import-P3.34a 305
                  4.4.2.1  Examples.   example-E3.1a 309
            4.4.3  Commutative and Associative Properties.   andcomm-P3.35-L1 313
            ​*4.4.4  Substitution Laws.   subneg-P3.39 323
            4.4.5  Theorems for "True" and "False" Constants.   true-P3.44 352
            ​*4.4.6  Re-deriving Chapter 2 Definitions.   andasim-P3.46-L1 354
​PART 5  Chapter 4: Propositional Calculus (continued)
      ​5.1  More Useful Rules.
            5.1.1  Law of Non-contradiction.   ncontra-P4.1 366
            5.1.2  Dual Forms of Introduction and Elimination Rules.   norel-P4.2a 367
            5.1.3  Other Forms of the Principle Of Explosion.   impoe-P4.4a 377
            5.1.4  Process of Elimination.   profeliml-P4.5a 385
            5.1.5  Joining Implications.   joinimandinc-P4.8a 397
            5.1.6  Separating Implications.   sepimandr-P4.9a 406
            5.1.7  Some Double Negation Laws.   dnegeq-P4.10 418
            5.1.8  Extended Syllogism and Transitivity Laws.   tsyl-P4.15 426
            ​*5.1.9  Negation Introduction Using "False" Constant.   falsenegi-P4.18 432
                  5.1.9.1  Rule.   falsenegi-P4.18 432
                  ​*5.1.9.2  Scheme.   rcp-FALSENEGI1 433
      ​5.2  Logical Equivalencies.
            5.2.1  Identity Laws for Conjunction and Disjunction.   idandtruel-P4.19a 438
            5.2.2  More Equivalence Laws Involving "True" and "False".   thmeqtrue-P4.21a 442
            5.2.3  Identity Laws Involving Theorems.   idandthml-P4.23a 446
            5.2.4  Idempotency Laws.   idempotand-P4.25a 450
            5.2.5  De Morgan's Laws.   dmorgafwd-L4.1 452
                  5.2.5.1  Parts of De Morgan's Laws.   dmorgafwd-L4.1 452
                  5.2.5.2  De Morgan's Laws.   dmorga-P4.26a 456
            5.2.6  Distributive Laws.   andoveror-P4.27-L1 459
                  5.2.6.1  Conjunction and Disjunction.   andoveror-P4.27-L1 459
                  5.2.6.2  Left Implication.   imoverand-P4.29a 472
            5.2.7  Antidistributive Laws.   rimoverand-P4.31-L1 480
            5.2.8  More Useful Logical Equivalencies.   lemma-L4.5 484
            5.2.9  Truth Tables.   truthtblnegt-P4.35a 493
                  5.2.9.1  Negation.   truthtblnegt-P4.35a 493
                  5.2.9.2  Implication.   truthtbltimt-P4.36a 495
                  5.2.9.3  Conjunction.   truthtbltandt-P4.37a 499
                  5.2.9.4  Disjunction.   truthtbltort-P4.38a 503
                  5.2.9.5  Equivalence.   truthtbltbit-P4.39a 507
      ​5.3  Peirce's Law.
            5.3.1  Classical Proof.   peirce-P4.40 511
            5.3.2  Equivalence of Peirce's Law and Law of Excluded Middle.   exclmid2peirce-P4.41a 512
      ​5.4  Appendix: Miscellaneous Utility Rules.
            ​*5.4.1  Reductio ad Absurdum.   raa-P4 514
                  5.4.1.1  Rule.   raa-P4 514
                  ​*5.4.1.2  Scheme.   rcp-RAA1 515
            5.4.2  Reductio ad Absurdum Using "False" Constant.   falseraa-P4 520
                  5.4.2.1  Rule.   falseraa-P4 520
                  ​*5.4.2.2  Scheme.   rcp-FALSERAA1 521
            5.4.3  Convert Implication to Assumption.   impime-P4 526
                  5.4.3.1  Rule.   impime-P4 526
                  ​*5.4.3.2  Scheme.   rcp-IMPIME1 527
            5.4.4  Combine Biconditional Elimination with Modus Ponens.   bimpf-P4 531
            5.4.5  Transposition Laws as Equivalence Laws.   trnspeq-P4a 535
            5.4.6  Different Form for Substitution Laws.   subneg2-P4 538
            5.4.7  More Convenient Forms for Commutivity Laws.   andcomm2-P4 564
            5.4.8  More Convenient Forms for Associativity Laws.   andassoc2a-P4 568
            5.4.9  More Convenient Forms for Joining Implications.   joinimandinc2-P4 576
​PART 6  Chapter 5: Predicate Calculus (FOL Axioms)
      ​6.1  Consequences of ax-GEN and ax-L4.
            6.1.1  The Universal Quantifier.   alloverim-P5 588
                  6.1.1.1  Generalization Augmentation.   alloverim-P5.RC.GEN 592
                  6.1.1.2  A Substitution Law for Universal Quantification.   suballinf-P5 594
            6.1.2  The Existential Quantifier.   wff-exists 595
                  6.1.2.1  Syntax Definition.   wff-exists 595
                  6.1.2.2  Formal Definition.   df-exists-D5.1 596
            6.1.3  Dual Properties of Universal / Existential Quantification.   allnegex-P5 597
            6.1.4  More Quantifier Laws.   alloverimex-P5 601
                  6.1.4.1  A Substitution Law for Existential Quantification.   subexinf-P5 608
            6.1.5  Quantified Implication Equivalence Laws.   qimeqallhalf-P5 609
      ​6.2  Consequences of ax-L5.
            6.2.1  Generalization Augmentation with Context.   alloverim-P5.GENV 621
            6.2.2  Substitution Laws for Quantifiers.   suballv-P5 623
      ​6.3  Consequences of Axioms Involving Equality ( ax-L6 - ax-L9 ).
            ​*6.3.1  Equivalence Properties of Equality Predicate.   eqref-P5 626
            6.3.2  More Substitution Laws.   subeql-P5 632
                  6.3.2.1  Substitution Laws for Equality.   subeql-P5 632
                  6.3.2.2  Substitution Laws for Primitive Predicate.   subelofl-P5 638
                  6.3.2.3  Substitution Laws for Functions.   subsucc-P5 644
      ​6.4  Implicit Variable Substitution and Law of Specialization.
            6.4.1  Preliminary Law of Specialization.   lemma-L5.02a 653
            6.4.2  Quantifier Removal Laws.   qremallv-P5 656
            6.4.3  Change of Bound Variables Laws.   cbvallv-P5-L1 658
            6.4.4  Weakened Law of Specialization.   specw-P5 661
                  6.4.4.1  Hypothesis Elimination Examples.   example-E5.01a 663
            6.4.5  Commutivity of Similar Quantifiers (weakened versions).   lemma-L5.03a 666
      ​​*6.5  Quantifier Collection Laws.
                  6.5.0.1  Prenex Form Example.   example-E5.04a 675
​PART 7  Chapter 6: Predicate Calculus (Definitions and ax-L10 - ax-L12).
      ​7.1  Effective Non-Freeness.
            ​*7.1.1  The "General For" Concept.   genallw-P6 676
                  7.1.1.1  Positive.   genallw-P6 676
                  7.1.1.2  Negated.   gennallw-P6 678
                  7.1.1.3  Dual.   exgenallw-P6 680
            7.1.2  Define Effective Non-Freeness.   wff-nfree 681
                  7.1.2.1  Syntax Definition.   wff-nfree 681
                  7.1.2.2  Formal Definition.   df-nfree-D6.1 682
            ​*7.1.3  Equivalencies.   dfnfreealt-P6 683
            ​*7.1.4  Relationship to Textbook Definition.   nfrv-P6 686
            7.1.5  More Consequences of Effective Non-Freeness.   nfrexgenw-P6 696
      ​7.2  Explicit Substitution.
            7.2.1  Motivation.   solvesub-P6a 704
            7.2.2  Define Proper Substitution.   wff-psub 714
                  7.2.2.1  Syntax Definition.   wff-psub 714
                  7.2.2.2  Justification Theorem.   psubjust-P6 715
                  7.2.2.3  Formal Definition.   df-psub-D6.2 716
            7.2.3  Simplified Definition.   dfpsubv-P6 717
      ​​*7.3  Scheme Completion Axiom ax-L12.
            7.3.1  Existential Quantifier Introduction and Specialization Revisited.   exi-P6 718
                  *7.3.1.1  Basic Forms.   exi-P6 718
                  ​*7.3.1.2  Traditional Textbook Forms.   exipsub-P6 720
            7.3.2  Strengthened Quantifier Removal Laws.   qremall-P6 722
            ​*7.3.3  Implicit / Explicit Substitution Conversion.   lemma-L6.01a 724
      ​7.4  Scheme Completion Axioms ax-L10 and ax-L11.
            ​*7.4.1  Strengthened "General For" Laws (first half).   gennall-P6 730
            ​*7.4.2  Strengthened "General For" / "Not Free" Conversion Laws.   nfrgen-P6 733
            ​*7.4.3  Strengthened "General For" Laws (second half).   genall-P6 737
            ​*7.4.4  Strengthened Quantifier Commutivity Laws.   allcomm-P6 739
            ​*7.4.5  Strengthened Effective Non-Freeness Properties.   nfrall1-P6 741
      ​7.5  Replacing Variable Restrictions with Non-Freeness Conditions.
            7.5.1  Basic Quantifier Rules with Non-Freeness Conditions.   allic-P6 745
            7.5.2  Change of Bound Variables Laws with Non-Freeness Conditions.   lemma-L6.04a 749
            7.5.3  (Implicit) Substitution Laws with Non-Freeness Conditions.   suball-P6 753
            7.5.4  Quantifier Collection Laws with Non-Freeness Conditions.   qcallimr-P6 757
      ​7.6  More on Proper Substitution.
            ​*7.6.1  Explicit to Implicit Substitution Conversion.   trnsvsub-P6 763
            7.6.2  Change of Bound Variable Using Proper Substitution.   cbvallpsub-P6 768
            7.6.3  An Alternate Definition of Proper Substitution.   lemma-L6.07a-L1 770
            7.6.4  Separating Atomic WFF Terms.   spliteq-P6-L1 775
                  7.6.4.1  Split Equality.   spliteq-P6-L1 775
                  7.6.4.2  Split Primitive Predicate.   splitelof-P6-L1 777
                  7.6.4.3  Effective Non-Freeness Over Terms.   nfrterm-P6 779
            ​*7.6.5  Relationship to Textbook Definition.   psubleq-P6 783
                  7.6.5.1  Proper Substitution Applied to Atomic Formulae.   psubspliteq-P6 800
                  7.6.5.2  Proper Substitution Applied to Atomic Terms.   psubvar1-P6 802
                  7.6.5.3  Proper Substitution Applied to Terms with Functions.   psubsuccv-P6-L1 805
      ​7.7  Deductive Forms.
            7.7.1  Some Lemmas.   nfrgencl-L6 811
            7.7.2  Effective Non-Freeness.   nfrimd-P6 815
            7.7.3  Universal Quantifier Introduction.   ndalli-P6 822
            7.7.4  Exestential Quantifier Elimination.   qremexd-P6 823
​PART 8  Chapter 7: Predicate Calculus (Natural Deduction)
      ​8.1  Natural Deduction for Predicate Calculus.
            8.1.1  Axiomatic Rules.   ndnfrv-P7.1 826
                  ​*8.1.1.1  Effective Non-Freeness Rules.   ndnfrv-P7.1 826
                  ​*8.1.1.2  Proper Substitution Rules.   ndpsub1-P7.13 838
                  ​*8.1.1.3  Quantifier Rules.   ndalli-P7.17 842
                  ​*8.1.1.4  Equality Introduction Axiom.   ndeqi-P7.21 846
                  ​*8.1.1.5  Substitution Rules (Equality Elimination).   ndsubeql-P7.22a 847
            ​*8.1.2  Derived Utility Rules.   ndsubeqd-P7 856
                  8.1.2.1  Dual Substitution Rules.   ndsubeqd-P7 856
                  8.1.2.2  Restricted Variable Forms of Natural Deduction Rules.   ndnfrall2-P7.9.VR12of2 860
                  8.1.2.3  Inference Forms of Natural Deduction Rules.   ndnfrneg-P7.2.RC 875
                  8.1.2.4  Closed Forms of Natural Deduction Rules.   ndnfrneg-P7.2.CL 904
      ​8.2  Recovering Hilbert Axioms and Definitions.
            8.2.1  Axiom L6 (Existential Form).   lemma-L7.01a 924
                  8.2.1.1  Recovered Axiom L6 (Existential Form).   axL6ex-P7 925
            8.2.2  Generalization Rule and Axiom L5.   nfrthm-P7 926
                  8.2.2.1  Recovered Generalization Rule.   axGEN-P7 933
                  8.2.2.2  Recovered Axiom L5.   axL5-P7 934
            8.2.3  Axiom L4.   eqsym-P7 936
                  8.2.3.1  Recovered Axiom L4.   axL4-P7 945
            8.2.4  Existential Quantifier   alli-P7 947
                  ​*8.2.4.1  Recovered Existential Quantifier Definition.   dfexists-P7 959
                  ​*8.2.4.2  Recovered Axiom L6 (Original Form).   axL6-P7 961
            8.2.5  Effective Non-Freeness.   lemma-L7.03 962
                  8.2.5.1  Recovered Alternate ENF Definition.   dfnfreealt-P7 967
                  ​*8.2.5.2  Recovered ENF Definition.   dfnfree-P7 968
            8.2.6  Proper Substitution.   alloverim-P7 970
                  8.2.6.1  Recovered Simplified Proper Substitution Definition.   dfpsubv-P7 977
                  8.2.6.2  Recovered Full Proper Substitution Definition.   dfpsub-P7 978
            8.2.7  Scheme Completion Axioms.   axL10-P7 979
                  8.2.7.1  Recovered Axiom L10.   axL10-P7 979
                  8.2.7.2  Recovered Axiom L11.   axL11-P7 980
                  8.2.7.3  Recovered Axiom L12.   axL12-P7 982
      ​8.3  Revisiting Chapter 5.
            ​*8.3.1  Equivalence Properties of Equality Predicate.   eqsym-P7r 983
            8.3.2  Simplified Quantifier Introduction / Elimination Rules.   alli-P7r 990
                  8.3.2.1  alle-P7 and exi-P7 Combined.   alleexi-P7 1004
                  8.3.2.2  Variants of alli-P7 and exe-P7.   allic-P7 1007
            8.3.3  Distributive Laws Producing Universal Quantifiers.   alloverim-P7r 1017
            8.3.4  Distributive Laws Producing Existential Quantifiers.   alloverimex-P7r 1028
            8.3.5  Quantifier Substitution Laws.   suball-P7r 1039
            ​*8.3.6  Dual Properties of Universal / Existential Quantification.   allnegex-P7r 1045
            8.3.7  Quantified Implication Equivalence Laws.   qimeqallhalf-P7r 1049
            8.3.8  Quantifier Commutivity Laws.   allcomm-P7 1058
            8.3.9  Change of Bound Variable Laws.   cbvall-P7-L1 1060
                  8.3.9.1  Proper Substitution Variants of cbvall-P7 and cbvex-P7.   cbvallpsub-P7 1070
      ​8.4  Examples.
            8.4.1  Conditional Non-Freeness Does Not Always Imply Effective Non-Freeness.   example-E7.1a 1074
​PART 9  Chapter 8: Predicate Calculus (Continued)
      ​9.1  Revisiting Chapter 6.
            9.1.1  "General For" / "Not Free" Conversion.   nfrgen-P8 1076
                  9.1.1.1  Standard Forms.   nfrgen-P8 1076
                  9.1.1.2  Dual Forms.   nfrexgen-P8 1080
                  9.1.1.3  Combined Forms.   nfrexall-P8 1086
            9.1.2  Nested Quantifier Idempotency Laws.   idempotall-P8 1093
            9.1.3  Quantifier Removal / Swapping Laws.   qremall-P8 1101
            9.1.4  Other Effective Non-Freeness Properties.   nfrthm-P8 1107
            9.1.5  Define Effective Non-Freeness Within a Term.   wff-nfreet 1114
                  9.1.5.1  Syntax Definition.   wff-nfreet 1114
                  9.1.5.2  Justification Theorem.   nfreetjust-P8 1115
                  9.1.5.3  Formal Definition.   df-nfreet-D8.1 1116
            9.1.6  Effective Non-Freeness Over Atomic Terms.   nfrzero-P8 1117
            9.1.7  Effective Non-Freeness Over Functional Terms.   nfrsucc-P8 1119
      ​9.2  More Quantifier Laws.
            9.2.1  Quantifier Collection Laws.   qcallimr-P8 1122
                  9.2.1.1  Implication.   qcallimr-P8 1122