[isabelle] Proving consistency



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





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