Most of your arguments concern (are answered with) the two-step approach, so let me answer your questions on Andrews and expressiveness first and then jump to the very end, where the two-step approach is discussed.
____________________________________________________ Ken Kubota doi.org/10.4444/100 <https://doi.org/10.4444/100> > Am 24.02.2020 um 22:30 schrieb Mario Carneiro <[email protected]>: > > > > On Mon, Feb 24, 2020 at 12:55 PM Ken Kubota <[email protected] > <mailto:[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. In section 1 of my original post I provided a quote by Andrews and an explanation: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ <https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ> The basic idea is to naturally express all of mathematics with a minimum of requirements. Q0 basically has lambda notation, two primitive symbols and two primitive types, and a single rule of inference. R0 has only little more. Both are Hilbert-style systems (operating at the object language level only). Andrews is Prof. Peter B. Andrews, creator of the higher-order logic Q0, Professor of Mathematics, Emeritus, Carnegie Mellon University. Homepage: http://gtps.math.cmu.edu/andrews.html <http://gtps.math.cmu.edu/andrews.html> Faculty: https://www.cmu.edu/math/people/faculty/andrews.html <https://www.cmu.edu/math/people/faculty/andrews.html> > > 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 >> <http://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. This is not quite correct. Not only that the first step is the logical foundation on which the second is established upon. Moreover, a reference implementation is required to study certain cases. In particular the violation of type restriction has to be avoided, as otherwise the system is rendered inconsistent. This is quite tricky, and case studies are necessary, especially if you want to implement new features such as type abstraction and dependent types. Also, you want to show that in principle all of mathematics can be expressed in the reference implementation (and the second step is due to practical considerations only). While of course you need the second step for numbers such as 2^2^2^60, all principle questions (such as whether an antinomy can be expressed) can be addressed with the first step. Finally, only in the first step (the ideal formal language) the formulation is very elegant, and logical rigor preserved in a philosophical sense. For example, a certain condition in Q0 appears as two distinct (independent) conditions in Isabelle's metalogic (a natural deduction system). Quote: For example, in Isabelle's metalogic M by Larry Paulson, the Eigenvariable conditions appear as two distinct (independent) conditions: [...] By contrast, in the logic Q0 by Peter Andrews, the restrictions in these (derived) rules have their origin in the substitution procedure of (the primitive) Rule R', which is valid only provided that it is not the case that "x is free in a member of [the set of hypotheses] H and free in [A = B]." [Andrews, 2002, p. 214]. [...] Hence, in a bottom-up representation (like Q0) - unlike in a top-down representation (like Isabelle's metalogic M) - it is possible to trace the origin of the two Eigenvariable conditions back to a common root, i.e., the restriction in Rule R'. https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-May/msg00013.html> So the formal language obtained in the first step is much more elegant than a practical system obtained in the second step. For foundational and philosophical research, the first is preferred, for advanced mathematics such as with large numbers the second is preferred. -- 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/F90B573C-606F-4E5D-87C1-1F24C32D6C16%40kenkubota.de.
