# [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.*