Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Cl-isabelle-users Digest, Vol 177, Issue 21


view this post on Zulip 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: Mar 28 2024 at 16:17 UTC