Email Gateway (Aug 23 2022 at 08:31): Email Gateway (Aug 23 2022 at 08:31):From: Joshua Chen <josh@joshchen.io>
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.
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
Date: Mon, 23 Mar 2020 23:23:45 +0300
From: Georgy Dunaev <georgedunaev@gmail.com>
Subject: [isabelle] What does Isabelle's statement mean? (semantics,
def of truth, interpretation)
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID:
<CAAMrf_35L8os7DR5mORobXkx6=4RrC0zfzbyGNme9J+Jsk8z3A@mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"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: Nov 21 2024 at 12:39 UTC