FYI -- Alexandre Rademaker http://arademaker.github.io <http://arademaker.github.io/> http://researcher.ibm.com/person/br-alexrad <http://researcher.ibm.com/person/br-alexrad>
> Begin forwarded message: > > From: Ken Kubota <m...@kenkubota.de> > Subject: [isabelle] Software Implementation of the Mathematical Logic R0 > Available for Download > Date: 11 May 2017 07:16:09 GMT-3 > To: HOL-info list <hol-i...@lists.sourceforge.net>, > cl-isabelle-us...@lists.cam.ac.uk, coq-c...@inria.fr > Cc: "Prof. Andrew M. Pitts" <andrew.pi...@cl.cam.ac.uk>, "Prof. Peter B. > Andrews" <andr...@cmu.edu>, "Prof. Thomas F. Melham" > <thomas.mel...@balliol.ox.ac.uk>, "Prof. Michael J. C. Gordon" > <m...@cl.cam.ac.uk>, John Harrison <john.harri...@cl.cam.ac.uk> > > Dear Members of the Research Community, > > I am pleased to announce that the software implementation of the mathematical > logic R0, a further development of Peter B. Andrews' logic Q0, is now > available. The syntactic features provided by R0 are type variables > (polymorphic type theory), the binding of type variables with the abstraction > operator and single variable binder λ (type abstraction), and (some of) the > means necessary for dependent types (dependent type theory). > > The software implementation can be downloaded (license restrictions apply) at > http://doi.org/10.4444/100.10.3 > > > The logic R0 does not only allow quantification over types with quantifiers, > as > specified in [Andrews, 1965] and [Melham, 1993b], but, moreover, the binding > of > type variables with lambda (type abstraction), as suggested by Mike Gordon > for > HOL: "[...] 'second order' [lambda]-terms like \a. \x:a. x, perhaps such > terms > should be included in the HOL logic." [Gordon, 2001, p. 22] > > The expressiveness of the formal language obtained with type abstraction > allows > for a natural formulation of group theory [cf. p. 12 of > http://doi.org/10.4444/100.10.2]. With the set (type) of Boolean values o, > the > exclusive disjunction XOR, and an appropriate definition of groups Grp [p. > 362], the fact that (o, XOR) is a group can be expressed in lambda notation > with [p. 420] > Grp o XOR > > This enhancement of the expressiveness of the formal language overcomes the > "limitation of the simple HOL type system [...] that there is no explicit > quantifier over polymorphic type variables, which can make many standard > results [...] awkward to express [...]. [...] For example, in one of the most > impressive formalization efforts to date [Gonthier et al., 2013] the entire > group theory framework is developed in terms of subsets of a single universe > group, apparently to avoid the complications from groups with general and > possibly heterogeneous types." [Harrison, Urban, and Wiedijk, 2014, pp. 170 > f.] > > While in both Andrews' Q0 and Gordon's HOL the universal quantifier is > defined > as > ALL := [\p. p = [\x.T] ] > [Andrews, 2002, p. 212; Gordon and Melham, 1993], in R0, with type > abstraction, > the type is made explicit: > ALL := [\t. [\p. p = [\x.T] ] ] > with p of type (ot), or t -> o [p. 359 of http://doi.org/10.4444/100.10.2]. > Then, the set-theoretic proposition > ALL n : NAT . n+1 > 0 > in type theory can be expressed very naturally by > ALL NAT [\n . n+1 > 0] > > Furthermore, the enhanced expressiveness provided by R0 avoids the > circumlocutions connected with preliminary solutions like axiomatic type > classes recently developed and discussed for Isabelle/HOL. The expressiveness > of type abstraction also replaces the notion of compound types, which in HOL > are used for ordered pairs (the Cartesian product, cf. [Gordon and Melham, > 1993]), that in R0 can be formalized without compound types [cf. pp. 378 f. > of > http://doi.org/10.4444/100.10.2]. > > > R0 has an intuitive method of type introduction, which does not require the > additional axioms of the HOL type introduction mechanism: "Whenever a theorem > of the form p{oa}e{a} is inferred [...] (which in set theory is expressed by > e > ∈ p) [...] p is acknowledged as a type" [p. 11 of > http://doi.org/10.4444/100.10.2]. > > > Mike Gordon's HOL developed at Cambridge University is, like Andrews' logic > Q0, > based on the Simple Theory of Types (1940) developed by Alonzo Church, > Andrews' > Ph.D. advisor at Princeton University. Among the HOL group, there has always > been the awareness that besides automation, there is the philosophical > (logical) desire to reduce the means of the logic to a few principles. In the > HOL handbook, Andrew M. Pitts wrote the legendary sentence: "From a logical > point of view, it would be better to have a simpler substitution primitive, > such as 'Rule R' of Andrews' logic Q0, and then to derive more complex rules > from it." [Gordon and Melham, 1993, p. 213] > > In the same spirit, Mike Gordon wrote on the genesis of HOL: "[T]he terms > [...] > could be encoded [...] in such a way that the LSM expansion-law just becomes > a > derived rule [...]. This approach is both more elegant and rests on a firmer > logical foundation, so I switched to it and HOL was born." [Gordon, 2000, p. > 173] > > The general principle of reducing the logic (including the language) to a few > principles is the main criterion for the design of Q0 (having only a single > primitive rule of inference, Rule R), which is summarized by Peter B. Andrews > as follows: "Therefore we shall turn our attention to finding a formulation > of > type theory which is as expressive as possible, allowing mathematical ideas > to > be expressed precisely with a minimum of circumlocutions, and which is as > simple and economical as is possible without sacrificing expressiveness. The > reader will observe that the formal language we find arises very naturally > from > a few fundamental design decisions." [Andrews, 2002, pp. 205 f.] > > R0 "follows Andrews' concept of expressiveness (I also use the term > reducibility), which aims at the ideal and natural language of formal logic > and > mathematics." [p. 11 of http://doi.org/10.4444/100.10.2] Therefore R0 is, > unlike most other implementations, a Hilbert-style system, opting for > expressiveness instead of automation. > > R0 implements the philosophical program of Russell's and Whitehead's > 'Principia > Mathematica', logicism, i.e., the reduction of mathematics to formal logic, > and > even more, generalizes this idea by reducing formal logic itself to a few > principles. > > > Like John Harrison's HOL Light, R0 has an extremely small logical kernel. > Being > a Hilbert-style system, it has the smallest number of rules of inference > among > the programs implementing a fixed logic (not regarding logical frameworks > with > another kind of expressiveness). R0 resembles Norman Megill's Metamath, which > "attempts to use the minimum possible framework needed to express mathematics > and its proofs." [http://us.metamath.org/] With a size of less than 100 KB, > it > is the smallest proof checker or interactive theorem prover, including the > current versions of John Harrison's HOL Light, Mark Adams' HOL Zero, Norman > Megill's Metamath, and Freek Wiedijk's reimplementation of Automath. > > Like Q0, R0 uses the description operator, avoiding the problems of the > epsilon > operator for HOL already discussed by Mike Gordon himself: "It must be > admitted > that the ε-operator looks rather suspicious." [Gordon, 2001, p. 24] "The > inclusion of ε-terms into HOL 'builds in' the Axiom of Choice [...]." > [Gordon, > 2001, p. 24] > > R0 and PVS are the only implementations based on classical type theory with > some form of dependent types. Also, R0 and PVS are the only implementations > based on classical type theory with mathematical entities that may have > different types (or which have at least some form of subtyping). > > Unlike in Coq, in R0, no use is made of the Curry-Howard isomorphism, > favoring > a direct (unencoded, and hence, natural) expression rather than the encoding > of > proofs. For the same reason, it is an object (fixed) logic and not a logical > framework (such as Larry Paulson's Isabelle and Norman Megill's Metamath). > Like > in Cris Perdue's Prooftoys [http://prooftoys.org, http://mathtoys.org] - a > natural deduction variant of Andrews' Q0 - in R0, the turnstile symbol is > replaced by the logical implication [p. 12 of > http://doi.org/10.4444/100.10.2]. > > R0 is, together with HOL Zero [Adams, 2016, p. 34], the only proof checker or > interactive theorem prover which has the property of Pollack-consistency, > namely "being able to correctly parse formulas that it printed itself" > [Wiedijk, 2012, p. 85]. R0 is the only proof checker or interactive theorem > prover which can correctly parse whole proofs (and not only formulas) that it > printed itself. Finally, R0 has the property of "faithfulness, where internal > representation and concrete syntax correctly correspond. A printer that > printed > false as true and true as false might be Pollack-consistent but would not be > faithful." [Adams, 2016, p. 21] > > R0 is, like Automath, a mere proof checker (practically without any > automation > at all). > > > A full treatment of R0 shall be announced at > http://doi.org/10.4444/100.10.1 > > For references, please see: http://doi.org/10.4444/100.111 > > The SHA-512 checksum for file 'R0-v1.0.0.tar.gz' is: > 538e742c5d42258cf460e46d84c60ceb fa6b5843efba4f73c2c17206f5bab931 > 7f6edb31686b933147abd17af8114277 b833baf189f42c2b7587c409aecaed1f > > > Kind regards, > > Ken Kubota > > ____________________ > > Ken Kubota > http://doi.org/10.4444/100 > -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para postar neste grupo, envie um e-mail para logica-l@dimap.ufrn.br. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/C570B4F1-EA22-4891-964F-5ACF762D6425%40gmail.com.
