Email Gateway (Oct 23 2025 at 15:23): Email Gateway (Oct 23 2025 at 15:23):From: "John F. Hughes" <jfh@cs.brown.edu>
I need a little setup to ask this question. I'll try to make it brief:
In projective geometry, there are four basic axioms, P1 ... P4, for a
projective plane. P1, for instance, says that given two distinct points,
there's a unique line containing both. P2 says that given two distinct
lines, there's at least one point that lies on both. A short proof using P1
shows that P2 can be strengthened to say that given two distinct lines,
there's a unique point lying on both.
We can swap the words "point" and "line" and the phrases "lies on" and
"contains" in any statement about a projective plane to get a so-called
"dual" statement. So P2 is the dual to P1. As it happens, the duals to P3
and P4 are also true in any projective plane, so if we have a set Pts of
point and Lns of lines, and a 'liesOn' predicate which together constitute
a projective plane Pi, then the set Lns, the set Pts, and 'contains'
also constitute
a projective plane, the 'dual' plane, called Pi*. I've got a locale,
"pplane" that takes a set of points, a set of lines, and a 'liesOn'
relation, so this can be stated as
theorem
This also means that any theorem about projective planes also has a 'dual'
theorem, gotten by replacing "point" with "line" and vice-version, and
doing the same for "lies on" and "contains". Because the duals of the
axioms are also facts, we get a conclusion that if some theorem S is true
for all projective planes, then so is the dual statement.
Hartshorne's little book about projective geometry says it like this
(please ignore the mention of P5):
[image: image.png]
More important is the corollary:
[image: image.png]
My question is this: is it possible to formulate such a theorem in
Isabelle? The statement of the corollary could actually be strengthened to
say that the proof of S* consists of simply dualizing the proof of S
(i.e., swap point/line, etc., in every fact in that proof).
I haven't, in my wanderings through Isabelle, seen anything that seems to
do this kind of introspection, i.e., that treats an Isabelle proof or
statement as an object that can be transformed/acted on by various
functions, etc. Then again, I may simply be looking in the wrong places.
I'd appreciate any suggestions, *or *reasons why this sort of thing cannot
be done.
--John
Email Gateway (Oct 23 2025 at 15:32):From: "John F. Hughes" <jfh@cs.brown.edu>
apologies...I cut myself off mid-edit. The claim was that I could write
this initial claim about duality as a small theorem:
[image: image.png]
On Thu, Oct 23, 2025 at 11:22 AM John F. Hughes <jfh@cs.brown.edu> wrote:
I need a little setup to ask this question. I'll try to make it brief:
In projective geometry, there are four basic axioms, P1 ... P4, for a
projective plane. P1, for instance, says that given two distinct points,
there's a unique line containing both. P2 says that given two distinct
lines, there's at least one point that lies on both. A short proof using P1
shows that P2 can be strengthened to say that given two distinct lines,
there's a unique point lying on both.We can swap the words "point" and "line" and the phrases "lies on" and
"contains" in any statement about a projective plane to get a so-called
"dual" statement. So P2 is the dual to P1. As it happens, the duals to P3
and P4 are also true in any projective plane, so if we have a set Pts of
point and Lns of lines, and a 'liesOn' predicate which together constitute
a projective plane Pi, then the set Lns, the set Pts, and 'contains'
also constitute a projective plane, the 'dual' plane, called Pi*. I've
got a locale, "pplane" that takes a set of points, a set of lines, and a
'liesOn' relation, so this can be stated as
theoremThis also means that any theorem about projective planes also has a 'dual'
theorem, gotten by replacing "point" with "line" and vice-version, and
doing the same for "lies on" and "contains". Because the duals of the
axioms are also facts, we get a conclusion that if some theorem S is true
for all projective planes, then so is the dual statement.Hartshorne's little book about projective geometry says it like this
(please ignore the mention of P5):
[image: image.png]
More important is the corollary:
[image: image.png]My question is this: is it possible to formulate such a theorem in
Isabelle? The statement of the corollary could actually be strengthened to
say that the proof of S* consists of simply dualizing the proof of S
(i.e., swap point/line, etc., in every fact in that proof).I haven't, in my wanderings through Isabelle, seen anything that seems to
do this kind of introspection, i.e., that treats an Isabelle proof or
statement as an object that can be transformed/acted on by various
functions, etc. Then again, I may simply be looking in the wrong places.
I'd appreciate any suggestions, *or *reasons why this sort of thing
cannot be done.
--John
Email Gateway (Oct 24 2025 at 06:32):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Your theorem can be stated exactly as below if pplane is formalized as a
locale. This would be the standard way in Isabelle, in my opinion.
As for the proofs, the obvious problem is that in Isabelle "proof
objects" are not the preferred point of view, proving is rather a
computation (in the sense of LCF, logic for computable functions).
However, the fact that the locale can be interpreted in the dual way
"morally" means just what you want: any proof in the locale pplane is
exactly the same independently of how the parameters are instantiated.
To stress this you could call the parameters of the locale in some
abstract way, like objects_one, objects_two, myrelataion, and then to
show that both dual instantiations interpret your locale.
Stepan
On 23-Oct-25 5:31 PM, John F. Hughes wrote:
apologies...I cut myself off mid-edit. The claim was that I could
write this initial claim about duality as a small theorem:
image.pngOn Thu, Oct 23, 2025 at 11:22 AM John F. Hughes <jfh@cs.brown.edu> wrote:
I need a little setup to ask this question. I'll try to make it
brief:In projective geometry, there are four basic axioms, P1 ... P4,
for a projective plane. P1, for instance, says that given two
distinct points, there's a unique line containing both. P2 says
that given two distinct lines, there's at least one point that
lies on both. A short proof using P1 shows that P2 can be
strengthened to say that given two distinct lines, there's a
unique point lying on both.We can swap the words "point" and "line" and the phrases "lies on"
and "contains" in any statement about a projective plane to get a
so-called "dual" statement. So P2 is the dual to P1. As it
happens, the duals to P3 and P4 are also true in any projective
plane, so if we have a set Pts of point and Lns of lines, and a
'liesOn' predicate which together constitute a projective plane
Pi, then the set Lns, the set Pts, and 'contains'
/also/ constitute a projective plane, the 'dual' plane, called
Pi*. I've got a locale, "pplane" that takes a set of points, a set
of lines, and a 'liesOn' relation, so this can be stated as
theoremThis also means that any theorem about projective planes also has
a 'dual' theorem, gotten by replacing "point" with "line" and
vice-version, and doing the same for "lies on" and "contains".
Because the duals of the axioms are also facts, we get a
conclusion that if some theorem S is true for all projective
planes, then so is the dual statement.Hartshorne's little book about projective geometry says it like
this (please ignore the mention of P5):
image.png
More important is the corollary:
image.pngMy question is this: is it possible to formulate such a theorem in
Isabelle? The statement of the corollary could actually be
strengthened to say that the /proof/ of S* consists of simply
dualizing the proof of S (i.e., swap point/line, etc., in every
fact in that proof).I haven't, in my wanderings through Isabelle, seen anything that
seems to do this kind of introspection, i.e., that treats an
Isabelle proof or statement as an object that can be
transformed/acted on by various functions, etc. Then again, I may
simply be looking in the wrong places. I'd appreciate any
suggestions, *or *reasons why this sort of thing cannot be done.
--John
Email Gateway (Oct 24 2025 at 09:40):From: "John F. Hughes" <jfh@cs.brown.edu>
Thanks for your comments.
I have indeed made a locale called "pplane", and the "dual_is_plane"
theorem has been written and proved, so I've formalized Hartshorne's
Proposition 4.1.
But it's his Corollary 4.2 that interests me (especially in the extended
form where one says "and the proof of the dual theorem is gotten by
dualizing each fact in the proof of the primal theorem") -- that is a
statement about theorems and proofs rather than about projective planes. As
a mathematician reading the book, I had no trouble believing Corr. 4.2, but
that's different from being able to formalize it.
At this point, if I have proved a theorem like
lemma prim: if Pi is a plane containing a line k and a point P not on k,
then there is a point Q such that Q is not on k and Q is not equal to P
I can then write its dual theorem by hand:
lemma dual: if Pi is a plane containing a point S and a line n not
containing S, then there is a line t such that t does not contain S and t
is not equal to n.
and there's a one-line Isabelle proof, using "prim" and "dual_is_plane".
But I do not know how to express, in Isabelle, that "no matter what primal
lemma I write, I will always be able to prove the dual with this same
one-line proof," which is the content of Corr. 4.2.
On Fri, Oct 24, 2025 at 2:26 AM Stepan Holub <holub@karlin.mff.cuni.cz>
wrote:
Your theorem can be stated exactly as below if pplane is formalized as a
locale. This would be the standard way in Isabelle, in my opinion.As for the proofs, the obvious problem is that in Isabelle "proof objects"
are not the preferred point of view, proving is rather a computation (in
the sense of LCF, logic for computable functions). However, the fact that
the locale can be interpreted in the dual way "morally" means just what you
want: any proof in the locale pplane is exactly the same independently of
how the parameters are instantiated. To stress this you could call the
parameters of the locale in some abstract way, like objects_one,
objects_two, myrelataion, and then to show that both dual instantiations
interpret your locale.Stepan
On 23-Oct-25 5:31 PM, John F. Hughes wrote:
apologies...I cut myself off mid-edit. The claim was that I could write
this initial claim about duality as a small theorem:
[image: image.png]On Thu, Oct 23, 2025 at 11:22 AM John F. Hughes <jfh@cs.brown.edu> wrote:
I need a little setup to ask this question. I'll try to make it brief:
In projective geometry, there are four basic axioms, P1 ... P4, for a
projective plane. P1, for instance, says that given two distinct points,
there's a unique line containing both. P2 says that given two distinct
lines, there's at least one point that lies on both. A short proof using P1
shows that P2 can be strengthened to say that given two distinct lines,
there's a unique point lying on both.We can swap the words "point" and "line" and the phrases "lies on" and
"contains" in any statement about a projective plane to get a so-called
"dual" statement. So P2 is the dual to P1. As it happens, the duals to P3
and P4 are also true in any projective plane, so if we have a set Pts of
point and Lns of lines, and a 'liesOn' predicate which together constitute
a projective plane Pi, then the set Lns, the set Pts, and 'contains'
also constitute a projective plane, the 'dual' plane, called Pi*. I've
got a locale, "pplane" that takes a set of points, a set of lines, and a
'liesOn' relation, so this can be stated as
theoremThis also means that any theorem about projective planes also has a
'dual' theorem, gotten by replacing "point" with "line" and vice-version,
and doing the same for "lies on" and "contains". Because the duals of the
axioms are also facts, we get a conclusion that if some theorem S is true
for all projective planes, then so is the dual statement.Hartshorne's little book about projective geometry says it like this
(please ignore the mention of P5):
[image: image.png]
More important is the corollary:
[image: image.png]My question is this: is it possible to formulate such a theorem in
Isabelle? The statement of the corollary could actually be strengthened to
say that the proof of S* consists of simply dualizing the proof of S
(i.e., swap point/line, etc., in every fact in that proof).I haven't, in my wanderings through Isabelle, seen anything that seems to
do this kind of introspection, i.e., that treats an Isabelle proof or
statement as an object that can be transformed/acted on by various
functions, etc. Then again, I may simply be looking in the wrong places.
I'd appreciate any suggestions, *or *reasons why this sort of thing
cannot be done.
--John
Email Gateway (Oct 24 2025 at 11:09):From: Fabian Huch <huch@in.tum.de>
Although theorems in Isabelle/HOL can represent proof rules, the actual
proofs are not part of the term language.
Instead, the basic inference rules are functions of the meta-language
that produce objects of the (meta-level) type 'thm'. Objects of type
'thm' can only be produced by those inference rules, so every 'thm' is
correct by construction, and no actual proof is carried around in the
logical system.
That means, in Isabelle/HOL you cannot express this property -- i.e.,
that something is provable, or how -- as a theorem. You can only express
that something holds, e.g. that a property implies its dual.
Fabian
On 10/24/25 11:39, John F. Hughes wrote:
Thanks for your comments.
I have indeed made a locale called "pplane", and the "dual_is_plane"
theorem has been written and proved, so I've formalized Hartshorne's
Proposition 4.1.But it's his Corollary 4.2 that interests me (especially in the
extended form where one says "and the proof of the dual theorem is
gotten by dualizing each fact in the proof of the primal theorem") --
/that/ is a statement about theorems and proofs rather than about
projective planes. As a mathematician reading the book, I had no
trouble believing Corr. 4.2, but that's different from being able to
formalize it.At this point, if I have proved a theorem like
lemma prim: if Pi is a plane containing a line k and a point P not on
k, then there is a point Q such that Q is not on k and Q is not equal to PI can then /write/ its dual theorem by hand:
lemma dual: if Pi is a plane containing a point S and a line n not
containing S, then there is a line t such that t does not contain S
and t is not equal to n.and there's a one-line Isabelle proof, using "prim" and
"dual_is_plane". But I do not know how to express, in Isabelle, that
"no matter what primal lemma I write, I will /always/ be able to prove
the dual with this same one-line proof," which is the content of Corr.
4.2.On Fri, Oct 24, 2025 at 2:26 AM Stepan Holub
<holub@karlin.mff.cuni.cz> wrote:Your theorem can be stated exactly as below if pplane is
formalized as a locale. This would be the standard way in
Isabelle, in my opinion.As for the proofs, the obvious problem is that in Isabelle "proof
objects" are not the preferred point of view, proving is rather a
computation (in the sense of LCF, logic for computable functions).
However, the fact that the locale can be interpreted in the dual
way "morally" means just what you want: any proof in the locale
pplane is exactly the same independently of how the parameters are
instantiated. To stress this you could call the parameters of the
locale in some abstract way, like objects_one, objects_two,
myrelataion, and then to show that both dual instantiations
interpret your locale.Stepan
On 23-Oct-25 5:31 PM, John F. Hughes wrote:
apologies...I cut myself off mid-edit. The claim was that I could
write this initial claim about duality as a small theorem:
image.pngOn Thu, Oct 23, 2025 at 11:22 AM John F. Hughes
<jfh@cs.brown.edu> wrote:I need a little setup to ask this question. I'll try to make
it brief:In projective geometry, there are four basic axioms, P1 ...
P4, for a projective plane. P1, for instance, says that given
two distinct points, there's a unique line containing both.
P2 says that given two distinct lines, there's at least one
point that lies on both. A short proof using P1 shows that P2
can be strengthened to say that given two distinct lines,
there's a unique point lying on both.We can swap the words "point" and "line" and the phrases
"lies on" and "contains" in any statement about a projective
plane to get a so-called "dual" statement. So P2 is the dual
to P1. As it happens, the duals to P3 and P4 are also true in
any projective plane, so if we have a set Pts of point and
Lns of lines, and a 'liesOn' predicate which together
constitute a projective plane Pi, then the set Lns, the set
Pts, and 'contains' /also/ constitute a projective plane, the
'dual' plane, called Pi*. I've got a locale, "pplane" that
takes a set of points, a set of lines, and a 'liesOn'
relation, so this can be stated as
theoremThis also means that any theorem about projective planes also
has a 'dual' theorem, gotten by replacing "point" with "line"
and vice-version, and doing the same for "lies on" and
"contains". Because the duals of the axioms are also facts,
we get a conclusion that if some theorem S is true for all
projective planes, then so is the dual statement.Hartshorne's little book about projective geometry says it
like this (please ignore the mention of P5):
image.png
More important is the corollary:
image.pngMy question is this: is it possible to formulate such a
theorem in Isabelle? The statement of the corollary could
actually be strengthened to say that the /proof/ of S*
consists of simply dualizing the proof of S (i.e., swap
point/line, etc., in every fact in that proof).I haven't, in my wanderings through Isabelle, seen anything
that seems to do this kind of introspection, i.e., that
treats an Isabelle proof or statement as an object that can
be transformed/acted on by various functions, etc. Then
again, I may simply be looking in the wrong places. I'd
appreciate any suggestions, *or *reasons why this sort of
thing cannot be done.
--John
Last updated: Nov 09 2025 at 20:21 UTC