74 views

Skip to first unread message

Mar 12, 2018, 3:48:42 PM3/12/18

to HOL-info list, cl-isabe...@lists.cam.ac.uk, meta...@googlegroups.com

Dear Members of the Research Community,

Finalizing my overview at http://www.owlofminerva.net/files/fom.pdf

I would like to ask for major logics and logical frameworks not considered yet.

The logical frameworks included now (as logical frameworks, not only object

logics like Isabelle/HOL) are Isabelle and Metamath. These are also the only

two logical frameworks mentioned by Freek Wiedijk as of 2003, see p. 9 at

http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf

Kinds regards,

Ken Kubota

____________________

Ken Kubota

http://doi.org/10.4444/100

Finalizing my overview at http://www.owlofminerva.net/files/fom.pdf

I would like to ask for major logics and logical frameworks not considered yet.

The logical frameworks included now (as logical frameworks, not only object

logics like Isabelle/HOL) are Isabelle and Metamath. These are also the only

two logical frameworks mentioned by Freek Wiedijk as of 2003, see p. 9 at

http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf

Kinds regards,

Ken Kubota

____________________

Ken Kubota

http://doi.org/10.4444/100

May 3, 2018, 4:49:18 PM5/3/18

to R. Pollack, HOL-info list, cl-isabe...@lists.cam.ac.uk, meta...@googlegroups.com

Hi Randy,

Thanks for your advice, which was very helpful.

In an email sent privately, somebody else also pointed out the importance of

Twelf as a logical framework system, and mentioned various logical frameworks

by Robin Adams as well as Beluga.

I have added Twelf to the graph (and a footnote on p. 3) and compiled my

research results further below.

The reason why I haven't studied the details of logical frameworks yet is that

there are two both legitimate, although conflicting methods of representing

mathematics, and logical frameworks clearly belong to the second method

(top-down), which is based on the first method (bottom-up).

For example, in Isabelle's metalogic M by Larry Paulson, the Eigenvariable

conditions appear as two distinct (independent) conditions:

"Eigenvariable conditions:

∀I: provided x not free in the assumptions

∃E: provided x not free in B or in any assumption save A"

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, p. 19

(The object logic serving as an example here is intuitionistic first-order

logic.)

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].

For the introduction of the universal quantifier, cf. the Rule of Universal

Generalization (Gen) (Theorem 5220 in [Andrews, 2002, p. 222]).

