• Proper Axiom files

  • ----------------------------

  • ax_equiv 4 predicates are stated to be equal via a chain of 3 equalities [pdf]
  • ax_ER, ax_ER_gen An Entity-Relationship model and its internal rendering [pdf,pdf]
  • ax_ER_old Variant of the Entity-Relationship model "ax_ER" [pdf]
  • ax_forkUr Existence of elements which are not pairs in fork algebras [pdf]
  • ax_graphIsom An isomorphism f between two graphs g,h which are devoid of isolated nodes [pdf]
  • ax_IsA Three IsA-chains, illustrating also the default-parameter mechanism [pdf]
  • ax_nats Tiny reduct of Peano arithmetic [pdf]
  • ax_plh Placeholder characterization [pdf]
  • ax_sets Algebraic formulation of a reduct of the Zermelo-Fraenkel set theory [pdf]
  • ax_sets_old Variant of "ax_sets" [pdf]
  • ax_sets_ur Algebraic formulation of a variant of Zermelo-Fraenkel catering for urelements [pdf]
  • ax_simplIsA Simplified variant of "ax_IsA" (it presupposes "defAs0A" and "defFoAs1") [pdf]
  • ax_tenseLogic Minimal tense logic [pdf]
  • axGraphIsom Various graph isomorphisms [pdf]

  • ----------------------------

  • ax_HdTl [pdf]
  • ax_HdTl_r [pdf]
  • ax_key [pdf]
  • axErnst [pdf]
  • ax_nested [pdf]
  • ax_plh0 A couple of axioms in the propositional letters r1,r2,r3,... (instead of in p1,p2,p3,...) [pdf]