Comparison of Metamath and Q0; Hilbert-style vs. Natural Deduction; Quotes on Metamath

[Ken Kubota]

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

[David A. Wheeler]

On Wed, 22 Feb 2017 00:04:49 +0100, Ken Kubota <ma...@kenkubota.de> wrote:
> 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...

> 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).

I've been trying to put together mmnatded.html, and coincidentally
I just expanded that "fundamentally" sentence to try to make clearer
what was intended. I hope I succeeded. New version:

"MPE is fundamentally a <B>Hilbert-style</B> system.
That is, MPE is based on a
larger number of axioms (compared to natural deduction systems),
a very small set of rules of inference (modus ponens),
and the context is not changed
by the rules of inference in the middle of a proof.
That said, MPE proofs can be developed using the
natural deduction (ND) approach as originally developed by
Ja&sacute;kowski and Gentzen."

I hope that makes the intended meaning clearer.
The purpose of the text in that section was to provide an introduction
to using natural deduction approaches in MPE. It certainly wasn't
intended to be a deep dive into the capabilities of Metamath itself.

It's certainly true that Metamath *itself* has a metarule (substitution)
in addition to the inference rule modus ponens that is defined within MPE.

I'll let Norm and Mario comment on the other points.

--- David A. Wheeler

[Mario Carneiro]

Hello Ken,

I believe some of your questions are best answered with a more careful distinction of "object" and "meta", which is (unsurprisingly) quite critical to reasoning about metamath.

Metamath is a formal system (a syntactic proof system), in which the object statements of metamath are semantically interpreted as theorem schemes in some "lower" object language (which is not actually present in the syntax). That is, metamath is an object language that is modeled after metalanguages. The variables of metamath are interpreted as metavariables of this lower object language, and the theorems of metamath are theorem schemes of the lower language. Keep this interpretation in mind for the rest.

On Tue, Feb 21, 2017 at 6:04 PM, Ken Kubota <ma...@kenkubota.de> wrote:

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

The way I would state the above is that ax-mp is a *single* theorem of metamath, namely the theorem ph, (ph -> ps) |- ps (where ph and ps are "concrete" variables). This works because metamath has variables that can denote wffs. In many presentations of propositional calculus systems, there are atomic wff symbols p,q,r,... - in terms of these the equivalent statement would be the single theorem p, (p -> q) |- q.

What makes metamath "fundamentally a Hilbert system" is the lack of a deduction theorem: we cannot reason from p |- q to |- (p -> q) within the logic itself. (Additional discussion on this point can be found at http://us2.metamath.org:88/mpegif/mmnatded.html and http://us2.metamath.org:88/mpegif/mmdeduction.html .)

 

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.

I am in agreement with you on this point. Metamath's "single rule" is the substitution of expressions for the variables in a theorem, meaning that from the theorem ph, (ph -> ps) |- ps we can conclude, for example, (ch -> ch), ((ch -> ch) -> ph) |- ph. This is a "zero step" proof, meaning that it is invisible to the derivation, which makes it easy to treat ph, (ph -> ps) |- ps as a theorem schema instead of a theorem, but it is in fact a theorem in the object language of Metamath (which, recall, can be viewed as a metalanguage for a more standard prop calc formal system).

 

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).

Metamath does not actually have the ability to express metatheorems of its own language. The single substitution rule, together with the positioning of the formal system as modeling a metalanguage for FOL, makes it easy to express theorems that would be metatheorems in these languages, but this is no different from the situation in which PA is able to express metatheorems of Q (such as commutativity of +) by means of an extra axiom, or a deep embedding (note that Q can prove theorems of PA by working at the meta-level). An example of an actual metamath metatheorem is the fact that metamath proves |- ( x = y -> P(x) = P(y) ) where P(x) is an expression containing the variable x and P(y) has the x replaced by y.

 

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.

I'm not sure I'm understanding your claim, but Metamath's "one rule" is definitely a metatheorem (which is to say, cannot be expressed in metamath's own language without a deep embedding). It says something like: If metamath proves theorem T and T' is obtained by substituting variables in T by expressions of the appropriate type, then T' is a theorem of metamath. (See Appendix C of the Metamath book for more details on this rule and more generally the formalization of the metamath formal system.)

Regards,

 

Mario Carneiro