For the elimination of the existential quantifier, cf. Rule C (Theorem 5245 in

[Andrews, 2002, p. 230]). (Note that Andrews' Rule C covers all cases, and

Paulson's rule ∃E only the special case x=y of Rule C.)

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'.

Generally speaking, in order to fully reveal the underlying philosophical

principles, a bottom-up representation is required, which follows the principle

of "expressiveness" (Andrews). I prefer the term "reducibility"; John Harrison

uses the term "decomposition": "complex inference rules which ultimately

decompose to these primitives".

http://www.cl.cam.ac.uk/~jrh13/papers/reflect.pdf, p. 1 (PDF p. 2)

A bottom-up representation (which is better suited for foundational research)

is clearly a Hilbert-style system: It has the elegance of having only a few

rules of inference (in Q0 even only a single rule of inference - Andy Pitts:

"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]).

Metatheorems are not expressible within the formalism; the metatheorems are

literally "meta" ("above" - i.e., outside of - the logic). In software

implementations of Q0 or descendants (Prooftoys by Cris Perdue or my R0

implementation), the metalogical turnstile (⊢) symbol is replaced by the

logical implication, which shows the tendency to eliminate metalogical elements

from the formal language.

A top-down representation (which is better suited for applied mathematics:

interactive/automated theorem proving) is either a natural deduction system

(like HOL) or a logical framework (like Isabelle): It has a proliferation of

rules of inference (e.g., eight rules for HOL [cf. Gordon and Melham, 1993, pp.

212 f.]). Metalogical properties (metatheorems) are expressible to a certain

extent, e.g., using the turnstile (⊢) symbol (the conditionals / the parts

before the turnstile may differ in the hypothesis and the conclusion), or the

meta-implication (⇒) in Isabelle's metalogic M (not to be confused with the

implication (⊃) of the object-logic), see

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, p. 4

Unfortunately, the gain of expressiveness in terms of metalogical properties by

making metatheorems symbolically representable is obtained at the price of

philosophical rigor and elegance in expressing the underlying object logic

(object language).

In summary, since the top-down representations (capable of expressing

metatheorems) are based on the corresponding bottom-up representation (object

logic), the bottom-up representation has to be studied first before unraveling

further dependencies in a top-down representation. I believe Q0 or some

descendant of it to be such a basis for reducing mathematics to formal logic as

intended in Russell's philosophical program of logicism.

For the references, please see: http://doi.org/10.4444/100.111

Best regards,

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Some Research Results on Logical Frameworks

Link collection:

- Twelf's wiki: http://twelf.org/wiki/Case_studies

- Abella's library: http://abella-prover.org/examples

- Beluga's distribution: http://complogic.cs.mcgill.ca/beluga/

- the Coq implementation of Hybrid:

http://www.site.uottawa.ca/~afelty/HybridCoq/

compiled from these two papers:

Amy Felty, Alberto Momigliano, Brigitte Pientka

An Open Challenge Problem Repository for Systems Supporting Binders

http://doi.org/10.4204/EPTCS.185.2 (p. 18)

Brigitte Pientka, Joshua Dunfield

Beluga: A Framework for Programming and Reasoning with Deductive Systems

(System Description)

http://doi.org/10.1007/978-3-642-14203-1_2 (p. 16)

A logical framework by Robin Adams:

Robin Adams

Lambda-Free Logical Frameworks

http://arxiv.org/abs/0804.1879v2

Some interesting papers by Frank Pfenning et al.:

Frank Pfenning, Conal Elliott (1988)

Higher-Order Abstract Syntax

http://doi.org/10.1145/53990.54010 and

http://www.cs.cmu.edu/~fp/papers/pldi88.pdf

Frank Pfenning (1996)

The Practice of Logical Frameworks

http://doi.org/10.1007/3-540-61064-2_33 and

http://www.cs.cmu.edu/~fp/papers/caap96.pdf

Frank Pfenning, Carsten Schürmann (1999)

System Description: Twelf – A Meta-Logical Framework for Deductive Systems

http://doi.org/10.1007/3-540-48660-7_14 and

http://www.cs.cmu.edu/~fp/papers/cade99.pdf

Frank Pfenning (2002)

Logical Frameworks - A Brief Introduction

http://doi.org/10.1007/978-94-010-0413-8_5 and

http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf

According to Pfenning and Elliott (1988), higher-order abstract syntax has an

even more expressive power than Isabelle's λ-calculus: "Isabelle [18] uses a

representation similar to ours for the statement of rules, and uses

higher-order unification for deduction. Isabelle's λ-calculus representation

does not have the expressive power of higher-order abstract syntax, but

explicitly encodes quantifier dependencies."

> Am 12.03.2018 um 23:41 schrieb R. Pollack <rpol...@gmail.com>:

>

> Ken,

>

> You should know about the Edinburgh Logical Framework (ELF), best implemented in the Twelf system. While ELF is a particular framework, there is tons of work about specification and programming in dependently typed frameworks. See e.g. many papers by Frank Pfenning, Amy Felty, Bob Harper, Brigitte Pientka, Alberto Momigliano. There is also a lot of work about other simply typed frameworks; e.g. Abella. There is a lot to say about consistency, expressiveness and usability of frameworks.

>

> You haven't even scratched the surface of logical frameworks.

>

> --Randy

Thanks for your advice, which was very helpful.

In an email sent privately, somebody else also pointed out the importance of

Twelf as a logical framework system, and mentioned various logical frameworks

by Robin Adams as well as Beluga.

I have added Twelf to the graph (and a footnote on p. 3) and compiled my

research results further below.

The reason why I haven't studied the details of logical frameworks yet is that

there are two both legitimate, although conflicting methods of representing

mathematics, and logical frameworks clearly belong to the second method

(top-down), which is based on the first method (bottom-up).

For example, in Isabelle's metalogic M by Larry Paulson, the Eigenvariable

conditions appear as two distinct (independent) conditions:

"Eigenvariable conditions:

∀I: provided x not free in the assumptions

∃E: provided x not free in B or in any assumption save A"

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, p. 19

(The object logic serving as an example here is intuitionistic first-order

logic.)

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].

For the introduction of the universal quantifier, cf. the Rule of Universal

Generalization (Gen) (Theorem 5220 in [Andrews, 2002, p. 222]).

