Re: [isabelle] Fwd: Question about Type Theory behind Isabelle

On 30/09/2019 21:48, Georgy Dunaev wrote:
> I've read Stefan Berghofer's paper
> ,
> it has great calculus on page 7.

A more up-to-date version (with more explanations and references) is the
"implementation" manual, chapter 2 "Primitive Logic". (E.g. see the
Documentation panel in Isabelle/jEdit).

> 3) And last, most important: please explain the rule with sigma from that
> calculus.
> What is $\Sigma(c) [\vec{\tau}_n / \vec{\alpha}_n] $. ?  What does it mean?
> Sigma is greek so it is a set of predicate variables.... I don't understand
> meaning of the formula "any set of terms which depend on proof(!) constant
> with any amount of types instead of atomic types". What does it mean?

That is the "axiom" rule in the above document; see also page 74 (top):

   The axiomatization of a theory is implicitly closed by forming all
instances of type and term variables

The consequence are admissible type-instantiation rules, also explained
in that section.

> Could someone clarify this whole constants' mechanism?

In the context of proof terms, "constants" are often "theorem" constants
(axioms or proven theorems). Plain term constants are also possible.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.