Email Gateway (Aug 19 2020 at 13:16): Email Gateway (Aug 19 2020 at 13:16):From: Georgy Dunaev <georgedunaev@gmail.com>
Dear all,
Previously I've asked for some help in similar question which is not well
formulated due to some linguistic difficulties:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-March/msg00106.html
(
https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/ZF/IFOL.html
)
But now I've wrote a small pdf about what exactly I hope to obtain (This
unfinished draft explains what exactly I want): (It is also attached to the
letter.)
https://github.com/georgydunaev/TRANSLATION/releases/download/0.1/translation.pdf
(Sources are here https://github.com/georgydunaev/TRANSLATION , I compile
with use of TexMaker.)
I want the translation function from Isabelle/ZF terms to
metatheorems about formulas of some predicate calculus. The set of
metatheorems about derivability of ZF f1st-order set theory is (badly)
called FOLFormulas.
( Details: There are countable amount of variables, formulas "forall x.
x=x" and "forall y. y=y" are not equal. There is one set of variables,
some are bounded and all the other are free.)
I feel like it exists, but I want it to be strictly defined at least once.
I believe it is important to have such a function explicitly, do you agree?
(In other words, the function is some program that rewrites terms to more
primitive, but more common form. Without recursive contexts, etc.) Are my
overall idea ok? How to treat symbols which type is not i, not [i,..,i]=>i
and not [i,..,i]=>o ?
Sincerely Yours,
Georgy Dunaev
translation.tex
translation.pdf
Email Gateway (Aug 20 2020 at 11:58):From: Georgy Dunaev <georgedunaev@gmail.com>
Dear All,
I am sorry about that letter about the translation: now I understand, that
it is very easy,
For example: this theorem
theorem enlight : "⋀n::o⇒o. (⋀P::o. (P⟶n(P))) ⟹ (⋀P::o. (P⟶n(n(P))))"
proof
fix n
assume H1:"(⋀P::o. (P⟶n(P)))"
fix P
assume H2:"P"
have H3:"n(P)"
by (rule mp[OF H1 H2])
show H4:"n(n(P))"
by (rule mp[OF H1 H3])
qed
should be translated as
$$\forall n : Fm->Fm. (\forall P\in Fm. T \vdash (P --> n(P)) ) -->
(\forall P\in Fm. T \vdash (P --> n(n(P))) )$$, where functions are
partial(n, for example) and \vdash is derivability in case that all
arguments of partial functions are in their domains.
So it is easy, indeed.
I think it is possible to implement(in Ocaml) such a function(let's call it
"t") in the Isabelle system, which will translate theorems of Isabelle/ZF
to theorems about Isabelle/ZF, but still inside the Isabelle/ZF.
So, what do you think about such a function t? May it be handy for some
applications?
Maybe the left-inverse function of t is also useful. It allows lifting of
proved theorems to the metatheory!
Kind regards,
Georgy Dunaev
Email Gateway (Aug 20 2020 at 14:35):From: Lawrence Paulson <lp15@cam.ac.uk>
I guess as the main proprietor of Isabelle/ZF I should answer this, but I don’t know what to say.
Such a translation might be feasible, but I don’t know what the applications for it would be.
Larry
Last updated: Apr 16 2024 at 08:18 UTC