[isabelle] Decidability



As a mathematician, I thought I had a decent idea of what a "function" was,
but perhaps I'm missing something important. Looking at

https://www.isa-afp.org/browser_info/current/AFP/Projective_Geometry/Projective_Space_Axioms.html

I see the following (slightly edited by thinning comments):

(* 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)"

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?

I'm quite happy with the notion that it might not be known to Isabelle
whether "incid P l" is True or False, and indeed, perhaps in some situation
where "incid" is described or characterized peculiarly, it might not be
possible for Isabelle to determine which of the two values it takes ---
exactly what Isabelle can compute is still baffling to me. But it seems to
me that if Isabelle is in fact modeling mathematical functions, then "incid
P l" is either True or False, in which case its negation is either False or
True respectively, hence the disjucntion is always True, and this needn't
be an additional axiom. So I'm a little bit mystified.

--John



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