[isabelle] refute refutes my simple axiom



Hi,

So if you have something inconsistent, you get to experience both the cheap thrills of sledgehammer, and the dashing of your naive dreams with refute. Still, automation is great. You want your naivety demolished as soon as possible.

Refute is finding a model. I simplified everything down to a theorem which states a simple axiom as an exists instead of a forall, and refute finds a model, although metis proves the theorem. I don't know how to interpret the results of refute. Here's the theory.

typedecl sT

axiomatization
empty_set::sT and
inS::"sT => sT => bool" (infixl "∈⇣σ" 55)
where
empty_ax:"!(x::sT). ~(x ∈⇣σ empty_set)"

theorem --"refute finds a model"
"~(?(x::sT). x ∈⇣σ empty_set)"
nitpick
refute
oops

theorem --"metis proves it."
"~(?(x::sT). x ∈⇣σ empty_set)"
by (metis empty_ax)

Refute returns this message:

Model found:
Size of types: ?'b: 1, sT: 1
empty_set: sTs_1ax.sT0
op ∈⇣σ: {(sTs_1ax.sT0, {(sTs_1ax.sT0, True)})}

Can anyone tell me how to interpret the refute message? Is there documentation on the web that tells me how to read the output of an SAT solver?

Actually, it looks like it might be saying that the empty_set is an element of the empty_set.

I could try to come up with a fix based on that hunch, but I spent 3 or 4 hours before I figured out to simplified the theory to the bare bones. It would be nice to know for sure, and if anyone wants to tell me how to fix the problem, that would be okay.

Attached is the complete theory.

Regards,
GB




theory sTs_1ax
imports Main
begin
nitpick_params [verbose, timeout = 120]

sledgehammer_params [provers = "
  e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire
", slice=true, verbose=true, isar_proof=true, timeout=120]

declare[[show_brackets=true]]
declare[[show_types=true]]
declare[[show_consts=true]]

typedecl sT

axiomatization
  empty_set::sT and
  inS::"sT => sT => bool" (infixl "\<in>\<^isub>\<sigma>" 55)
  where
  empty_ax:"!(x::sT). ~(x \<in>\<^isub>\<sigma> empty_set)"

theorem --"refute finds a model"
  "~(? x. x \<in>\<^isub>\<sigma> empty_set)"
  nitpick
  refute
  oops

theorem --"metis proves it."
  "~(? x. x \<in>\<^isub>\<sigma> empty_set)"
  by (metis empty_ax)

end


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