Email Gateway (Aug 19 2022 at 08:23): Email Gateway (Aug 19 2022 at 08:23):From: John Munroe <munddr@gmail.com>
Hi,
Is it correct to say that there's object-level reasoning done in
Isabelle? It seems that each step in an object-level proof is written
using meta-level notations. Does that mean proving an object-level
sentence involves only meta-level reasoning?
Thanks a lot for your time.
John
Email Gateway (Aug 19 2022 at 08:24):From: John Munroe <munddr@gmail.com>
Thanks, Randy. You're right that I'm not clear on the terms meta-level
and object-level.
So if I have, e.g.,
const P :: "nat => bool"
lemma "P x = True"
Would you say that I'm actually encoding an object-level sentence in
the meta-level? That is, I'm essentially translating the object-level
sentence "\forall x. P(x) = True" into Isabelle's notations, and thus
"using the meta-level language only to talk about the object level".
Regarding the way the object-level is represented in the meta-level
and how unification in the meta-level are reflected in the
object-level, that's all down to using Pure, right? A short
clarification will be much appreciated.
Thanks a lot for your time.
John
Last updated: Nov 21 2024 at 12:39 UTC