Hi Mario,
Since some of the questions (no. 2) are relevant for type theory, too,
let me copy to the HOL list, and answer below each quoted passage.
The whole discussion can be found at
https://groups.google.com/forum/#!topic/metamath/s19SSncdtiM
> Am 16.04.2017 um 01:56 schrieb Mario Carneiro <[email protected]>:
>
> Hi Ken,
>
> I've been interested in the discussions surrounding this new logic / software
> system, but frankly I don't know how to enter the arena because it hasn't
> been made clear to me what R0 *is*, as a logic. Your publication is over 800
> pages of computer output, with only one page on motivation and no "how to
> read this paper" discussion. What does the program do, and how? Given where
> you are publishing I already know it is a proof verifier for a new logic, but
> the nature of this logic is not clear, and without this I cannot effectively
> perform a comparison with Metamath.
1.
R0 is based on and very similar to Q0, so studying Peter B. Andrews' Q0
is the first step.
The reference is [Andrews, 2002, pp. 201–237] as specified on p. 11 of
http://www.owlofminerva.net/files/formulae.pdf
A large portion of the proofs formalized in my publication is directly
taken from there, e.g., the derivation of Modus Ponens, for which
the source is given (p. 94):
"Source: [Andrews 2002 (ISBN 1-4020-0763-9), p. 224]"
The proofs in Andrews' 2002 textbook are much more reader friendly.
R0 extends Q0 with type variables and binding of type variables with
lambda (type abstraction), which allows for explicit quantification over
types as desired by John Harrison at el. for HOL in the paper quoted.
Peter is Professor Emeritus at CMU and still living in Pittsburgh,
according to his email from last month. As you seem to be a
Ph.D. student at CMU, you might have the chance to meet him
and ask questions about Q0.
My publication is only one of three parts, as indicated at
http://doi.org/10.4444/100.10
I will try to make the software available as soon as possible.
The text with the full explanation might be published next year.
I will send you the 2015 draft for private use.
Please do not quote without explicit permission.
The R0 implementation allows to express all wffs of R0 and
obtain all inferences of R0 using the rules mentioned on p. 12.
R0 takes commands from a file or interactively, and only
mathematically valid theorems can be obtained.
The input and source code files are in subsections 2.2.*,
and the formatted output files are in subsections 2.1.*.
Hence the R0 software represents the R0 logic, and ideally,
this should be more or less identical with mathematics in general.
(more below)
> On Sat, Apr 15, 2017 at 6:19 PM, Ken Kubota <[email protected]> wrote:
> > Am 15.04.2017 um 22:53 schrieb vvs <[email protected]>:
> >
> > Thanks for your answer.
> >
> > On Saturday, April 15, 2017 at 11:00:55 PM UTC+3, Ken Kubota wrote:
> > So the LCF approach is a matter of the architectural design of the software,
> > but does not confine the logic to having either a poor or rich type system.
> >
> > Yes, but the software implementations surely have some design preferences
> > which could make it better fit for certain applications. Seems that the
> > current trend is to prefer complex software systems for computer science
> > problems, while it's more viable to use simpler ones for the work related
> > to foundations of mathematics. And I have an impression that most practical
> > effort goes into computer science applications, which could be seen by a
> > number of implementations alone.
>
> From my experience, I would basically agree, but add some detail.
> The complex software systems are very good in finding (automating)
> mathematical proofs, but automating proofs is, which supports your statement,
> not related to the foundations of mathematics.
>
> Without judging the philosophical concept, but looking at the
> technical software design only, there are, roughly spoken,
> three levels of (software) complexity:
>
> 1. simple software implementations: Automath, Metamath, R0
> 2. medium complex software implementations: HOL, HOL Light, HOL Zero
> 3. very complex software implementations: Isabelle [Isabelle/HOL]
>
> The simple software implementations, providing little or no automation,
> are rather proof checkers and are suited for mathematics only.
> The medium and complex software implementations are used for
> both mathematics and practical applications such as hardware verification.
>
> I want to remind you that the link between a kernel and an interface with
> automation need not be one-to-one. In particular, Metamath can be small and
> still have automation of arbitrary complexity. This is similar to the LCF
> kernel approach, except this suggests the image that the kernel is one part
> of a single behemoth program, where I prefer to think of one (or more)
> kernels extended with additional automation packages or IDEs in a pluralistic
> way
>
> As such, I reject the above inference that Metamath and similar systems
> cannot be used for hardware verification because they lack automation
> capabilities, since this can be added after the fact. You can have your cake
> and eat it too in this way.
2.
I'm not familiar with Metamath in detail, and might be mistaken
and apologize for this.
Of course, ZFC is a very expressive, but for general reasons,
I consider type theory the better approach for expressing
mathematics than (axiomatic) set theory.
Type theory prevents the paradoxes by means of the language,
as it makes the classification of mathematical objects explicit.
The concept of (axiomatic) set theory then appears as a rather
auxiliary solution, since with the distinction between classes and
sets first all inferences are forbidden, and with the axioms some
are allowed again. This renders the set of axioms as historically
arbitrary (the mathematics currently used), as shown with later
additions like axioms for large cardinals.
So (axiomatic) set theory does not provide a systematic solution
like type theory, which uses the means of the formal language
for preventing the paradoxes as intended by Russell.
> Another clear distinction is Hilbert-style vs. natural deduction.
> For automation, natural deduction is inevitable.
> If you look at the diagram on p. 1 of
> http://www.owlofminerva.net/files/fom.pdf
> you will see Q0 and HOL as the two descendants of Church's STT.
> Q0 is the more philosophical system with its focus on expressiveness
> (hence, Hilbert-style), whereas HOL is designed for automation
> necessary for practical applications (hence, natural deduction).
>
> I am not sure whether Metamath is Hilbert-style or natural deduction,
> and already had a short discussion with Cris Perdue about this.
> It might even be a third alternative, since Metamath is a logical framework.
> The reason why I do not consider Metamath as fully Hilbert-style is, that,
> being a logical framework, it has some meta-level (or meta-theory),
> rendering, at the very first glance, the Metamath substitution rule
> practically a representation of many rules expressed in a different manner.
>
> I need not point out that Metamath clearly brands itself as a Hilbert-style
> system. If you take pure Metamath, with no axioms, the "one axiom" involves
> substitution into theorems, applied as inference rules. This gives proofs a
> clear tree (or dag) structure, and is not significantly different from either
> Hilbert-style or natural deduction (written as tree proofs of Gamma |- phi,
> not trees of formulas with hypothesis cancellation).
I would have to take a closer look at Metamath, but my main point will follow
below.
> In the design of (Hilbert-style) R0, it was important for me that there
> is no meta-theory at all, which is also the reason why the turnstile is
> replaced by the logical implication (a decision that was made
> independently by Cris Perdue, too, for his Prooftoys system, a
> natural deduction variant of Q0).
>
> This distinction makes no sense to me. What does the head symbol have to do
> with it? Do you have a complete and unambiguous specification of R0's logical
> system that I could look at?
3.
[Andrews, 2002, pp. 201–237] together with my 2015 draft emailed to you
should be sufficient for a specification of the R0 logic.
The axioms for R0 can be found on pp. 353 ff. of
http://www.owlofminerva.net/files/formulae.pdf
For the definitions, see pp. 359 ff.
One approach is the semantic approach (model theory), which is
appealing to many mathematicians, as the justification for the syntactic
inference is expressed with mathematical means.
But there is also another possibility, the syntactic approach.
In philosophy, a justification by a meta-theory (in which the
semantic evaluation takes place in model theory) is considered
problematic.
If a theory is justified by a meta-theory, than what justifies the meta-theory?
Such an approach would be considered as "outward" in philosophy.
The alternative is trying to express as much as possible within (!) the
language,
this approach is called "immanent" (= within).
For this reason, the meta-perspective (bird's view from top) as used
with the turnstile symbol for provability should not be used for
expressing rules: "The turnstile (⊢) was eliminated and replaced by
the logical implication (⊃) [e.g., cf. pp. 303 ff. (K8025 = Deduction Theorem)
and Andrews, 2002, pp. 228 f. (5240 = Deduction Theorem)]."
http://www.owlofminerva.net/files/formulae.pdf (p. 12)
The turnstile may be used for metamathematics expressing properties
of a formal system after (!) setting up the language and logic, but should
not be used before, legitimizing or setting up the logic itself.
> Mario Carneiro
Kind regards,
Ken Kubota
____________________
Ken Kubota
http://doi.org/10.4444/100
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
