Dear List Members,
dear Norman Megill,
Metamath (
metamath.org) seems to have a concept very similar to that of
Andrews' logic Q0 described online at:
https://plato.stanford.edu/entries/type-theory-church/#ForBasEqu
The passages from the Metamath homepages quoted below correspond to what
Andrews calls "expressiveness", and the description of the Metamath system
there resembles the R0 implementation, a further development of Q0. For more
information, see the overview at:
http://doi.org/10.4444/100.111
As I would like to quote from these passages and to credit the quotes
correctly, please let me know if the author is not Norman Megill.
It is claimed that Metamath "is fundamentally a Hilbert-style system."
http://us.metamath.org/mpegif/mmnatded.html#natural-deduction-metamath
However, I would like to make a distinction. Already in the above quote a
careful formulation was used, as indicated by the limitation "fundamentally".
It is, of course, correct, that Metamath is a Hilbert-style system in the sense
that it doesn't use heavyweight metamathematical operations as primitive rules
involving the union of or the deletion from the sets of hypotheses, as for
example in HOL Light, cf. pp. 2 f. at
http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf
But in Metamath, the logic can reason explicitly about Hilbert-style
metatheorems. For example, in Q0, the rule of Modus Ponens is obtained as a
derived metatheorem:
"If H |- A and H |- A -> B, then H |- B." [Andrews, 2002, p. 224 (5224)]
Note that the terms "If", "and" and "then" indicate that this relation is not
part of the formal language, but that this is a metatheorem [Andrews, 2002, p.
11] ("meta": "above" the language).
In Metamath, this is expressed by:
"Rule of Modus Ponens ax-mp |- ph & |- (ph -> ps) => |- ps"
http://us.metamath.org/mpegif/mmset.html#scaxioms
It is claimed: "The symbols & and => are used informally in the table above to
indicate the relationship between hypotheses and conclusion; they are not part
of the formal language."
http://us.metamath.org/mpegif/mmset.html#scaxioms
However, de facto this rule (stated as axiom) is used to infer from the schema
to specific instances by substitution, making it part of the formal reasoning,
which is equivalent to being part of the formal language.
In the R0 implementation, metatheorems like rule of Modus Ponens cannot be
expressed explicitly like in Metamath
http://us.metamath.org/mpegif/ax-mp.html
but only as template, which means that for each instance the proof has to be
carried out again, and not proven generally and then instantiated by
substitution as in Metamath; hence metatheorems remain "meta", i.e., outside of
the language (and the reasoning). In this sense, it is following the concept of
Metamath, but is slightly more consequent.
As a result, proofs in R0 are much slower, as many recursions occur. There is
no chance of verifying 20,000 theorems within 5 or 6 seconds.
Therefore I would like to distinguish between Hilbert-style systems in a wide
sense (to which Metamath belongs), and Hilbert-style systems in a narrow sense
not allowing to directly express metatheorems (to which Metamath does not
belong).
More controversial I find the claim that Metamath has only one rule, which
holds for Q0 (with the single rule of inference Rule R [Andrews, 2002, p. 213],
also a substitution rule). The variables instantiated by the Metamath rule as
described
http://us.metamath.org/mpegif/mmset.html#proofs
correspond to syntactical variables as defined in [Andrews, 2002, p. 11], which
means that the Metamath "single rule" is actually a rule of the meta-language,
and regular rules can be coded as axioms with this Metamath meta-language rule.
So while Q0 has a single rule of inference (of the formal language itself) from
which all other rules are derived (as metatheorems outside of the formal
language), the Metamath substitution rule is actually a meta-language rule
allowing the usual rules of the formal language to be expressed as
axioms/theorems.
For the references, please see:
http://doi.org/10.4444/100.111
Kind regards,
Ken Kubota
____________________
Ken Kubota
http://doi.org/10.4444/100
Quotes
1. Minimum Possible Framework
"Unlike most other systems, Metamath attempts to use the minimum possible
framework needed to express mathematics and its proofs. Other systems do not
consider that aspect necessarily important, and their underlying computer
programs can be large and complex in order to perform mathematical reasoning at
a higher level. Metamath's proofs are often quite long compared to those of
other systems, but they are completely transparent with nothing hidden from the
user. All reasoning is done directly in the proof itself rather than by
algorithms embedded in the verification program. Metamath is unique in this
sense, offering an alternative approach for those attracted to its philosophy
of simplicity."
http://us.metamath.org/index.html
2. Reverse Engineering
"As humans, we observe interesting patterns in these 'meaningless' symbol
strings as they evolve from the axioms, and we attach meaning to them. One
result is the set of natural numbers, whose properties match those we observe
when we count everyday objects, and their extensions to rational and real
numbers. Of course, numbers were discovered centuries before set theory, and
historically they were 'reversed engineered' back to the axioms of set theory.
The proof of 2 + 2 = 4 shows what was involved in that reverse engineering,
representing the work of many mathematicians from Dedekind to von Neumann. At
the other extreme of abstraction is the theory of infinite sets or transfinite
cardinal numbers. Some of the world's most brilliant mathematicians have given
us deep insight into this mysterious and wondrous universe, which is sometimes
called 'Cantor's paradise.'"
http://us.metamath.org/mpegif/mmset.html#overview