Email Gateway (Aug 22 2022 at 20:30): Email Gateway (Aug 22 2022 at 20:30):From: Georgy Dunaev <georgedunaev@gmail.com>
I've read Stefan Berghofer's paper
http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf ,
it has great calculus on page 7.
1) Does exist more detailed book or paper on this calculus?
2) I will also highly appreciate any reference to e.g. correctness theorem
of this calculus.
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?
Could someone clarify this whole constants' mechanism?
Thanks!
Georgy Dunaev
Email Gateway (Aug 22 2022 at 20:42):From: Makarius <makarius@sketis.net>
On 30/09/2019 21:48, Georgy Dunaev wrote:
I've read Stefan Berghofer's paper
http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf ,
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.
Makarius
Last updated: Apr 27 2024 at 01:05 UTC