Email Gateway (Aug 18 2022 at 15:52): Email Gateway (Aug 18 2022 at 15:52):From: John Munroe <munddr@gmail.com>
Hi all,
I was wondering how consistency can be proved in general. For example,
for the following simple setup:
locale A =
fixes a :: real
and b :: real
assumes ax1: "a > 0 & b > 0"
and ax2: "a + b > 0"
What is the theorem for proving that A is consistent? On paper, I'd
like to show that I can't prove False from A, but how can that be done
in practice?
Thank you in advance,
John
Email Gateway (Aug 18 2022 at 15:52):From: Benedikt N <bnord01@googlemail.com>
In this case simply proving that there exists an instance of A.
If you could prove False from A and there exists an instance of A then
you would have proven False in Isabelle.
And thereby proving that Isabelle is inconsistent.
Of which you have to believe that it isn't the case if you want to
prove anything with it. ;)
Benedikt
Email Gateway (Aug 18 2022 at 15:52):From: Tjark Weber <webertj@in.tum.de>
It can't (Goedel's second incompleteness theorem comes to mind).
But you can easily prove consistency relative to higher-order logic by
providing a model of your axioms. For instance, a=1 and b=1 makes your
axioms true. To give a formal proof in Isabelle, simply say
interpretation A 1 1
by (unfold_locales, auto)
Tjark
Last updated: Apr 30 2024 at 04:19 UTC