Re: [isabelle] Using implications



On Wed, Jan 26, 2011 at 10:14 AM, Eg Gloor <egglue at gmail.com> wrote:
> axiomatization
> S :: "real set" and
> foo :: "real => real" and
> bar :: "real => real" and
> bax :: "real => real" and
> c :: real
> where ax1: "ALL f g. (ALL x y. x > c & y > c <-> f x = g y) --> f = g"
> and ax2: "ALL a b. bax a > c & bax b > c <-> foo (bax a) = bar (bax b)"

Once again, we see that axioms are evil. Your ax1 is already
inconsistent all by itself:

lemma "False"
proof -
  let ?f = "%x::real. if x > c then (0::real) else 1"
  let ?g = "%x::real. if x > c then (0::real) else 2"
  have "?f = ?g"
    by (rule ax1 [rule_format], simp)
  hence "?f c = ?g c"
    by (rule arg_cong)
  thus "False"
    by simp
qed

- Brian





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