HOL Explorer Home Higher-Order Logic Explorer
Bibliographic Cross-References
Mirrors  >  Home  >  HOL Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the High-Order Logic Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular reference, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Higher-Order Logic Explorer
Bibliographic Reference DescriptionHigher-Order Logic Explorer Page(s)
[BellMachover] p. 461Axiom Extaxext 219
[Hamilton] p. 73Rule 1axmp 206
[Hamilton] p. 74Rule 2axgen 210
[Margaris] p. 49Axiom A1ax1 203
[Margaris] p. 49Axiom A2ax2 204
[Margaris] p. 49Axiom A3ax3 205
[Margaris] p. 89Theorem 19.7alnex 186
[Margaris] p. 90Theorem 19.14exnal 201
[Margaris] p. 90Theorem 19.20alimdv 184
[Margaris] p. 90Theorem 19.22eximdv 185
[Megill] p. 444Axiom C5ax17m 218
[Megill] p. 445Lemma L12ax10 213
[Megill] p. 448Scheme C6'ax7 209
[Megill] p. 448Scheme C8'ax8 211  ax9 212
[Megill] p. 448Scheme C9'ax12 215
[Megill] p. 448Scheme C12'ax13 216  ax14 217
[Monk2] p. 105Axiom C4ax5 207
[Monk2] p. 105Axiom C7ax8 211  ax9 212
[Monk2] p. 105Axiom C8ax11 214
[Monk2] p. 113Axiom C5-1ax17m 218
[Monk2] p. 113Axiom C5-2ax6 208
[TakeutiZaring] p. 19Axiom 5axrep 220
[Tarski] p. 70Lemma 16ax11 214
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax17m 218
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax13 216  ax14 217

  This page was last updated on 14-Aug-2016.
Copyright terms: Public domain
W3C HTML validation [external]