On Mon, Feb 24, 2020 at 2:20 PM Ken Kubota <[email protected]> wrote:
> 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 > > > > 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]> 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 > 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). > Why do you say Q0 or R0 and not "simple type theory"? There are contentions that HOL is too weak a type theory for much of mathematics. Simple type theory is even weaker. So in what sense is it expressive? (Granted, you can do a great deal with just PA, and I'm sure your system is at least as strong. But there is plenty of mathematics that goes beyond this.) > 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. > But the move to the second step adds new axioms, so even if the ideal formal language is elegant and rigorous, that property may not be preserved by the second level language, which is also the one that people actually use. 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 > > 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. > What is the computer implementation for then? As a practical tool, it is too limited, and in particular the exponential blowup means that you are pushing the upper bound caused by the finiteness of the hardware down to below many theorems that matter to people. If you want a system "for foundational and philosophical research", you can do that on paper. If you want to prove properties about the system, you need to formalize the system itself inside a theorem prover (presumably with a stronger axiom system). Within that system, you will be able to prove the provability of a lot of things you wouldn't be able to do directly in the system, by making use of the metalogical natural numbers to prove schematic constructions. 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/CAFXXJSsj%2Bn9TaeG8xdJJZYns3Ynt0dOUh2VEDT%2BtUSCQsJoMfQ%40mail.gmail.com.
