One widely-used system is Higher Order Logic (with various extensions sometimes), one core of which you can find here: http://sourceforge.net/projects/hol/files

One widely-used system is Higher Order Logic (with various extensions sometimes), one core of which you can find here: http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf/download http://sourceforge.net/projects/hol/files/hol/kananaskis-10/... This is based on type theory (and has a model in set theory), but isn't as powerful as the logics used in Coq and similar theorem provers (the Calculus of (Inductive) Constructions). You might be interested in metamath: http://us.metamath.org/ http://us.metamath.org/, which lists the axioms used in its largest body of work: http://us.metamath.org/mpegif/mmset.html#axioms http://us.metamath.org/mpegif/mmset.html#axioms