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)

Tjark






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.