Email Gateway (Aug 22 2022 at 19:18): Email Gateway (Aug 22 2022 at 19:18):From: "John F. Hughes" <jfh@cs.brown.edu>
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
Email Gateway (Aug 22 2022 at 19:18):From: Manuel Eberl <eberlm@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC