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 206
[Hamilton] p. 73Rule 1axmp 193
[Hamilton] p. 74Rule 2axgen 197
[Margaris] p. 49Axiom A1ax1 190
[Margaris] p. 49Axiom A2ax2 191
[Margaris] p. 49Axiom A3ax3 192
[Margaris] p. 89Theorem 19.7alnex 174
[Margaris] p. 90Theorem 19.14exnal 188
[Margaris] p. 90Theorem 19.20alimdv 172
[Margaris] p. 90Theorem 19.22eximdv 173
[Megill] p. 444Axiom C5ax17 205
[Megill] p. 445Lemma L12ax10 200
[Megill] p. 448Scheme C6'ax7 196
[Megill] p. 448Scheme C8'ax8 198  ax9 199
[Megill] p. 448Scheme C9'ax12 202
[Megill] p. 448Scheme C12'ax13 203  ax14 204
[Monk2] p. 105Axiom C4ax5 194
[Monk2] p. 105Axiom C7ax8 198  ax9 199
[Monk2] p. 105Axiom C8ax11 201
[Monk2] p. 113Axiom C5-1ax17 205
[Monk2] p. 113Axiom C5-2ax6 195
[TakeutiZaring] p. 19Axiom 5axrep 207
[Tarski] p. 70Lemma 16ax11 201
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax17 205
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax13 203  ax14 204

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