For the elimination of the existential quantifier, cf. Rule C (Theorem 5245 in

[Andrews, 2002, p. 230]). (Note that Andrews' Rule C covers all cases, and

Paulson's rule ∃E only the special case x=y of Rule C.)

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'.

Generally speaking, in order to fully reveal the underlying philosophical

principles, a bottom-up representation is required, which follows the principle

of "expressiveness" (Andrews). I prefer the term "reducibility"; John Harrison

uses the term "decomposition": "complex inference rules which ultimately

decompose to these primitives".

http://www.cl.cam.ac.uk/~jrh13/papers/reflect.pdf, p. 1 (PDF p. 2)

A bottom-up representation (which is better suited for foundational research)

is clearly a Hilbert-style system: It has the elegance of having only a few

rules of inference (in Q0 even only a single rule of inference - Andy Pitts:

"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]).

Metatheorems are not expressible within the formalism; the metatheorems are

literally "meta" ("above" - i.e., outside of - the logic). In software

implementations of Q0 or descendants (Prooftoys by Cris Perdue or my R0

implementation), the metalogical turnstile (⊢) symbol is replaced by the

logical implication, which shows the tendency to eliminate metalogical elements

from the formal language.

A top-down representation (which is better suited for applied mathematics:

interactive/automated theorem proving) is either a natural deduction system

(like HOL) or a logical framework (like Isabelle): It has a proliferation of

rules of inference (e.g., eight rules for HOL [cf. Gordon and Melham, 1993, pp.

212 f.]). Metalogical properties (metatheorems) are expressible to a certain

extent, e.g., using the turnstile (⊢) symbol (the conditionals / the parts

before the turnstile may differ in the hypothesis and the conclusion), or the

meta-implication (⇒) in Isabelle's metalogic M (not to be confused with the

implication (⊃) of the object-logic), see

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf, p. 4

Unfortunately, the gain of expressiveness in terms of metalogical properties by

making metatheorems symbolically representable is obtained at the price of

philosophical rigor and elegance in expressing the underlying object logic

(object language).

In summary, since the top-down representations (capable of expressing

metatheorems) are based on the corresponding bottom-up representation (object

logic), the bottom-up representation has to be studied first before unraveling

further dependencies in a top-down representation. I believe Q0 or some

descendant of it to be such a basis for reducing mathematics to formal logic as

intended in Russell's philosophical program of logicism.

For the references, please see: http://doi.org/10.4444/100.111

Best regards,

Ken

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Some Research Results on Logical Frameworks

Link collection:

- Twelf's wiki: http://twelf.org/wiki/Case_studies

- Abella's library: http://abella-prover.org/examples

- Beluga's distribution: http://complogic.cs.mcgill.ca/beluga/

- the Coq implementation of Hybrid:

http://www.site.uottawa.ca/~afelty/HybridCoq/

compiled from these two papers:

Amy Felty, Alberto Momigliano, Brigitte Pientka

An Open Challenge Problem Repository for Systems Supporting Binders

http://doi.org/10.4204/EPTCS.185.2 (p. 18)

Brigitte Pientka, Joshua Dunfield

Beluga: A Framework for Programming and Reasoning with Deductive Systems

(System Description)

http://doi.org/10.1007/978-3-642-14203-1_2 (p. 16)

A logical framework by Robin Adams:

Robin Adams

Lambda-Free Logical Frameworks

http://arxiv.org/abs/0804.1879v2

Some interesting papers by Frank Pfenning et al.:

Frank Pfenning, Conal Elliott (1988)

Higher-Order Abstract Syntax

http://doi.org/10.1145/53990.54010 and

http://www.cs.cmu.edu/~fp/papers/pldi88.pdf

Frank Pfenning (1996)

The Practice of Logical Frameworks

http://doi.org/10.1007/3-540-61064-2_33 and

http://www.cs.cmu.edu/~fp/papers/caap96.pdf

Frank Pfenning, Carsten Schürmann (1999)

System Description: Twelf – A Meta-Logical Framework for Deductive Systems

http://doi.org/10.1007/3-540-48660-7_14 and

http://www.cs.cmu.edu/~fp/papers/cade99.pdf

Frank Pfenning (2002)

Logical Frameworks - A Brief Introduction

http://doi.org/10.1007/978-94-010-0413-8_5 and

http://www.cs.cmu.edu/~fp/papers/mdorf01.pdf

According to Pfenning and Elliott (1988), higher-order abstract syntax has an

even more expressive power than Isabelle's λ-calculus: "Isabelle [18] uses a

representation similar to ours for the statement of rules, and uses

higher-order unification for deduction. Isabelle's λ-calculus representation

does not have the expressive power of higher-order abstract syntax, but

explicitly encodes quantifier dependencies."

> Am 12.03.2018 um 23:41 schrieb R. Pollack <rpol...@gmail.com>:

>

> Ken,

>

> You should know about the Edinburgh Logical Framework (ELF), best implemented in the Twelf system. While ELF is a particular framework, there is tons of work about specification and programming in dependently typed frameworks. See e.g. many papers by Frank Pfenning, Amy Felty, Bob Harper, Brigitte Pientka, Alberto Momigliano. There is also a lot of work about other simply typed frameworks; e.g. Abella. There is a lot to say about consistency, expressiveness and usability of frameworks.

>

> You haven't even scratched the surface of logical frameworks.

>

> --Randy

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu