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  CLASSICAL FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Other axiomatizations of classical propositional calculus
      1.4  Predicate calculus mostly without distinct variables
      1.5  Predicate calculus with distinct variables

Detailed Table of Contents
PART 1  CLASSICAL 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 9
            1.2.4  Logical conjunction and logical equivalence   wa 96
            1.2.5  Logical negation (intuitionistic)   ax-in1 527
            1.2.6  Logical disjunction   wo 606
            1.2.7  Classical logic   con4d 715
            1.2.8  Miscellaneous theorems of propositional calculus   pm5.21nd 836
            1.2.9  Abbreviated conjunction and disjunction of three wff's   w3o 902
      1.3  Other axiomatizations of classical propositional calculus
            1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom   meredith 1250
            1.3.2  Derive the standard axioms from the Lukasiewicz axioms   luklem1 1268
            1.3.3  Logical 'nand' (Sheffer stroke)   wnand 1279
            1.3.4  Derive Nicod's axiom from the standard axioms   nic-justlem 1281
            1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom   nic-imp 1291
            1.3.6  True and false constants   wtru 1310
            1.3.7  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1   ee22 1319
      1.4  Predicate calculus mostly without distinct variables
            1.4.1  "Pure" (equality-free) predicate calculus axioms ax-5, ax-6, ax-7, ax-gen   wal 1335
            1.4.2  Introduce equality axioms ax-8 through ax-14 except ax-9   cv 1382
            1.4.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1402
            1.4.4  Derive ax-9 from a weaker version   a9wa9lem1 1404
            1.4.5  Introduce Axiom of Existence ax-9   ax-i9 1417
            1.4.6  Derive ax-4, ax-5o, and ax-6o   ax4 1423
            1.4.7  "Pure" predicate calculus including ax-4, without distinct variables   a4i 1432
            1.4.8  The existential quantifier   19.8a 1479
            1.4.9  Equality theorems without distinct variables   a9e 1556
            1.4.10  Axioms ax-10 and ax-11   ax10o 1575
            1.4.11  Substitution (without distinct variables)   wsbc 1604
            1.4.12  Theorems using axiom ax-11   equs5a 1631
      1.5  Predicate calculus with distinct variables
            1.5.1  Derive the axiom of distinct variables ax-16   a4imv 1641
            1.5.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1653
            1.5.3  Theorems without distinct variables that use axiom ax-11o   ax11b 1656
            1.5.4  Predicate calculus with distinct variables (cont.)   ax11v 1703
            1.5.5  More substitution theorems   equsb3lem 1771
            1.5.6  Existential uniqueness   weu 1829

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