Reformat Metamath

By Charles R Greathouse IV Last update Jan 29, 2010 — Installed 114 times.

Script Summary: Simplifies, expands, or simply reformats axiom requirements for Norman Megill's Metamath.



Version: 0.40 (beta), 2010-01-29

License: Public domain

Overview

Metamath is a system for methodically proving theorems all the way back to their axioms. This script can simplify requirements by removing provably redundant axioms; alternately, it can expand requirements by including all logical entailments.

The script also groups axioms together by type to make it easier to grasp, at a glance, what the theorem requires. For example, theorem ruc requires all of ZF except for the axiom of regularity, so the requirements are given as:

Propositional calculus:ax-1 ax-2 ax-3 ax-mp
Predicate calculus:ax-5 ax-6 ax-7 ax-gen ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-14 ax-17
ZF (fragment): ax-ext ax-rep ax-un ax-pow ax-inf  (missing ax-reg)

If the reformatting is all you want, you can of course turn off simplification. The script may also make other minor changes. One useful one is the ability to decide between gif and Unicode instead of changing to the link you click.

Use

Click Install in the top-right of this page to install the script. To change its options, click the 'Options' button to the right of the (now-simplified) axioms.

Support

If you find an error in the script (the script breaks on a page, or axioms are not fully simplified) feel free to drop me a line: my_firstname.my_lastname(@)case.edu. Please include your operating system (e.g. 32-bit Windows 7 or Ubuntu 9.04 64-bit), browser type and version (e.g. Firefox 3.5.3), the URL of the page that fails, and anything else that seems relevant. I may be able to help.

Alternately, try posting on the forums. If your problem is general enough someone may come to your aid.

Version History

0.40 (beta)Chromium/Google Chrome support added
0.30 (beta)Added support for the Hilbert Space Explorer and Quantum Logic Explorer.
0.20 (beta)BUGFIX: include the Axiom of Infinity as a part of Tarski–Grothendieck set theory, stability fixes
0.10 (beta)Added tooltips; refactored source
0.00 (beta)Initial public release.