Email Gateway (Aug 23 2022 at 08:40): Email Gateway (Aug 23 2022 at 08:40):From: Georgy Dunaev <georgedunaev@gmail.com>
Hello,
The question is about Isabelle underlying logic. (I think it is important
to understand it in full rather than blindly believe in Isabelle's
output...)
The screenshot of "Program Extraction in simply-typed Higher Order Logic"
by Stefan Berghofer is attached to this mail. (or may be found here:
https://postimg.cc/GBHgDjf5 , I've highlighted parts which are not obvious
for me)
A) What does it mean "substitute a few atomic types of a constant with a
few complex types"?
B) What does it mean "Sigma and c in parenthesis followed by substitution"?
C) Are these substitutions are real ones or just sequence of symbols?(like
some kind of label) I am sure that 5th is real one, but what about the
others?
Some very simple examples of derivation will help a lot!
By the way, can one recall what are known theorems about this very
important formal system? I.e. which useful properties it has? (Any
references are highly appreciated!)
Sincerely yours,
G D
myquestion.png
Email Gateway (Aug 23 2022 at 08:40):From: Makarius <makarius@sketis.net>
The material by Stefan Berghofer is approx. 20 years old. A more up-to-date
version of it is in the official Isabelle documentation, see chapter 2
"Primitive Logic" in the "implementation" manual
http://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/implementation.pdf
Substitution rules are mention in the text for figure 2.4.
Note that even if you "understand that in full", it will be only a tiny part
of the Isabelle system as a whole.
Isabelle users are living in the illusion of working directly with logic, but
the reality is quite different: the majority of concepts are extra-logical,
building a huge pyramid of towers on top of each other. A nice illustration of
this is in the slides by Tom Hales for BigProof 2019:
https://www.icms.org.uk/downloads/bigproof/Hales.pdf on page 16.
Makarius
Last updated: May 06 2024 at 20:16 UTC