Script Summary: Simplifies, expands, or simply reformats axiom requirements for Norman Megill's Metamath.
Version: 0.40 (beta), 2010-01-29
License: Public domain
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:
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.
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.
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.
|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.|