Email Gateway (Aug 23 2022 at 08:31): Email Gateway (Aug 23 2022 at 08:31):From: Makarius <makarius@sketis.net>
On 23/03/2020 21:23, Georgy Dunaev wrote:
What is the precise definition of truthfulness of an Isabelle's expression?
Could you please help me to translate the following expressions in
set-theoretic language:
"(A==>B)==>(A-->B)"
"(!!x. P(x))==>(\forall x. P(x))" ?
This is a formal notation for Natural Deduction rules, see also section 2.4 in
the "implementation" manual.
Most Isabelle object-logics can work with that format directly, even
Isabelle/ZF. (These days I say more often "Isabelle application environment"
instead of the more traditional "object-logic".)
But I need a precise translation from syntax to semantics in this language.
(I am talking about Isabelle/FOL or ZF if it matters.)I need an interpretation.
If you want you can just collapse everything: identify type "prop" with "o"
and use the identity function for "Trueprop" etc.
In that view, the explicit structure merely helps to compose proofs, e.g. in
the Isar proof language or with proof methods like "rule" or "blast".
Makarius
Email Gateway (Aug 23 2022 at 08:32):From: Joshua Chen <josh@joshchen.io>
My sincerest apologies for forgetting to change the subject line!
Josh
The setting for thinking about logical frameworks is different from that
of traditional (first-order, classical, set-theoretic) model theory, so
asking for set-theoretic interpretations of the sentences you give is
not exactly an answerable question. Though if one really wants, one may
think about ==>, !! as being the "actual" (meta) implication and
universal quantifier, and -->, \forall as being their Gödel encodings.
I recommend https://ncatlab.org/nlab/show/logical+framework as a good
intro to the general ideas and for references.
Cheers,
Josh
Email Gateway (Aug 23 2022 at 08:32):From: Joshua Chen <josh@joshchen.io>
By which I of course mean that sentences involving -->, \forall are
Gödel encodings of their counterparts that involve ==>, !!. Then you
might choose to read
(A ==> B) ==> (A --> B)
as being the meta-statement that "the encoding of 'A ==> B' is derivable
if A implies B", and similarly for (!!x. P(x)) ==> (\forall x. P(x)).
Josh
Email Gateway (Aug 23 2022 at 08:32):From: Lawrence Paulson <lp15@cam.ac.uk>
Could you please help me to translate the following expressions in
set-theoretic language:
"(A==>B)==>(A-->B)"
It’s best to include the implicit (and normally hidden) coercion, Trueprop:
"(Trueprop A ==> Trueprop B) ==> Trueprop (A-->B)”
Since ==> is ordinary implication (in the meta-logic), this axiom expresses part of the truth table for —>.
"(!!x. P(x))==>(\forall x. P(x))”
This one is
"(!!x. Trueprop (P x)) ==> Trueprop (\forall x. P(x))”
and similarly expresses that (\forall x. P(x)) must be true whenever (P x) is true for all x.
More information in the paper https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/chap700.pdf
Larry
Email Gateway (Aug 23 2022 at 08:32):From: Georgy Dunaev <georgedunaev@gmail.com>
Thanks for your response, but it is not exactly what I am looking for...
Types, terms and proofs of Isabelle may be encide in Z(FC) themselves. They
are syntactic objects. But they also has to have some precise "meaning",
i.e. semantics. Which is also encoded in zfc. What is the function between
these two sets?
In order to overcome the language barrier I've to ask similar question:
What is a model of the natural deduction which is used in Isabelle? Does it
exist? By model I mean a set with structure, like in model theory. Maybe
there is an article with precise definition of such model?
There certainly should be a soundness theorem and a completeness theorem
for this system... :/
Thanks!
Yours sincerely,
G. D.
Email Gateway (Aug 23 2022 at 08:32):From: Lawrence Paulson <lp15@cam.ac.uk>
As I mentioned earlier, the key paper is this one:
https://link.springer.com/article/10.1007%2FBF00248324
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.html
I describe Isabelle’s meta-logic as “intuitionistic higher-order logic”. Here “intuitionistic” means that the excluded middle isn’t assumed, but this logic still has classical models too, including Church’s original (1940) model for simple type theory.
So you have both a semantic explanation and also (in the paper) a proof-theoretic explanation of how it all works.
Larry Paulson
Email Gateway (Aug 23 2022 at 08:47):From: Georgy Dunaev <georgedunaev@gmail.com>
Hello!
What is the precise definition of truthfulness of an Isabelle's expression?
Could you please help me to translate the following expressions in
set-theoretic language:
"(A==>B)==>(A-->B)"
"(!!x. P(x))==>(\forall x. P(x))" ?
Intuitively, I know that 1st is the deduction theorem, and the 2nd is
generalisation rule.
But I need a precise translation from syntax to semantics in this language.
(I am talking about Isabelle/FOL or ZF if it matters.)
I need an interpretation.
I know interpretation for object language: that is called models and it is
about sets, functions on them and predicates on them. I need something
similar. I feel that the definition of valid expressions is somehow
extended from object language to the metalanguage.
Thanks!
Sincerely yours,
Georgy Dunaev
Last updated: Apr 25 2024 at 12:23 UTC