TOC of Theorem List - Linear Logic Proof Explorer

Home	Linear Logic Proof Explorer Theorem List (Table of Contents)	< Wrap  Next >
		Mirrors  >  Metamath Home Page  >  LLPE Home Page  >  Theorem List Contents       This page:  Detailed Table of Contents  Page List

Table of Contents Summary

PART 1  Hilbert-style axiomatisation of Linear Logic
      1.1  Basic stuff
      1.2  Intuitionistic logic
      1.3  Message passing
      1.4  Lambda calculus
      1.5  Quantifiers and equality

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

​*PART 1  Hilbert-style axiomatisation of Linear Logic
      *1.1  Basic stuff
            *1.1.1  Multiplicatives   wbot 1
            *1.1.2  Additives   wtop 29
            *1.1.3  Exponentials   wne 48
            *1.1.4  Implication   wlb 55
            *1.1.5  Operator properties and duals   wone 103
                  1.1.5.1  Multiplicatives revisited   wone 103
                  1.1.5.2  Additives revisited   wzero 129
                  1.1.5.3  Exponentials revisited   wpe 148
            *1.1.6  Miscellaneous theorems   ionei 163
      ​*1.2  Intuitionistic logic
      ​*1.3  Message passing
            1.3.1  Axioms for message passing   nvar 203
                  *1.3.1.1  Creation operator   ax-int 208
                  1.3.1.2  Communication   ax-subse1 220
            1.3.2  Message passing theorems   sead 231
            *1.3.3  Message passing dual operators   wnse 240
            1.3.4  Nilad abstractions   nnab 266
      1.4  Lambda calculus
            1.4.1  Intuitionistic logic but with lambda calculus   ntru 297
      ​*1.5  Quantifiers and equality
            1.5.1  Axioms for predicate logic with equality   wal 318
            1.5.2  Auxiliary axioms for predicate logic with equality   ax-negf 330