On Mon, Feb 24, 2020 at 12:55 PM Ken Kubota <[email protected]> wrote:
> My knowledge about Metamath is limited, but I believe that Mario is
> correct in that the form of reasoning resembles that of a Hilbert-style
> system.
>
> However, my perspective is different since my intention is to find the
> natural language of mathematics (following Andrews' notion of
> expressiveness).
> This means that (like in Andrews' Q0) metatheorems cannot be expressed
> directly using the means of the formal language only.
>
Do you have a reference for "Andrews' notion of expressiveness"? I see many
references to your work in your posts, but not any external citations. (I
don't know who Andrews is in this comment.) I think that expressiveness is
indeed key, but to me this also includes the avoidance of certain
in-principle exponential blowups that occur with some formalisms, naively
implemented. More on that below.
While implementations based on Q0 (such as Cris Perdues' Prooftoys or my R0
> software) use logical implication (located at the object language level) as
> the key symbol of the Hilbert-style system, logical frameworks use the
> turnstile or another symbols (located at the meta-language level) which
> denotes derivability / provability.
>
I do not know how to place metamath by this metric. You can identify both
an implication arrow in the logic, and a turnstile that is not quite in the
metalogic but is not directly accessible to reasoning.
So by definition Metamath (as a logical framework / a metalogic) doesn't
> fit into the definition of a Hilbert-style system in the narrow sense,
> which simply reflects the fact that the design purposes are different and
> therefore the language levels are.
>
I believe it is fair to characterize Metamath as a logical framework,
although it uses a weaker metalogic than LF does (essentially only
composition of universally quantified horn clauses).
But if you are too restrictive in your definition of a Hilbert style
system, you may end up excluding Hilbert as well. *No one* actually works
at the object level, certainly not the logicians that describe the object
level. Metamath aims to cover enough of the metalevel to be able to do
"logician proofs" about the object level. That is an expressiveness
concern, in case you can't tell.
> In real life no one does object-language proofs, not even textbooks that
> claim to work with Hilbert-style systems, because you can't reuse the
> theorems for other instances, and proofs become astronomically long. Let
> us say the object-language variables are v1, v2,... There is a Metamath (
> set.mm) scheme called "id" that states "phi -> phi" for any wff phi. If
> a proof in the style you are insisting on needed two instances of this, say
> "v1 = v2 -> v1 = v2" and "v3 e. v4 -> v3 e. v4" ("e." meaning "element
> of"), they would each have to be proved all over again starting from
> appropriate instantiations of the starting axiom schemes.
>
>
> Exactly this is done in the R0 software implementation: it does object
> language proofs only.
> Instead of schemes, templates are used (*.r0t files instead of the regular
> *.r0 files), so you can re-use the template with different initial values
> and simply include the template file.
> In his 2002 textbook, Andrews carefully distinguishes meta-language proofs
> from object language proofs by introducing boldface "syntactical variables"
> [Andrews, 2002, p. 11].
>
If that's the case, then the system is fundamentally limited, and subject
to exponential blowup, long before you get to the level that mathematicians
care about.
For comparison to a system you may be more familiar with, HOL has a rule
called INST, which allows you to derive from A1,...,An |- B the sequent
A1(sigma),...,An(sigma) |- B(sigma) where sigma = [x1 -> t1, ..., xm -> tm]
is a substitution of free variables in the A's and B with terms. (You can
also substitute type variables with a separate rule.)
This is what metamath does in its "one rule". The point here is that you
can prove a theorem once and instantiate it twice, at two different terms.
If you don't do this, if you reprove the theorem from axioms every time,
then if T2 uses T1 twice at two different terms, the proof of T2 will be
(at least) twice as long as that of T1. If T3 uses T2 twice and T4 uses T3
twice and so on, the lengths of the proofs grow exponentially, and if you
are rechecking all these proof templates at all instantiations then the
check time also increases exponentially. This is not a merely theoretical
concern; metamath.exe has a mechanism to calculate the length of direct
from axioms proofs and they are quite often trillion trillions of steps. If
you have no mechanism to deal with this, your proof system is dead on
arrival.
In order to fulfil both philosophical and practical needs, my suggestion is
> a two-step approach:
>
> The first step focuses on logical rigor and uses the object language only.
> (This is my current R0 software implementation.)
> In the second step the logic is reformulated in a meta-language where
> metatheorems can be expressed directly.
>
The thing is, the trust has to go into the higher level system too, because
you can't run object level proofs. (To this you will say you have an
implementation already, but as I and Norm have argued this system will die
on most proofs people care about.) The meta level system is stronger, but
only in the sense that weak subsystems of PA can be subsumed by stronger
subsystems of PA. Basically you have to believe in the existence of large
numbers with short descriptions, like 2^2^2^60. If the system is strong
enough to prove these numbers exist, then you can do proof existence proofs
to collapse that exponential blowup.
That's the logician analysis of what a substitution axiom does for a proof
system. Yes it's conservative, but it is also essential for getting things
done.
In summary, the object language (the first step) is not important, except
as a specification for the second step. Only the second step matters for
correctness and practical usability.
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvob5NjYAP3LuGoaJkPo%2BwcY0_2hkOR3mS%3D2mbZjVVo4g%40mail.gmail.com.
