HomeHome Intuitionistic Logic Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Bad symbols? Use Firefox
(or GIF version for IE).

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
      1.5  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  The axioms of propositional calculus   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 526
            1.2.6  Logical disjunction   wo 605
            1.2.7  Decidable propositions   wdc 714
            1.2.8  Classical logic   ax-3 719
            1.2.9  Miscellaneous theorems of propositional calculus   pm5.21nd 808
            1.2.10  Abbreviated conjunction and disjunction of three wff's   w3o 852
            1.2.11  True and false constants   wtru 1198
            1.2.12  Logical 'xor'   wxo 1216
            1.2.13  Operations on true and false constants   truantru 1224
            1.2.14  Stoic logic indemonstrables (Chrysippus of Soli)   mpto1 1246
            1.2.15  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1   ee22 1250
      1.3  Predicate calculus mostly without distinct variables
            1.3.1  Equality-free predicate calculus axioms ax-5, ax-7, ax-gen   wal 1266
            1.3.2  Introduce equality axioms   cv 1323
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1349
            1.3.4  Introduce Axiom of Existence   ax-i9 1353
            1.3.5  Additional intuitionistic axioms   ax-ial 1358
            1.3.6  Predicate calculus including ax-4, without distinct variables   a4i 1360
            1.3.7  The existential quantifier   19.8a 1403
            1.3.8  Equality theorems without distinct variables   a9e 1473
            1.3.9  Axioms ax-10 and ax-11   ax10o 1488
            1.3.10  Substitution (without distinct variables)   wsbc 1523
            1.3.11  Theorems using axiom ax-11   equs5a 1550
      1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   a4imv 1567
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1578
            1.4.3  More theorems realted to ax-11 and substitution   albidv 1580
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1610
            1.4.5  More substitution theorems   hbs1 1679
            1.4.6  Classical logic theorems we'll need for existential uniqueness   orri 1757
            1.4.7  Existential uniqueness   weu 1766
      1.5  Classical (not intuitionistic) results
            1.5.1  Law of the excluded middle (classical)   exmid 1885
            1.5.2  Relationships between connectives (classical)   pm4.64 1892
            1.5.3  Additional substitution theorems (classical)   dfsb2 1897
            1.5.4  Exclusive or and related theorems (classical)   xor 1899
            1.5.5  Predicate logic axioms (classical)   dvelimfALT 1911

    < 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-1942
  Copyright terms: Public domain < Wrap  Next >