Email Gateway (Aug 18 2022 at 17:25): Email Gateway (Aug 18 2022 at 17:25):From: John Munroe <munddr@gmail.com>
Hi,
I have a general theorem proving/logic question: does it make sense to
have a proof obligation that checks for unprovability? For example,
the proof obligation may require that a particular sentence, like "f =
g" to be unprovable from a theory T, i.e. "T |+ f = g". Checking for
unprovability is undecidable, right? If such a constraint is
impractical, then is there a more practical formulation for checking
the same/similar property?
Thanks a lot
John
Email Gateway (Aug 18 2022 at 17:25):From: Mark.Janney@gdc4s.com
You could try to exhibit a model of T in which 'f = g' holds and then
exhibit another model of T in which 'f = g' does not hold. That's how
the 'parallel postulate' of Euclidian geometry was shown to be
unprovable from the other axioms.
Email Gateway (Aug 18 2022 at 17:25):From: John Thingstad <jpthing@online.no>
Yes it makes sense.. In stead of me going into detail I suggest you read
the short document the link points to.
www.cs.umd.edu/~gasarch/largeramsey/bovINTRO.pdf
Email Gateway (Aug 18 2022 at 17:25):From: Timothy McKenzie <tjm1983@gmail.com>
I'm currently doing this in Isabelle. The way I've chosen to do
it is using locales. I have a locale for (Tarski's axioms of) the
absolute plane. I've proven that the real Cartesian plane is an
instance of this locale and that it also satisfies Tarski's
version of "Euclid's axiom".
I've now defined a model of the hyperbolic plane, and I'm in the
process of proving that it's also an instance of my absolute plane
locale. Then I'll need to prove that it doesn't satisfy Euclid's
axiom.
Only my work on the hyperbolic plane is necessary to establish
that Euclid's axiom is unprovable in Tarski's theory of the
absolute plane, but my work on the Cartesian plane establishes
that the negation of Euclid's axiom is also unprovable from that
theory.
In all of this, I have to rely on the assumption that Isabelle/HOL
is consistent, but I guess all work in Isabelle/HOL makes that
assumption.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 17:25):From: John Munroe <munddr@gmail.com>
I see. Do you know where I can find the proof that shows that it's unprovable?
Thanks
John
Email Gateway (Aug 18 2022 at 17:26):From: Timothy McKenzie <tjm1983@gmail.com>
I'm not sure exactly what you're looking for. Are you after the
proof that Euclid's axiom is unprovable from Tarski's other axioms
of the plane? This is surprisingly difficult to find.
The version of Tarski's axioms I'm using is from Metamathematische
Methoden in der Geometrie by Schwabhäuser, Szmielew, and Tarski
(which is made slightly more difficult by the fact that I don't
speak German --- not yet, anyway). I'm told that the first
published version of Tarski's axioms was in The Axiomatic Method
(1959); from memory it was the second paper.
The following paper in The Axiomatic Method was Some
Metamathematical Problems Concerning Elementary Hyperbolic
Geometry, by Szmielew. She used a modified version of Tarski's
axioms, where Euclid's axiom was replaced with a hyperbolic axiom,
stronger than the negation of Euclid's axiom. Her theorem 2.15
states that a system is a model of these axioms of hyperbolic
space if and only if it's isomorphic with the Klein space of
appropriate dimension.
Unfortunately for me, her proof begins by asserting that it's
"well known" that the Klein space satisfies the hyperbolic version
of Tarski's axioms. It's a little difficult to see how it could
already be well known as soon as the axioms were first published.
(The proof goes on to show in more detail that every model of the
hyperbolic version of Tarski's axioms must be isomorphic to the
Klein space, which isn't the direction I need.)
Other publications (including Metamathematische Methoden in der
Geometrie) that state the result I want, or something closely
related, generally refer the reader to Szmielew's paper for the
"proof", which is frustrating.
Szmielew did partly make up for it, though. The book I'm finding
most useful in formalizing this independence result is Foundations
of Geometry by Borsuk & Szmielew (which I am grateful was
translated into English from the original Polish). It uses a
different set of axioms from Tarski's, but they're similar enough
to be helpful. The book describes the Klein-Beltrami model of the
hyperbolic plane, starting on page 245, and then checks that it
satisfies their axioms, starting on page 250.
In the process of formalizing the independence result in Isabelle,
I've found a few errors in Borsuk & Szmielew, but I guess this is
likely in any similar publication.
The Klein-Beltrami model of the hyperbolic plane is by no means
the only one. It's useful to me because it preserves betweenness,
which is one of the primitive relations in Tarksi's axioms. If
you're using a different set of axioms, another model might be
more useful.
Tim
<><
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC