Re: [isabelle] Proving consistency
On Thu, 2010-08-19 at 15:50 +0100, John Munroe wrote:
> 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?
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and