Re: [isabelle] Decidability



On 06/03/2019 21:56, John F. Hughes wrote:
> (* One has a type of points *)
> typedecl "points"
> (* One has a type of lines *)
> typedecl "lines"
> (* There is a relation of incidence between points and lines *)
> consts incid :: "points ⇒ lines ⇒ bool"
>  axiomatization where
> (* The relation of incidence is decidable *)
> incid_dec: "(incid P l) ∨ ¬(incid P l)"

This use of "typedecl" and "axiomatization" is somewhat "old-fashioned".
These days, one would probably just use a locale for this kind of thing,
which has the advantage of being modular in the sense that you can
actually give different interpretations for these constants instead of
axiomatising them in the logic.

> That last axiom seems to me to follow from the nothing that "incid" is a
> function, and that {True, False} is its codomain. Can someone explain to me
> why this might not be so?

It follows from the law of the excluded middle. This is an axiom in HOL,
so it is superfluous here. My guess would be that the author comes from
the word of constructive type theory (e.g. Coq); the comment about
"decidability" of incidence certainly seems to suggest that. In a system
like Coq, the statement "P x ∨ ¬P x" is not necessarily true for all P
and if it is true, it means that P is a decidable predicate.

It seems to me that the style of this AFP entry is a bit unidiomatic for
Isabelle/HOL.

(Disclaimer: I don't actually know very much about Coq and constructive
type theory. I hope what I said is mostly correct)

Manuel




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