HomeHome Intuitionistic Logic Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page:  Detailed Table of Contents  Page List

Table of Contents Summary
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Predicate calculus mostly without distinct variables
      1.4  Predicate calculus with distinct variables
PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
PART 3  CLASSICAL LOGIC
      3.1  Classical (not intuitionistic) results

Detailed Table of Contents
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
            1.1.1  Inferences for assisting proof development   dummylink 1
      1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            1.2.2  Propositional logic axioms for implication   ax-1 5
            1.2.3  Logical implication   mp2b 8
            1.2.4  Logical conjunction and logical equivalence   wa 95
            1.2.5  Logical negation (intuitionistic)   ax-in1 527
            1.2.6  Logical disjunction   wo 609
            1.2.7  Decidable propositions   wdc 718
            1.2.8  Theorems of decidable propositions   condc 724
            1.2.9  Miscellaneous theorems of propositional calculus   pm5.21nd 791
            1.2.10  Abbreviated conjunction and disjunction of three wff's   w3o 846
            1.2.11  True and false constants   wtru 1192
            1.2.12  Logical 'xor'   wxo 1211
            1.2.13  Operations on true and false constants   truantru 1229
            1.2.14  Stoic logic indemonstrables (Chrysippus of Soli)   mpto1 1251
            1.2.15  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1   ee22 1255
      1.3  Predicate calculus mostly without distinct variables
            1.3.1  Equality-free predicate calculus axioms ax-5, ax-7, ax-gen   wal 1271
            1.3.2  Introduce equality axioms   cv 1328
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1356
            1.3.4  Introduce Axiom of Existence   ax-i9 1360
            1.3.5  Additional intuitionistic axioms   ax-ial 1365
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1367
            1.3.7  The existential quantifier   19.8a 1417
            1.3.8  Equality theorems without distinct variables   a9e 1506
            1.3.9  Axioms ax-10 and ax-11   ax10o 1521
            1.3.10  Substitution (without distinct variables)   wsbc 1563
            1.3.11  Theorems using axiom ax-11   equs5a 1593
      1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1610
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1621
            1.4.3  More theorems related to ax-11 and substitution   albidv 1623
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1655
            1.4.5  More substitution theorems   hbs1 1727
            1.4.6  Existential uniqueness   weu 1812
PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
            2.1.1  Introduce the Axiom of Extensionality   ax-ext 1906
            2.1.2  Class abstractions (a.k.a. class builders)   cab 1909
            2.1.3  Class form not-free predicate   wnfc 2046
            2.1.4  Negated equality and membership   wne 2085
                  2.1.4.1  Negated equality   nnedc 2089
                  2.1.4.2  Negated membership   neleq1 2170
            2.1.5  Restricted quantification   wral 2175
            2.1.6  The universal class   cvv 2418
            2.1.7  Conditional equality (experimental)   wcdeq 2604
            2.1.8  Russell's Paradox   ru 2620
PART 3  CLASSICAL LOGIC
            3.0.1  Classical logic theorems   ax-3 2621
            3.0.2  Existential uniqueness (supplemental)   mo 2656
      3.1  Classical (not intuitionistic) results
            3.1.1  Additional substitution theorems (classical)   dfsb2 2691
            3.1.2  Exclusive or and related theorems (classical)   xordi 2693

    < Wrap  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2693
  Copyright terms: Public domain < Wrap  Next >