Email Gateway (Aug 18 2022 at 19:25): Email Gateway (Aug 18 2022 at 19:25):From: Bill Richter <richter@math.northwestern.edu>
Hi, I'm a mathematician writing a rigorous axiomatic geometry paper
http://www.math.northwestern.edu/~richter/hilbert.pdf
using Hilbert's axioms. I want to cite geometry proofs nicely coded
and checked by proof-checker like Isabelle. I've written Mizar code
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
and I want to port it to Isabelle, which Freek Wiedijk seems to
suggest is an improvement. Makarius has been helping me, and he said
I should ask here about formalizations of geometry. My feeling, which
could be mistaken, is that Coq and HOL Light are primarily
theorem-provers (procedural) and require considerable tweaking to
allow folks to type in readable axiomatic geometry (declarative)
proofs, but that Isabelle is both procedural and declarative.
My Mizar code is a largely a port of Julien Narboux's Coq pseudo-code
http://dpt-info.u-strasbg.fr/~narboux/tarski.html. I partially prove
the theorem of the 1983 book Metamathematische Methoden in der
Geometrie by Schwabhäuser, Szmielew, and Tarski, that Tarski's
(extremely weak!) plane geometry axioms imply Hilbert's axioms. I get
about as far as Narboux, with Gupta's amazing proof which implies
Hilbert's axiom I1 that two points determine a line. I don't think my
Mizar code is that great, but it's a lot more readable than Julien's
Coq pseudo-code. No doubt some Mizar experts could improve my code,
but I'm putting them off as a last resort, because Mizar seems
unsuitable as a language to use in a high school math class.
So I'd appreciate your Isabelle help, including the easiest way run
Isabelle programs. Do I really need Proof General? I'll also accept
geometry help! I haven't seen Schwabhäuser's book, and I can't see
how to go any farther with Tarski's axioms. I'm basically missing
Hilbert's Pasch Betweenness axiom (Tarski's axiom is about 1/3 of it)
and Hilbert's angle construction axiom.
Email Gateway (Aug 18 2022 at 19:26):From: Ramana Kumar <rk436@cam.ac.uk>
No, I believe the modern way to run Isabelle is with the jEdit interface
that comes with the Isabelle distribution.
Email Gateway (Aug 18 2022 at 19:26):From: Bill Richter <richter@math.northwestern.edu>
I appreciate your work [...] Maybe we could join our efforts.
Julien, I'd be thrilled to work with you and Gabriel Braun, especially
as you & Makarius are on a committee studying Theorem Proving
Components for Educational Software. So you & Makarius are people I
want to talk to about teaching geometry, and not only vital
programming resources. This is very interesting:
I appreciate your work, your proofs seem to be really more readable
than Coq proofs. Of course my LCF style proofs are not meant to be
readable. In fact, I believe that these proofs about Tarski's
axioms are really low level and it is hard to have intuition about
the proofs because there are basic facts which are hard to prove
(for instance existence of the midpoint arrives only at chapter 7
!) and therefore it is not really the kind of proof one wants to
show in high-school, that is why I did not try to produce readable
proofs.
Surely no one should teach Tarski's axioms in high school, as the
proofs are way too hard since his axioms are so weak. But the Tarski
proofs are still worth understanding, for the same reason that high
school kids (arguably) ought to learn Hilbert's axioms and not use the
stronger axioms of Moise & Venema, based on Birkhoff's real line for
distances and angles, and taking the plane separation axiom instead of
Hilbert's weaker Pasch axiom.
Moise proofs are a lot easier than Hilbert proofs. But only using
Moise raises the question in the student's mind: am I smart enough to
understand the supposedly harder Hilbert axioms? And if I'm not smart
enough, maybe I shouldn't even be using the simpler Moise axioms!
The only way to reassure the students is to write up nice Hilbert proofs,
and I think I succeeded, or at least made a start, in
http://www.math.northwestern.edu/~richter/hilbert.pdf
The same remarks go for Tarksi, at least for me (the teacher). I know I
couldn't figure out the Tarski proofs myself, I needed your Coq code,
but am I even smart enough to understand the proofs?
I think there is definitely is Tarski geometry intuition, although
it's hard to come by. Gupta's amazing proof is definitely based on
intuition, and you can see the intuition in the pictures you and the
wikiproofs folks draw. Gupta's theorem
a ≠ b ∧ Babc ∧ Babd → Bacd ∨ Badc
would be easy if we could find two points p & q that are equidistant
from a, b & c. We could easily do that if we had Hilbert's angle
construction axiom, but we don't. So Gupta (as you explained to me in
your Coq code) first finds a rhombus (which turns out to be flat), and then
shows the diagonals of the rhombus bisect each other (that's generally
true, and in our flat case it follows easily from the Inner Pasch
axiom), and then we can do enough angle construction using this
bisected rhombus to find the points p & q, which turn out to be on the
same line after all. Isn't that an amazing proof?
Your email from last week reactivated my interest in these proofs
and I worked on the proof of Hilbert's Pasch axiom.
Excellent! I noticed that your proof of the full Pasch axiom in your
(in progress) http://dpt-info.u-strasbg.fr/~narboux/Tarski/Hilbert.html
seems to be still in progress.
Also, you didn't quite prove the midpoint theorem, but only
Lemma l7_25 : forall A B C, Cong C A C B -> exists X, is_midpoint X A B.
Your C should exist, by constructing an isosceles triangle, but I
can't even do that.
I don't know why my address from hol-info bounced, as I've gotten mail
from other hol-info users. Can you check what my bad address was?
About your questions about Isabelle, I think you could use the
latest use interface based on Jedit.
Thanks. Makarius told me this after I posted. I still don't know how
to use Isabelle. Makarius stressed that I ought to try Coq.
Email Gateway (Aug 18 2022 at 19:26):From: Bill Richter <richter@math.northwestern.edu>
they have built a large Coq library about high school geometry.
[...] But this [ Coq declarative proof] language is not used much
by the Coq community so you may encounter bugs.
Julien, I think that you and your coauthors in
http://hal.inria.fr/docs/00/58/49/18/PDF/iccsaConf.pdf are using Coq
to figure out how to teach the course, and not asking the students to
write Coq code proofs. This sentence in your paper concerns me:
The work closest to ours is the one by
P. Scott and J. Fleuriot [17].
http://www.springerlink.com/content/b715100716u1t347/?MUD=MP
I know I just got here, and I'm not trying to fight with anyone, but I
think this paper shows I have some value to the group already.
Scott and Fleuriot took on a challenging and interesting HOL Light
project, to fill in the gaps of Hilbert's book FoG. That will show
the power of HOL Light and their programming skill.
But their paper doesn't seem helpful in teaching a rigorous Hilbert
geometry course. Reading Greenberg's & Hartshorne's books (or my
paper http://www.math.northwestern.edu/~richter/hilbert.pdf) would
much more helpful. The authors don't seem to understand the gaps in
Euclid's work which were fixed by Hilbert's axioms. Euclid messed up
every single result that involved angle addition, including the
triangle sum theorem (sum 3 angles = 180). That's a result kids
taking a Hilbert geometry course need to know! The authors study
instead possible deficiencies of Hilbert's book FoG, and there may be
plenty, but you can't teach a geometry course out of FoG, as there
isn't enough interesting material. Euclid's errors are much more
interesting, as Euclid was often used as a textbook (for centuries?).
Scott and Fleuriot say something misleading in their intro:
Indeed, it is sufficient to note that Hilbert followed Euclid in
one pervasive omission: they both give proofs on an ambient plane
when the axioms characterise solid geometry [8].
First, they're citing Heath (a valuable Euclid resource), who mentions
Hilbert quite often but shows absolutely no understanding of how
Hilbert's work fixes Euclid's pervasive angle-addition errors.
Second, is there even an error, as Scott and Fleuriot quote Heath as
saying? I don't see any plane/solid-geometry error in Hilbert's
axioms listed http://en.wikipedia.org/wiki/Hilbert%27s_axioms
In my paper I explain (following Moise's rigorous book) how to handle
this solid geometry biz. Basically, for all the 2-dim stuff you have
to say "in a plane" and in the 3-dim part you then use the planar
stuff plus extra incidence axioms. Euclid's book XI is a fantastic
treatment of solid geometry, which Moise simplifies.
Email Gateway (Aug 18 2022 at 19:26):From: Josef Urban <josef.urban@gmail.com>
Hi Bill,
transforming the raw Mizar texts is often painful. Depending on
the application, it is often better to transform the XML layer or
even the Prolog (MPTP) layer. A simple XSL stylesheet that
implements your mizar->isar function is now at
https://raw.github.com/JUrban/xsl4mizar/master/ISA/isa_main.xsl .
Use it as follows:
git clone git://github.com/JUrban/xsl4mizar.git
mizf joe.miz
xsltproc xsl4mizar/addabsrefs.xsl joe.xml > joe.xml1
xsltproc --param display_thesis \'0\' xsl4mizar/ISA/isa_main.xsl
joe.xml1 | html2text
You can extend it by overloading in isa_main.xsltxt the other
printing functions from MHTML/. The API description is at
http://mizar.org/version/current/doc/xml/Mizar.html . I can
probably help with some harder parts if this leads somewhere.
This can only get you so far. For the general issues with
transforming the Mizar dependent type system to HOL-like systems,
see Ondrej Kuncar's paper:
http://ktiml.mff.cuni.cz/~kuncar/kuncar-wds10.pdf .
It might also be easier for you to first transform your code to
HOL Light's Mizar mode, because it does not have the keyword
incompatibilities that Isar introduced, and it has quite faithful
implementation of the Mizar "by" inference. In Isabelle, you
could later try to replace such calls with "metis" calls. If you are
interested in Coq, it also has a declarative Mizar-like mode, but it
is much less used than Isar.
And one more translation alternative: You could also ask the OMDoc
people (Florian Rabe I guess) about OMDoc->Isabelle export. They
do have quite fresh import of Mizar (using the XML layer).
Best,
Josef
Email Gateway (Aug 18 2022 at 19:27):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
At the end of February, I submitted my Master's thesis, which was about
an Isabelle formalization of the independence of the parallels
postulate. Specifically, I chose Tarski's axioms, and showed that his
Euclidean axiom (Axiom 10 in Metamathematische Methoden in der
Geometrie) is independent of the others, by proving that the
Klein--Beltrami model of the hyperbolic plane satisfies the rest of
Tarski's axioms, but not the Euclidean axiom.
As you will have gathered, my work was primarily about models of
Tarski's axioms, rather than consequences of them, but if you're
interested, ask me off-list, and I can send you a copy of my thesis, or
my Isabelle files, or whatever interests you. Please understand,
though, that I haven't heard back from the examiners yet, and I think
they're entitled to ask me to make changes to my thesis, so what I send
you shouldn't be considered to be the final version of my thesis.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:27):From: Bill Richter <richter@math.northwestern.edu>
Josef, as you're a real Mizar expert, I'll be grateful if you look at
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
I'll endure pain to manually transform my 1467 lines of Mizar Tarski
geometry proofs to Isabelle (or Coq or HOL Light even). I'm grateful
to the Mizar folks for writing a language I could learn and code up my
Tarski proofs, not least because I now believe my proofs. But I think
Mizar is too clunky a language to recommend high school students to
code in. That brings up HOL Light's Mizar mode, as you mentioned, or
Freek's miz3, but I couldn't get any of them to run on HOL Light 3.09,
nor could I compile the latest version of HOL Light, and Freek
suggests often that Isabelle is an improvement over Mizar.
Could you just get me started on Isabelle? I finally ran the
executable ./Isabelle, and up popped jedit. I'm reading various
Isabelle dox, and it's all great, but I haven't found what I want:
How do we code up first order logic (FOL) proofs that follow from some
FOL axioms? I really think the Isabelle dox ought to explain this.
You can't exactly do that in Mizar, I believe, and maybe you can't do
it in any of the proof assistants. Mizar is all about set theory
(using I think Tarski's FOL set theory axioms), so we have to talk
instead about a model of my FOL axioms. That's fine.
So we have to define some ``class'' of mathematical objects, which is
the sets, functions & relations that define a model. In my case,
that's a set S with a 3-ary and 4-ary relation equiv and between
satisfying various properties (Tarski's axioms). Now we have to code
up proofs about this class i.e. prove theorems about models of
Tarski's axioms, which amounts to the FOL proofs we want. This must
be explained somewhere in the Isabelle dox.
Email Gateway (Aug 18 2022 at 19:27):From: Bill Richter <richter@math.northwestern.edu>
Tim, that sounds great! Please send me anything you like privately.
I'd love to look at your code. But if you know the answer to the
question I just posted, please post the answer on the list. How in
Isabelle do we define models of some FOL axioms and then prove
theorems about the models? And feel free to post an answer to my
geometry questions too! How in Tarski's axioms do you prove Hilbert's
full Pasch axiom and angle construction axiom from Tarksi's?
Email Gateway (Aug 18 2022 at 19:27):From: Makarius <makarius@sketis.net>
These are not "keyword incompatibilities", but fundamental differences in
the approach to structured proofs, and the meaning of the language
elements. It all follows Isabelle/Pure and its higher-order natural
deduction environment. Similarities with Mizar and other "declaritive
proof" modes are quite superficial. I never use the "declarative"
terminolgy for Isar, it does not quite fit what it actually is.
In particular, their is no built-in automation in Isar. Users can draw on
an existing repertoire of proof methods taken from the library, such as
"metis" in Isabelle/HOL, but they don't have to.
Makarius
Email Gateway (Aug 18 2022 at 19:27):From: Josef Urban <josef.urban@gmail.com>
Hi Bill,
On Mon, Apr 30, 2012 at 5:55 AM, Bill Richter
<richter@math.northwestern.edu> wrote:
Josef, as you're a real Mizar expert, I'll be grateful if you look at
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
Superficially it looked OK. But there are better experts than me, and
you can get reviews and suggestions if you submit the article to MML.
I'll endure pain to manually transform my 1467 lines of Mizar Tarski
geometry proofs to Isabelle (or Coq or HOL Light even). I'm grateful
to the Mizar folks for writing a language I could learn and code up my
Tarski proofs, not least because I now believe my proofs. But I think
Mizar is too clunky a language to recommend high school students to
code in. That brings up HOL Light's Mizar mode, as you mentioned, or
Freek's miz3, but I couldn't get any of them to run on HOL Light 3.09,
nor could I compile the latest version of HOL Light, and Freek
suggests often that Isabelle is an improvement over Mizar.
I just saw the extensive discussion on the hol list, and I don't think
I can add much. Particularly John knows really a lot. One recent
comparison talk by Freek is at www.cs.ru.nl/~freek/talks/lsfa.pdf .
Could you just get me started on Isabelle?
Why me? :-) There are so many Isabelle experts here.
Best,
Josef
I finally ran the
executable ./Isabelle, and up popped jedit. I'm reading various
Isabelle dox, and it's all great, but I haven't found what I want:How do we code up first order logic (FOL) proofs that follow from some
FOL axioms? I really think the Isabelle dox ought to explain this.You can't exactly do that in Mizar, I believe, and maybe you can't do
it in any of the proof assistants. Mizar is all about set theory
(using I think Tarski's FOL set theory axioms), so we have to talk
instead about a model of my FOL axioms. That's fine.So we have to define some ``class'' of mathematical objects, which is
the sets, functions & relations that define a model. In my case,
that's a set S with a 3-ary and 4-ary relation equiv and between
satisfying various properties (Tarski's axioms). Now we have to code
up proofs about this class i.e. prove theorems about models of
Tarski's axioms, which amounts to the FOL proofs we want. This must
be explained somewhere in the Isabelle dox.--
Best,
Bill
Email Gateway (Aug 18 2022 at 19:38):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
I don't think they're saying that there's a problem with the axioms;
they're saying that there's a problem with some of Hilbert's proofs.
See, for example,
Meikle, L. I., and Fleuriot, J. D. Formalizing Hilbert’s Grundlagen in
Isabelle/Isar. In Theorem Proving in Higher Order Logics, D. Basin and
B. Wolff, Eds., vol. 2758 of Lecture Notes in Computer Science.
Springer Berlin / Heidelberg, 2003, pp. 319–334.
In particular, on page 327, they say "The Grundlagen proof then applied
Axiom(II,4). This was not possible in the mechanical proof until all
nine assumptions of the axiom were present. ...
Hilberts_missing_assumptions was a lemma used to achieve this. Its
proof was difficult, especially having to show that EG lay on the plane
AFC. Hilbert failed to mention these difficulties."
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:46):From: Bill Richter <richter@math.northwestern.edu>
Jeremy, I'll look at your paper, but don't want to discuss Euclid with
you or anyone else here unless they understand Hilbert's formal (not
informal) first order axiomatization of plane geometry as explained in
Hartshorne's book: 3 incidence axioms, 4 betweenness axioms, 6
congruence axioms, the parallel postulate and the circle-circle axiom.
With these axioms, you can prove every plane geometry result Euclid
stated, and you ought to be able to code the proofs up nicely in
Isabelle, and maybe even teach a high school or college course where
the students code up their own rigorous axiomatic Hilbert proofs. You
can't code up proofs of Euclid's propositions using Euclid's axioms.
Your paper is relevant to this group if you can code up your
enhanced-Euclid proofs in Isabelle. I couldn't tell from my brief
glance at your paper if this is possible. What do you think?
Email Gateway (Aug 18 2022 at 19:47):From: Bill Richter <richter@math.northwestern.edu>
Tim and Makarius, I can't follow the Isabelle dox, and I need
something like ``Isabelle for Dummies.'' I just want to know how to
write my FOL proofs in Isabelle, how to compile them, with examples.
Now I feel strongly that Isabelle (like Mizar) ought to be able to
check FOL proofs without specifying any proof strategies like Tim's
simp add' or blast'. Mizar makes lots of proof shortcuts that I
wouldn't have expected, and I'd be happier if Isabelle did few proof
shortcuts. I want the students to have to write up most of the proof.
I think in strict FOL, you have to insert so many needless steps that
the proofs become unreadable. I guess we need a good compromise.
I untarred Isabelle2011-1_bundle_x86-linux.tar.gz and went to the
directory Isabelle2011-1.
I ran the executable ./Isabelle and up popped jedit. I pasted in
Isabelle code from Tim's master's thesis into Scratch.thy. There's
extensive jedit help on the Help menu, but I couldn't figure out how
to compile my buffer. So then I tried
bin/isabelle emacs po.thy &
and up popped a Proof General Emacs frame displaying my short file
po.thy based on the first example in the
Isabelle2011-1/doc/locales.pdf.
------ po.thy ----
theory PO
imports Main
begin
locale partial_order =
fixes le :: " 'a ⇒ 'a ⇒ bool " (infixl "\<sqsubseteq>" 50)
assumes refl [intro, simp]: "x \<sqsubseteq> x"
and anti_sym [intro]: "[[ x \<sqsubseteq> y; y \<sqsubseteq> x ]] =⇒ x = y"
and trans [trans]: "[[ x \<sqsubseteq> y; y \<sqsubseteq> z ]] =⇒ x \<sqsubseteq> z"
------ end po.thy ----
Now I can see how to compile my file! I click on menu item
Isabelle -> Start Isabelle
I think that's the much the same thing as clicking the down-arrow
button which says ``process whole buffer''. I get an error message:
I have no idea what this means. Posibly I'm using the wrong quote.
I'm writing 'a, but locales.pdf actually shows ’a. So I changed to
this quote, and I got a new error message:
*** Inner lexical error at: ’a ⇒ ’a ⇒ bool (line 6 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")
*** Failed to parse type
*** At command "locale" (line 5 of "/home/richter/Isabelle/Isabelle2011-1/po.thy")
Maybe that's progress, because Proof General is now noticing my first
quote a, and not just the second one.
I'm actually trying to understand Tim's Tarski geometry axiom code.
So I tried compiling a simple version of it below. Proof General
gives me an error message similar to the above one:
*** Outer syntax error (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy"): command expected,
*** but symbolic identifier - (line 5 of "/home/richter/Isabelle/Isabelle2011-1/Scratch.thy") was found
But it's the code I'm more interested in now. Tim's axioms make
perfect sense, except for the (- - ≡ - - [99,99,99,99] 50) on the line
defining C. I'm concerned about lemma A1, which just restates the
axiom A1. I do something like that in my Mizar code, and I was really
hoping it wouldn't be necessary in Isabelle. Maybe I don't know what
lemma A1 is for. But there's plenty of stuff I don't understand in
Tim's proof, like
by (simp add: A1)
with A2 show ?thesis by blast
On p 123 of isar-ref.pdf, this is somewhat explained:
Typically, the soundness proof is relatively straight-forward,
often just by canonical automated tools such as “by simp ” or “by
blast ”.
I'm guessing that simp and blast are like what HOL Light calls
tactics, search strategies for Isabelle to concoct a proof. One of
the nice things about Mizar is that you don't ever have to specify any
proof strategies, although clearly Mizar is using a strategy.
Tim's ?thesis I bet can understand, from p 6:
?thesis — the main conclusion of the innermost pending claim
Tim's show ?thesis seems to be explained on p 126:
Typical idioms for concluding calculational proofs are “finally show ?thesis .”
---- simple version of Tim's Tarski code ----
theory Tarski
imports Main
begin
locale tarski-first7 =
fixes C :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool " (- - ≡ - - [99,99,99,99] 50)
fixes B :: 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool
assumes A1: \<forall> a b. a b \<equiv> b a
and A2: \<forall> a b p q r s. a b \<equiv> p q \<and> a b \<equiv> r s −\<rightarrow> p q \<equiv> r s
and A3: \<forall> a b c. a b \<equiv> c c −\<rightarrow> a = b
and A4: \<forall> q a b c. \<exists> x. B q a x \<and> a x \<equiv> b c
and A5: \<forall> a b c d a b c d . a = b \<and> B a b c \<and> B a b c
\<and>ab \<equiv> a b \<and>bc \<equiv> b c \<and>ad \<equiv> a d \<and> bd \<equiv> b d
−\<rightarrow> c d \<equiv> c d
and A6: \<forall> a b. B a b a −\<rightarrow> a = b
and A7: \<forall> a b c p q. B a p c \<and> B b q c −\<rightarrow> (\<exists> x. B p x b \<and> B q x a)
context tarski-first7
begin
lemma A1 : a b \<equiv> b a
by (simp add: A1)
lemma A2 : [[a b \<equiv> p q; a b \<equiv> r s]] =\<Rightarrow> p q \<equiv> r s
proof −
assume a b \<equiv> p q and a b \<equiv> r s
with A2 show ?thesis by blast
qed
lemma A3 : a b \<equiv> c c =\<Rightarrow> a = b
by (simp add: A3)
theorem th2-1: a b \<equiv> a b
proof −
from A2 [of b a a b a b] and A1 [of b a] show ?thesis by simp
qed
theorem th2-2: a b \<equiv> c d =\<Rightarrow> c d \<equiv> a b
proof −
assume a b \<equiv> c d
with A2 [of a b c d a b] and th2-1 [of a b] show ?thesis by simp
qed
theorem th2-3: [[a b \<equiv> c d; c d \<equiv> e f ]] =\<Rightarrow> a b \<equiv> e f
proof −
assume a b \<equiv> c d
with th2-2 [of a b c d] have c d \<equiv> a b by simp
assume c d \<equiv> e f
with A2 [of c d a b e f ] and c d \<equiv> a b show ?thesis by simp
qed
theorem th2-4: a b \<equiv> c d =\<Rightarrow> b a \<equiv> c d
proof −
assume a b \<equiv> c d
with th2-3 [of b a a b c d] and A1 [of b a] show ?thesis by simp
qed
theorem th2-5: a b \<equiv> c d =\<Rightarrow> a b \<equiv> d c
proof −
assume a b \<equiv> c d
with th2-3 [of a b c d d c] and A1 [of c d] show ?thesis by simp
qed
Email Gateway (Aug 18 2022 at 19:48):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Bill,
As soon as you open a theory file (extension ".thy") with jEdit, it is
constantly "checked" (even in parallel, for lemmas that are not
dependent in a linear fashion). (There is a thin column next to the main
text buffer, where the total progress or errors are indicated.
Furthermore, errors are marked by red wavy lines inside the text buffer.)
On a more general note. In principle I would strongly suggest to start
with trivial proofs in order to get acquainted with the mechanisms of
Isabelle. And only afterwards try to formalize something serious.
Concerning some of the points you mentioned:
PDFs or HTML sites that are generated from Isabelle theory files often
use slightly different symbols/notation than is actually used as input.
A good way to get "the real thing" is having a look (e.g., with jEdit)
at the example theory files that are located in <Isabelle
directory>/src/HOL/ex/.
In parallel to referring to reference manuals (like isar-ref) it is a
good idea to read more tutorial-like texts, e.g., tutorial.pdf and
isar-overview.pdf, that are part of the documentation of Isabelle.
It is mostly your own decision how big the steps of a proof are. You
can do single steps (using the "rule" method) which results in huge
undigestable proofs. Or you can use methods like "simp" (equational
reasoning), "blast" (logical reasoning which should succeed on many
first-order proofs), "auto" (somewhat a combination of the previous
two), "induction" (for ... well, induction), "cases" (for case
analysis). (In courses it is often done that students are only allowed
to use certain rules in order to proof a statement, since the automatic
tools would outright solve many typical examples.)
hope this helps,
chris
Email Gateway (Aug 18 2022 at 19:49):From: Bill Richter <richter@math.northwestern.edu>
I've posted a number of times without getting the help I wanted.
Included below is 1000 lines of HOL-Light/miz3 code that works great.
I couldn't have written it without the help of John Harrison, who got
me started in 3 separate ways, and also Freek Wiedijk. Someone can
probably tell me how to port this code to Isabelle. The Isabelle dox
for proofs look great, but to me they are impenetrable. I think I
coded in the axioms correctly, in the file light below (Tarski) but I
can't figure out how to write any Isabelle proofs.
theory Tarski
imports Main
begin
locale tarski-first7 =
fixes C :: "'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool" (- - \<equiv> - - [99,99,99,99] 50)
fixes B :: 'p \<Rightarrow> 'p \<Rightarrow> 'p \<Rightarrow> bool
assumes A1: "\<forall> a b. a b \<equiv> b a"
and A2: "\<forall> a b p q r s. a b \<equiv> p q \<and> a b \<equiv> r s =\<Rightarrow> p q \<equiv> r s"
and A3: "\<forall> a b c. a b \<equiv> c c =\<Rightarrow> a = b"
and A4: "\<forall> q a b c. \<exists> x. B q a x \<and> a x \<equiv> b c"
and A5: "\<forall> a b c d a' b' c' d' . not(a = b) \<and> B a b c \<and> B a' b' c'
\<and> a b \<equiv> a' b' \<and> b c \<equiv> b' c' \<and> a d \<equiv> a' d' \<and> b d \<equiv> b' d'
=\<Rightarrow> c d \<equiv> c' d'"
and A6: "\<forall> a b. B a b a =\<Rightarrow> a = b"
and A7: "\<forall> a b c p q. B a p c \<and> B b q c =\<Rightarrow> \<exists> x. B p x b \<and> B q x a"
end
Email Gateway (Aug 18 2022 at 19:49):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
I think what you might be looking for is Isabelle's locales. In my
thesis, I used a locale (actually, several incremental locales) to
characterize Tarski's axioms. Then, I could prove consequences of the
axioms inside the locales, and I could define models of the axioms
outside the locales that I later proved were instances of the locales.
Tim
<><
signature.asc
Email Gateway (Aug 18 2022 at 19:53):From: Bill Richter <richter@math.northwestern.edu>
Jeremy, if you or anyone else wants to talk about Euclid off-line, I'd
be happy to talk. As I try to explain in my paper, I love the Elements
http://www.math.northwestern.edu/~richter/hilbert.pdf
It's very creative and forms the basis of non-Euclidean geometry.
Thanks, Chris, that's very helpful. I'll look for the red wavy error
lines in jedit. I'll look at /src/HOL/ex/. I've looked at
tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good.
Thanks for explaining simp, blast etc, although I don't really know
what you mean. Is there somewhere an FOL example, with a long
(perhaps indigestible) single step "rule" method proof, which is
shortened with simp, and then shortened even more with blast & auto?
(In courses it is often done that students are only allowed to use
certain rules in order to proof a statement, since the automatic
tools would outright solve many typical examples.)
Wow! Can you point me to any of these courses? That sounds like what
I need to know. As I posted earlier, I'm mostly trying to cite some
good code for my geometry paper above (which I'll then submit). I
don't have to write the code myself, although I did
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
Examples of real classroom situations where students hand in Isabelle
proofs would be fantastic! Dunno about Europe, but US public schools
are really gungho about computer applications.
Email Gateway (Aug 18 2022 at 19:54):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Bill,
On 05/02/2012 01:09 PM, Bill Richter wrote:
Thanks, Chris, that's very helpful. I'll look for the red wavy error
lines in jedit. I'll look at /src/HOL/ex/. I've looked at
tutorial.pdf, but I'll look again, and isar-overview.pdf sounds good.
Thanks for explaining simp, blast etc, although I don't really know
what you mean. Is there somewhere an FOL example, with a long
(perhaps indigestible) single step "rule" method proof, which is
shortened with simp, and then shortened even more with blast& auto?
Well, not really indigestible, but consider the following Isabelle/HOL
proof of Pierce's Law:
lemma Pierce1: "((P --> Q) --> P) --> P"
proof (rule impI)
assume 1: "(P --> Q) --> P"
have "(~ P) | P" by (rule excluded_middle)
thus P
proof (rule disjE)
assume "P" thus "P" by assumption
next
assume 2: "~ P"
have "P --> Q"
proof (rule impI)
assume "P"
with 2 show "Q" by (rule notE)
qed
with 1 show "P" by (rule mp)
qed
qed
Which just uses the existing lemmas
impI: (?P ==> ?Q) ==> ?P --> ?Q
excluded_middle: ~ ?P | ?P
disjE: ?P | ?Q ==> (?P ==> ?R) ==> (?Q ==> ?R) ==> ?R
notE: ~ ?P ==> ?P ==> ?R
mp: ?P --> ?Q ==> ?P ==> ?Q
where the question marks indicate that variables can be instantiated
arbitrarily (i.e., they are so called "schematic variables"). In this
proof every step (w.r.t. some given set of rules) is done explicitly. If
we use "blast" (or "auto" for that matter) it reduces to.
lemma Pierce2: "((P --> Q) --> P) --> P" by blast
But note that both proofs are equally rigorous, since blast just applies
existing lemmas that are setup as introduction and elimination rules for
logical symbols (besides others). (The whole idea of proof assistants
like Isabelle, is that internally everything is reducible to the initial
axioms, whether this is done by hand or left to the system is to some
extend the users choice [sometimes the automatic methods are just not
powerful enough to solve a goal and the user has to divide it in smaller
pieces manually].)
(In courses it is often done that students are only allowed to use
certain rules in order to proof a statement, since the automatic
tools would outright solve many typical examples.)Wow! Can you point me to any of these courses? That sounds like what
I need to know. As I posted earlier, I'm mostly trying to cite some
good code for my geometry paper above (which I'll then submit). I
don't have to write the code myself, although I did
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
Examples of real classroom situations where students hand in Isabelle
proofs would be fantastic! Dunno about Europe, but US public schools
are really gungho about computer applications.
There is the Isabelle Community Wiki
https://isabelle.in.tum.de/community
(which has not yet really come to life). It contains pointers to some
courses that use or are about Isabelle
https://isabelle.in.tum.de/community/Course_Material
This could be interesting for you.
hope this helps
chris
Email Gateway (Aug 18 2022 at 19:56):From: Bill Richter <richter@math.northwestern.edu>
Makarius ported to Isabelle 100+ lines (below) of my HOL-Light/miz3
code I posted here on May 20, which is more or less a port of Julien
Narboux's Coq pseudo-code. I'm thrilled the Isabelle maintainers took
such an interest in Tarski axiomatic geometry:
M> I've spent maybe 1 or 2 hours on the various versions of the Tarski
M> axiomatization by Bill, Julien Narboux, John Harrison, and
M> Wikipedia. Bill had a slight divergence in some details in his 2
M> or 3 versions that I did not follow to the bottom.
Makarius's port proved a theorem that's false, the last theorem below,
C1. The problem seems to be Makarius's axiom
A5: "a ≠ b ⟹ Bet a b c ⟹ Bet a' b' c' ⟹ a b c ≐≐ a' b' c' ⟹
b d ≐ b' d' ⟹ c d ≐ c' d'"
I think this is my error, from my Isabelle file 6Tarski.thy, which I
think I posted here. My deepest apologies! I should have written
and A5: "∀ a b c d a' b' c' d' . not(a = b) ∧ B a b d ∧ B a' b' d'
∧ a b ≡ a' b' ∧ b c ≡ b' c' ∧ a d ≡ a' d' ∧ b d ≡ b' d'
=⇒ c d ≡ c' d'"
which is basically Tarksi's version of the SAS axiom (which Tarski
cleverly defined without having angles!), which I got right in miz3
let A5 = new_axiom
!a b c d a' b' c' d'.
~(a = b) /\ a,b,c cong a',b',c' /\
Between(a,b,d) /\ Between(a',b',d') /\ b,d === b',d'
==> c,d === c',d';;
Makarius, I think you needed
Bet a b d ⟹ Bet a' b' d',
but you sure did a whole better than I did! I couldn't even get the
axiom locale to work, or prove anything. I made the change, and now
jedit gives an error, with do-not-enters on the last 4 lines:
with neq Bet Bet have "y x ≐ y y" using b x ≐ b y by (rule A5)
then show ?thesis by (rule A3)
qed
end
So I uncommented the assumption
and "Bet a b x"
but I still get these 4 do-not-enters. Uh, would you try try again?
A few things confuse me about your code, e.g.
defines "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"
So ≡ means "if and only if", which in HOL-Light is <=>?
Two of Tarski's first 7 axioms are constructive (some point x exists),
A4 and A7, and you proved rules for them, using what I thought was a
very powerful automation tool blast:
lemma A4_rule: obtains x where "Bet q a x" and "a x ≐ b c"
using A4 by blast
and then used A4 by e.g. writing
obtain x where x: "Bet q a x" "a x ≐ a a" by (rule A4_rule)
Hmm, you don't have to do that in Mizar or Freek's miz3.
Now I ran your code in the spanking new Isabelle:
(poisson)Isabelle2012> ./Isabelle ../Tarski.thy &
I'm a newbie, but it sure looks to me that jedit thinks your code is
perfect. Let me explain why your last result shouldn't be true:
lemma C1:
assumes neq: "a ≠ b"
and Bet: "Bet a b y"
(* and "Bet a b x" -- "FIXME unused" *)
and "b x ≐ b y"
shows "y = x"
proof -
have 1: "a b ≐ a b" ..
have 2: "b y ≐ b y" ..
have "a b y ≐≐ a b y" ..
with neq Bet Bet have "y x ≐ y y" using b x ≐ b y by (rule A5)
then show ?thesis by (rule A3)
qed
Tarski's axioms hold in the plane R^2, in which the result means this.
Let l' be the line containing two distinct points a' and b'. Take
y' to be a point on `l' so that b is between a and y. (That means
that y can equal b.) Now take a point x in the plane so that
length bx = length by.
Then x = y.
Of course that's false (unless y = b). There's a whole circle of such
points x, with center b and radius length by.
Email Gateway (Aug 18 2022 at 19:56):From: Makarius <makarius@sketis.net>
On Fri, 25 May 2012, Bill Richter wrote:
Makarius's port proved a theorem that's false, the last theorem below,
C1. The problem seems to be Makarius's axiomA5: "a ≠ b ⟹ Bet a b c ⟹ Bet a' b' c' ⟹ a b c ≐≐ a' b' c' ⟹
b d ≐ b' d' ⟹ c d ≐ c' d'"I think this is my error, from my Isabelle file 6Tarski.thy, which I
think I posted here. My deepest apologies! I should have writtenand A5: "∀ a b c d a' b' c' d' . not(a = b) ∧ B a b d ∧ B a' b' d'
∧ a b ≡ a' b' ∧ b c ≡ b' c' ∧ a d ≡ a' d' ∧ b d ≡ b' d'
=⇒ c d ≡ c' d'"which is basically Tarksi's version of the SAS axiom (which Tarski
cleverly defined without having angles!), which I got right in miz3
Of course the theorem was true under the given assumptions. It happens
routinely in formalizations that something else is formalized than
expected. This is why unguarded axiomatizations are so dangerous. Here
we made a locale definition instead, and in the worst case the
corresponding predicate tarski_first7 could turn out to be always False,
not more no less.
I made the change, and now jedit gives an error, with do-not-enters on
the last 4 lines:with neq Bet Bet have "y x ≐ y y" using
b x ≐ b yby (rule A5)
then show ?thesis by (rule A3)
qedend
So I uncommented the assumption
and "Bet a b x"
but I still get these 4 do-not-enters. Uh, would you try try again?
Here is my proof with the amended locale definition:
lemma C1:
assumes neq: "a ≠ b"
and Bet1: "Bet a b y"
and Bet2: "Bet a b x"
and b: "b x ≐ b y"
shows "y = x"
proof -
have "y x ≐ y y"
using neq Bet2 Bet1 _ b
proof (rule A5)
show "a b y ≐≐ a b y" ..
qed
then show ?thesis by (rule A3)
qed
We are doing precise single step reasoning here, which means all the slots
for the rules need to be filled in the correct order. This is not Mizar
or any of the Mizar modes for HOL, which are centered around classic
predicate logic with some builtin proof automation to bridge larger gaps.
Note that the precise natural deduction of the Pure Isar proof has
exhibited the mistake in the A5 specification, in the first place.
A few things confuse me about your code, e.g.
defines "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"
So ≡ means "if and only if", which in HOL-Light is <=>?
No it is Pure equality. Unlike 'definition', the 'defines' element cannot
work with object-level =.
Two of Tarski's first 7 axioms are constructive (some point x exists),
A4 and A7, and you proved rules for them, using what I thought was a
very powerful automation tool blast:lemma A4_rule: obtains x where "Bet q a x" and "a x ≐ b c"
using A4 by blastand then used A4 by e.g. writing
obtain x where x: "Bet q a x" "a x ≐ a a" by (rule A4_rule)
Hmm, you don't have to do that in Mizar or Freek's miz3.
The locale definition only allows closed Pure rule statements, not the
open Isar form with fixes/assumes--shows/obtains, so I proved them as
lemmas later on in the context. By doing that, the heavy-duty classical
reasoning of blast was clearly isolated in some derived rules. In Mizar or
miz3, it would have intruded the proof, and the mistake in your A5 would
not have been discovered. (You did not have it in the miz3 version that
you sent me, but in the Isabelle attempt.)
Let me explain why your last result shouldn't be true:
lemma C1:
assumes neq: "a ≠ b"
and Bet: "Bet a b y"
(* and "Bet a b x" -- "FIXME unused" *)
and "b x ≐ b y"
shows "y = x"
proof -
have 1: "a b ≐ a b" ..
have 2: "b y ≐ b y" ..
have "a b y ≐≐ a b y" ..
with neq Bet Bet have "y x ≐ y y" usingb x ≐ b yby (rule A5)
then show ?thesis by (rule A3)
qedTarski's axioms hold in the plane R^2, in which the result means this.
Let
l' be the line containing two distinct pointsa' andb'. Takey' to be a point on `l' so that b is between a and y. (That means
that y can equal b.) Now take a point x in the plane so that
length bx = length by.
Then x = y.Of course that's false (unless y = b). There's a whole circle of such
points x, with center b and radius length by.
That is an informal argument. It merely motivates why something in the
formalization had to be amended.
Makarius
Email Gateway (Aug 18 2022 at 19:57):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Makarius, I'll run your code and study it. Is this explained
somewhere in the Isabelle dox, or could you explain it better:
We are doing precise single step reasoning here, which means all
the slots for the rules need to be filled in the correct order.
This is not Mizar or any of the Mizar modes for HOL, which are
centered around classic predicate logic with some builtin proof
automation to bridge larger gaps.
I would have said FOL instead of predicate logic, does that mean the
same? I'm not an expert in FOL, but I think FOL proofs tend to be
very tedious, and the builtin Mizar proof automation turns these FOL
proofs into something that is a real pleasure to code up. Is that
right? And Isabelle (Isar?) is doing something different from that?
Of course that's false (unless y = b). There's a whole circle of
such points x, with center b and radius length by.
That is an informal argument. It merely motivates why something in
the formalization had to be amended.
Absolutely!
In Mizar or miz3, it would have intruded the proof, and the mistake
in your A5 would not have been discovered.
I bet it would have been discovered! I wrote 1500 lines of Mizar
proofs (slimmed down to 1000 miz3 lines), that's bound to shake out
bugs in the axioms.
(You did not have it in the miz3 version that you sent me, but in
the Isabelle attempt.)
Let me apologize again for sending you the busted A5 Isabelle code.
This is why unguarded axiomatizations are so dangerous. Here we
made a locale definition instead, and in the worst case the
corresponding predicate tarski_first7 could turn out to be always
False, not more no less.
Yes, and thus locales are definitely a real advantage of Isabelle over
HOL Light right now. Still, I wonder why one can't just define all
the sets you'd want in HOL Light (only very lightly typed) to get
something like a locale. That is, I think of your locale as something
close to FOL Tarski axiomatic geometry proofs. But instead we could
look at all models of Tarski's axioms, a model being some sets and
functions with some properties. Can you do this in Isabelle too?
Email Gateway (Aug 18 2022 at 19:57):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Oops, of course I meant "Peirce" (but after three occurrences I can
hardly claim this as a typo ;)).
Email Gateway (Aug 18 2022 at 19:58):From: Makarius <makarius@sketis.net>
On Sun, 27 May 2012, Bill Richter wrote:
Thanks, Makarius, I'll run your code and study it. Is this explained
somewhere in the Isabelle dox, or could you explain it better:We are doing precise single step reasoning here, which means all
the slots for the rules need to be filled in the correct order.
This is not Mizar or any of the Mizar modes for HOL, which are
centered around classic predicate logic with some builtin proof
automation to bridge larger gaps.I would have said FOL instead of predicate logic, does that mean the
same? I'm not an expert in FOL, but I think FOL proofs tend to be
very tedious, and the builtin Mizar proof automation turns these FOL
proofs into something that is a real pleasure to code up. Is that
right? And Isabelle (Isar?) is doing something different from that?
The Isabelle/Pure framework is centered around higher-order natural
deduction, and Isabelle/Isar as a proof language continues these ideas. To
understand these things properly, you should first blot out "FOL", then
get used to Pure + Isar, then add HOL as object-logic, and then rediscover
what predicate logic (including FOL) will do for you here via some add-on
tools.
Yes, and thus locales are definitely a real advantage of Isabelle over
HOL Light right now. Still, I wonder why one can't just define all
the sets you'd want in HOL Light (only very lightly typed) to get
something like a locale.
In principle any of the HOL systems could provide their own locale
mechanism, or something similar. It is not possible to "just" do it,
though. Isabelle has required 10+ years to get this all done right. It is
also a matter of culture. John Harrison would certainly not add such
complexity to his system. You have to use Isabelle or Coq for such
sophisticated module concepts, or maybe Mizar.
That is, I think of your locale as something close to FOL Tarski
axiomatic geometry proofs. But instead we could look at all models of
Tarski's axioms, a model being some sets and functions with some
properties. Can you do this in Isabelle too?
If this means you want to study the meta-theory of Tarski axioms, then any
of the HOL systems -- Isabelle/HOL included -- can do this for you, if you
define the syntax and inference system more concretely (via datatypes and
inductive relations).
Makarius
Email Gateway (Aug 18 2022 at 20:00):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Makarius, and I really like your posts on hol info. I'd be
happy for you to post there about miz3 ocaml dirty code cache issues.
The Isabelle/Pure framework is centered around higher-order natural
deduction, and Isabelle/Isar as a proof language continues these
ideas. To understand these things properly, you should first blot
out "FOL", then get used to Pure + Isar, then add HOL as
object-logic, and then rediscover what predicate logic (including
FOL) will do for you here via some add-on tools.
I'm not opposed to learning Pure + Isar, but it would be a whole lot
easier for me to learn if I knew in advance how it related to FOL,
which as a mathematician I have a rudimentary (but not practical)
understanding of. Let me make a rudimentary FOL point:
I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom. I don't have a full list of the tedium
strict FOL can cause. But I'm only willing to write up FOL-type
proofs if the proof assistant will automate that tedium. Do similar
issues arise with Pure + Isar?
Also, as you may have observed on hol info, I know next to nothing
about HOL. Basically I understand the 20 pages of set theory John
explains in his reference manual. Isn't Isabelle HOL much the same as
HOL as in HOL Light HOL? Where is a good place to learn about HOL?
Yes, and thus locales are definitely a real advantage of Isabelle
over HOL Light right now. Still, I wonder why one can't just
define all the sets you'd want in HOL Light (only very lightly
typed) to get something like a locale.
In principle any of the HOL systems could provide their own locale
mechanism, or something similar. It is not possible to "just" do
it, though. Isabelle has required 10+ years to get this all done
right. It is also a matter of culture. John Harrison would
certainly not add such complexity to his system. You have to use
Isabelle or Coq for such sophisticated module concepts, or maybe
Mizar.
Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing. More below:
But instead we could look at all models of Tarski's axioms, a
model being some sets and functions with some properties. Can
you do this in Isabelle too?
If this means you want to study the meta-theory of Tarski axioms,
then any of the HOL systems -- Isabelle/HOL included -- can do this
for you, if you define the syntax and inference system more
concretely (via datatypes and inductive relations).
Great, but I don't know what meta-theory means. A model of Tarski's
geometry axioms is be a set S (of points), a 3-ary relation Between on
S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I
only use his first 7 axioms, and you coded them up in Isabelle). So
there might be a predicate TarskiModel(S, Between, Equiv), and
theorems in a Tarski model would begin
assume TarskiModel(S, Between, Equiv)...
I don't understand HOL well enough to actually pull this off, but John
explained how to get started. My point is that I don't think any
typing is involved here, beyond maybe something rudimentary like
new_type("point",0);;
new_type_abbrev("TarskiPlane",:point->bool);;
Email Gateway (Aug 18 2022 at 20:00):From: Makarius <makarius@sketis.net>
On Wed, 30 May 2012, Bill Richter wrote:
I'd be happy for you to post there about miz3 ocaml dirty code cache
issues.
Better not. I did not really follow that detail of this highly complex
thread. It is part of the miz3 philosophy to do things in a certain way,
and Freek has a right to take his preferred way.
The Isabelle/Pure framework is centered around higher-order natural
deduction, and Isabelle/Isar as a proof language continues these
ideas. To understand these things properly, you should first blot
out "FOL", then get used to Pure + Isar, then add HOL as
object-logic, and then rediscover what predicate logic (including
FOL) will do for you here via some add-on tools.I'm not opposed to learning Pure + Isar, but it would be a whole lot
easier for me to learn if I knew in advance how it related to FOL,
which as a mathematician I have a rudimentary (but not practical)
understanding of.
In my rough "education plan" above, the relation to FOL was the last step,
not the first one. It is easier to get started with a clear mind.
Let me make a rudimentary FOL point:
I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom. I don't have a full list of the tedium
strict FOL can cause. But I'm only willing to write up FOL-type
proofs if the proof assistant will automate that tedium. Do similar
issues arise with Pure + Isar?
I can only guess what you mean by "strict axiomatic FOL proof". There are
many ways to define what a logical inference system is, and how proofs are
done.
In Isabelle Pure it is done over lambda-calculus as syntax, and via
backchaining of natural deduction rules with implicit unification to solve
the instantiation problems arising here. BTW, Isar means "Intelligible
semi-automated reasoning", because the only proof automation built into
the proof language is unification, which is typically used together with
implicit selection of rules from the context (library etc.) as determined
from the structure of the text. That's the whole secret of it.
Any other proof automation is quoted explicitly in the Isar text, via
"proof methods": blast, simp, auto, metis, smt, ... ad infinitum. You go
to the store and order the kind of washing machine you prefer, or do
things purely by hand ...
Also, as you may have observed on hol info, I know next to nothing
about HOL. Basically I understand the 20 pages of set theory John
explains in his reference manual. Isn't Isabelle HOL much the same as
HOL as in HOL Light HOL? Where is a good place to learn about HOL?
You should not spend to much time with that. If you take HOL as a
simplified version of set-theory with explicit syntactic types it is OK as
a start. Foundationally, HOL is not so interesting than it was in 1940 or
1950.
In principle any of the HOL systems could provide their own locale
mechanism, or something similar. It is not possible to "just" do
it, though. Isabelle has required 10+ years to get this all done
right. It is also a matter of culture. John Harrison would
certainly not add such complexity to his system. You have to use
Isabelle or Coq for such sophisticated module concepts, or maybe
Mizar.Sure, but I really dislike the Mizar type system, and I want to
lightly typed sets to avoid any hard typing.
Note that HOL typing is particularly hard. Every type is its own isolated
universe, although a rather small one. You need explicit morphisms to
travel between such distinct worlds.
But instead we could look at all models of Tarski's axioms, a
model being some sets and functions with some properties. Can
you do this in Isabelle too?If this means you want to study the meta-theory of Tarski axioms,
then any of the HOL systems -- Isabelle/HOL included -- can do this
for you, if you define the syntax and inference system more
concretely (via datatypes and inductive relations).Great, but I don't know what meta-theory means. A model of Tarski's
geometry axioms is be a set S (of points), a 3-ary relation Between on
S and a 4-ary relation Equiv on S satisfying Tarski's axioms (so far I
only use his first 7 axioms, and you coded them up in Isabelle). So
there might be a predicate TarskiModel(S, Between, Equiv), and
theorems in a Tarski model would begin
You get such a predicate already from the locale tarski_first7 that I've
produced for you. It is called "tarski_first7" and can be used within the
logical language:
term "tarski_first7"
The system will check that and print the most general type for it:
"('a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ bool". You
can also hover over the formal term to get it explained.
Note that the type is naturally curried as everything by default in
Isabelle Pure -- just like in good HOL families.
Moreover your carrier set S is actually modeled as a type here, in the
usual manner in HOL. You can relativize it to a set over the base type,
but that is a different story of the larger HOL family.
assume TarskiModel(S, Between, Equiv)...
This is what the locale context "begin" does for you implicitly, and then
you start to define derived things and state theorems and do proofs from
it. This means you are developing a concrete "theory", but this is not
meta-theory.
Meta theory means you speak about things, by stepping aside or outside
from it. Here is an arbitrary example from AFP, which I have happened to
have browsed two weeks ago with a student:
http://afp.sourceforge.net/entries/Completeness.shtml
The example develops the logical inference system and semantics of a
version of first-order logic in the usual way, almost literally from the
book (I don't know which one). There are just the usual formalization
tweaks to represent it as concrete formal things inside HOL (and a slight
tendency of redundant copies of basic mathematical HOL concepts used in
the development).
I don't understand HOL well enough to actually pull this off, but John
explained how to get started. My point is that I don't think any
typing is involved here, beyond maybe something rudimentary likenew_type("point",0);;
new_type_abbrev("TarskiPlane",:point->bool);;
That is a global axiomatic theory. In Isabelle/HOL is would look like
this:
axiomatization
Cong :: "point ⇒ point ⇒ point ⇒ point ⇒ bool" ("_ _ ≐ _ _" [1000,
1000, 1000, 1000] 50) and
Cong3 ("_ _ _ ≐≐ _ _ _" [1000, 1000, 1000, 1000, 1000, 1000] 50) and
Bet :: "point ⇒ point ⇒ point ⇒ bool"
where
Cong3_def: "a b c ≐≐ x y z ≡ a b ≐ x y ∧ a c ≐ x z ∧ b c ≐ y z"
and A1: "a b ≐ b a"
and A2: "a b ≐ p q ⟹ a b ≐ r s ⟹ p q ≐ r s"
and A3: "a b ≐ c c ⟹ a = b"
and A4: "∃x. Bet q a x ∧ a x ≐ b c"
and A5: "a ≠ b ⟹ Bet a b d ⟹ Bet a' b' d' ⟹ a b c ≐≐ a' b' c' ⟹
b d ≐ b' d' ⟹ c d ≐ c' d'"
and A6: "Bet a b a ⟹ a = b"
and A7: "Bet a p c ⟹ Bet b q c ⟹ ∃x. Bet p x b ∧ Bet q x a"
Showing that publicly on isabelle-users, most people should frown upun it
-- shudder. There are all these sophisticated ways to make things local
in Isabelle ...
Makarius
Email Gateway (Aug 18 2022 at 20:00):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Tim! I'll look carefully at your code, and study locales.
I should read Scott and Fleuriot's HOL Light article carefully, and
also Meikle and Fleuriot's Isabelle paper you cited
http://www.springerlink.com/content/6ngakhj9k7qj71th/fulltext.pdf.
I'm annoyed Hilbert wrote such an unreadable book FoG, and I wonder he
didn't take too much credit from Pasch. So I can learn from Scott,
Fleuriot & Meikle. But they need to learn how Euclid's errors were
corrected using Hilbert's axioms. I explain this nicely in
http://www.math.northwestern.edu/~richter/hilbert.pdf
Almost no working mathematicians understand the Euclid and
Hilbert's-axiom story, and I only learned it this year, to help my son
with Geometry, as his textbook was incredibly unrigorous. He read my
paper and my Mizar code quite carefully, and that's why I'm here.
What Meikle and Fleuriot write here is misleading:
It is generally accepted that Hilbert’s work managed to eradicate
the need for INTUITION in deriving results.
That's OK if we replace INTUITION by `drawing pictures instead of
using axioms'. What is generally accepted is that Hilbert’s work
managed to eradicate Euclid's pervasive angle-addition errors.
Back to Scott and Fleuriot, you may be correct that they found an
error involving solid geometry vs plane geometry. I'll look into it.
But Scott and Fleuriot's full quote is very misleading:
in their attempt to formalise the axiomatics and its elementary
theorems, Meikle and Fleuriot found many missing lemmas
[11]. Indeed, IT IS SUFFICIENT to note that Hilbert followed Euclid
in one pervasive omission: they both give proofs on an ambient
plane when the axioms characterise solid geometry [8].
It is not sufficient. We must note that textbooks by Greenberg &
Hartshorne gave acceptably rigorous treatments using Hilbert's axioms,
and nobody has ever given rigorous proofs using Euclid's axioms.
Tim, you really ought to understand the Euclid and Hilbert-axiom
story, being a Tarski geometry guy. Can you find
M. Greenberg, Euclidean and non-Euclidean geometries, W. H. Freeman
and Co., 1974.
R. Hartshorne, Geometry, Euclid and Beyond, Undergraduate Texts in
Math., Springer, 2000.
Greenberg's recent survey is quite readable and has interesting
mathematical logic relating Tarski's axioms to Hilbert's.
Old and new results in the foundations of elementary plane Euclidean
and non-Euclidean geometries, Amer. Math. Monthly 117 (2010),
198--219.
Email Gateway (Aug 18 2022 at 20:02):From: Bill Richter <richter@math.northwestern.edu>
Our paper aims to provide a formal system, E, that mirrors the
structure of Euclid's proof. We show how such a system can be
interpreted in terms of more conventional proof systems (like
Hilbert's),
Jeremy, this is very interesting, and explained on p 69 of your paper:
ADM> Below, however, we will show that with a modicum of tinkering,
ADM> Tarski’s axioms can be expressed in a restricted form, namely, as
ADM> a system of geometric rules. We will then invoke a cut
ADM> elimination theorem, due to Sara Negri, that shows that if a
ADM> sequent of suitably restricted complexity is provable in the
ADM> system, there is a proof in which every intermediate sequent is
ADM> also of restricted complexity. This will allow us to translate
ADM> proofs in Tarski’s system to proofs in E.
I don't see where you went the other way, translating your proofs into
Tarski axiomatic proofs. You are saying that rigorous Hilbert/Tarski
axiomatic proofs are simpler than proofs in your framework, right?
Probably you understand the advantage of Tarski's axioms over
Hilbert's, but I'll say it anyway: Mostly the advantage is that Tarski
in a first order axiom basically said that every line is the real
line, so that the model is R x R. Hilbert got that earlier with a
second order logic axiom, a Dedekind cuts axiom. Tarski actually only
got F x F, for a real closed field F, but that's good enough, as he
showed that the theory of real closed fields is decidable. But do you
need decidability? I see you mention it often. Ziegler's result that
you cite is used by Greenberg (Amer. Math. Monthly 2010) to show that
Hilbert's first order geometry is undecidable.
but getting Isabelle to verify proofs in E as such would require
extending Isabelle with some automation to bridge the gap.
But the Isabelle folks are looking for that kinda work (so I copied
the list)! I think that's why Scott, Fleuriot & Meikle are coding up
Hilbert's book FoG, to give HOL Light and Isabelle a workout.
Email Gateway (Aug 18 2022 at 20:02):From: Bill Richter <richter@math.northwestern.edu>
Thanks for the example, Chris! I'll have to study it. Your links
https://isabelle.in.tum.de/community/Course_Material seemed more about
learning Isabelle (and so relevant to me) than teaching undergraduate
math courses. But I know Julien Narboux and others are thinking that
way. I took your advice to read the tutorial, and have a bug report:
I learned interesting Isabelle from Proof General, but not jedit. I
learned the main thing that I wanted to know: we you can use fancy
symbols Mizar disallows, like ⇒, in isabelle proofs. I pasted in the
tutorial.pdf file Toylist.thy below of sec 2.3, with the last `done'
commented out. I opened it in jedit:
(localhost)Isabelle2011-1> bin/isabelle jedit Toylist.thy &
and get only the error message
Bad filename "Toylist.thy" for theory ToyList.
So I can't do any of the sec 2.3 tests in jedit! I think I got some
red wiggly lines of yours, and definitely a red-and-white do not enter
sign on the left of the first line theory ToyList. So instead I
opened it in Proof Generaland everything works.
(localhost)Isabelle2011-1> bin/isabelle emacs Toylist.thy &
I get the message
proof (prove): step 2
goal:
No subgoals!
By commenting things out and looking at the Proof General output, I
can understand the proof, which I'll explain. It's about Scheme-type
lists, built with cons (although no car & cdr), and the two simple
list functions append (@) and reverse. They inductively prove
xs @ [] = xs
(xs @ ys) @ zs = xs @ (ys @ zs)
rev(xs @ ys) = (rev ys) @ (rev xs)
rev(rev xs) = xs
with each proof using the previous results. We prove each statements
is true for xs = [], and then we prove that the statement for xs
implies the statement for x # xs. Let's just do the last one:
The base case is easy:
rev(rev []) = rev([]) = []
Now note that
rev([x]) = rev(x # []) = rev([]) @ (x # []) = [] @ (x # []) = x # []
Now assume theorem rev_rev is true xs. Then using lemma rev_app, the
induction assumption and the above, we prove the induction equation:
rev(rev (x # xs)) = rev(rev(xs) @ [x]) = rev([x]) @ rev(rev(xs))
= (x # []) @ xs = x # ([] @ xs) = x # xs
That's a nice proof. I don't know why we have to use strategy auto as
well as induct_tac, because it sure looks like just induction to me.
But if we comment out just the apply(auto) in the proof of theorem
rev_rev, we get the output
proof (prove): step 1
goal (2 subgoals):
Well, isabelle did nothing put state the inductive case. It didn't
even prove the base case. Page 12 of tutorial.pdf says
apply(induct_tac xs)
This tells Isabelle to perform induction on variable xs.
Apparently that's not true: to perform induction we need also auto.
If we instead comment out app_assoc and rev_app, we get message
goal (1 subgoal):
------------------------------ Toylist.thy ------------------------------
theory ToyList
imports Datatype
begin
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
(* This is the append function: *)
primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
where
"[] @ ys = ys" |
"(x # xs) @ ys = x # (xs @ ys)"
primrec rev :: "'a list \<Rightarrow> 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) @ (x # [])"
lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)
done
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply(auto)
done
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply(auto)
done
theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induct_tac xs)
apply(auto)
(* done *)
Email Gateway (Aug 18 2022 at 20:02):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Bill,
On 05/03/2012 12:38 PM, Bill Richter wrote:
I learned interesting Isabelle from Proof General, but not jedit. I
learned the main thing that I wanted to know: we you can use fancy
symbols Mizar disallows, like ⇒, in isabelle proofs. I pasted in the
tutorial.pdf file Toylist.thy below of sec 2.3, with the last `done'
commented out. I opened it in jedit:
(localhost)Isabelle2011-1> bin/isabelle jedit Toylist.thy&
and get only the error messageBad filename "Toylist.thy" for theory ToyList.
Well this error message is actually very informative. The file name and
the name of the theory differ (in case) and that is against conventions,
it's rather a bug of ProofGeneral to accept your file.
Now assume theorem rev_rev is true xs. Then using lemma rev_app, the
induction assumption and the above, we prove the induction equation:rev(rev (x # xs)) = rev(rev(xs) @ [x]) = rev([x]) @ rev(rev(xs))
= (x # []) @ xs = x # ([] @ xs) = x # xsThat's a nice proof. I don't know why we have to use strategy auto as
well as induct_tac, because it sure looks like just induction to me.
The induct/induction/induct_tac methods just set up an induction proof
(i.e., base cases + inductive cases) according to the variable you want
to induct over. It's the same with pen'n'paper actually. What you do to
solve the base case and inductive case is not induction, but mostly
different techniques like equational reasoning etc.But if we comment out just the apply(auto) in the proof of theorem
rev_rev, we get the outputproof (prove): step 1
goal (2 subgoals):
1. rev (rev []) = []
2. \<And>a list. rev (rev list) = list \<Longrightarrow> rev (rev (a # list)) = a # listWell, isabelle did nothing put state the inductive case. It didn't
even prove the base case. Page 12 of tutorial.pdf saysapply(induct_tac xs)
This tells Isabelle to perform induction on variable xs.Apparently that's not true: to perform induction we need also auto.
If we instead comment out app_assoc and rev_app, we get message
goal (1 subgoal):
1. \<And>a list. rev (rev list) = list \<Longrightarrow> rev (rev list @ a # []) = a # list *)
cheers
chris
Email Gateway (Aug 18 2022 at 20:02):From: Bill Richter <richter@math.northwestern.edu>
Bad filename "Toylist.thy" for theory ToyList.
Well this error message is actually very informative. The file name and
the name of the theory differ (in case) and that is against conventions,
it's rather a bug of ProofGeneral to accept your file.
You're a good teacher, Chris! You made me think: I was supposed to
write theory toylist', and not theory ToyList' in my Isabelle file.
The induct/induction/induct_tac methods just set up an induction
proof (i.e., base cases + inductive cases) according to the
variable you want to induct over. It's the same with pen'n'paper
actually. What you do to solve the base case and inductive case is
not induction, but mostly different techniques like equational
reasoning etc.
I need to understand what you mean in order to understand how to write
Isabelle or HOL Light proofs, but what I did is certainly what
mathematicians call an inductive proof. I showed the results were
true for lists of length 0 (just []), and then assumed the results
were true for all lists of length n, and used that to prove the
results were true for all lists length n+1. I've heard Schemers call
that tree induction.
Email Gateway (Aug 18 2022 at 20:02):From: Bill Richter <richter@math.northwestern.edu>
Sorry, Chris, I messed it up again. Noch einmals: my filename is
Toylist.thy, so I should have typed theory Toylist. I'm looking
forward to doing more exercises in jedit. Proof General is a pain.
Email Gateway (Aug 18 2022 at 20:02):From: Lars Noschinski <noschinl@in.tum.de>
There are two steps in an inductive proof: In a first step the original
goal ("property holds for all lists") is transformed with an induction
rule in a number of new goals ("property holds for lists of length 0"
and "assuming property holds for all lists of length n, it holds for all
lists of length n + 1"). In a second step these new goals have to be proven.
Isabelle's "induct" and "induct_tac" methods only perform the first
step. This transformation is done purely schematic -- even if e.g. the
base case is trivial, it will not be solved automatically. The second
step needs to be performed explicitly (here "auto").
-- Lars
Email Gateway (Aug 18 2022 at 20:02):From: Jeremy Avigad <avigad@cmu.edu>
Dear Bill,
I agree that it would be nice to see Elements-style proofs verified in
Isabelle. I have talked about E with friends in the Isabelle community,
so they know about the work.
I'll respond to the rest of the message off-list, though, since the
details are not related to Isabelle.
Best wishes,
Jeremy
Email Gateway (Aug 18 2022 at 20:06):From: Jeremy Avigad <avigad@cmu.edu>
Dear all,
At the risk of taking the discussion too far from Isabelle, I'd like to
mention that Ed Dean, John Mumma, and I have carried out a detailed
analysis of the style of reasoning one finds in Euclid:
A formal system for Euclid's Elements
Review of Symbolic Logic, 2:700-768, 2009
http://journals.cambridge.org/repo_A674ohNM
(additional links and errata are on my web page)
We argue that Euclid is more rigorous than is commonly acknowledged, in
that there are clearly discernible norms to diagrammatic reasoning
(though they are different from the norms of axiom-based proof). We also
note that Euclidean theorems have a very restricted logical form, and
show that his methods are complete (for that class of sentences) with
respect to the modern semantics of ruler-and-compass constructions.
Best wishes,
Jeremy
Email Gateway (Aug 18 2022 at 20:08):From: Bill Richter <richter@math.northwestern.edu>
Thank you very much Makarius, for a long interesting lecture. I
didn't know any of that stuff. This in particular:
If you take HOL as a simplified version of set-theory with explicit
syntactic types it is OK as a start.
But I think we'd communicate a lot better if you understood math
logic, from say Enderton's book Mathematical Logic. Until then you
won't know why I'm floundering. I apologize if I misunderstand you.
I can only guess what you mean by "strict axiomatic FOL proof".
I mean what Enderton means (same for `models'), and I'd like you to
know too. Look, you're really good at what you do, and you
communicate really well, and you go to the trouble to speak
intelligibly to newbies like me... but don't you want to know the
proof of the Goedel incompleteness theorem?
Anyway, eventually I'll take all of your suggestions. I'll go through
the Isar manuals and learn Pure + Isar and see how close that is to
Enderton's FOL. I want to learn! Isabelle is the only proof
assistant with nice fonts and serious documentation.
Email Gateway (Aug 18 2022 at 20:08):From: Tjark Weber <webertj@in.tum.de>
Dear Bill,
I haven't been following this thread in detail, so I am not sure what
you've been told already. Surely you realize that FOL is just one logic
(albeit an important one). There are many other logics, and interactive
proof assistants are usually not built on FOL.
There are very good reasons for this design choice, but it also has its
drawbacks. For instance, it tends to puzzle mathematicians with an
interest in foundations who have been taught that everything rests on
FOL and ZFC.
If you are specifically looking for systems that perform (automated)
first-order reasoning, take a look at
http://en.wikipedia.org/wiki/Automated_theorem_proving
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 20:12):From: Bill Richter <richter@math.northwestern.edu>
Thanks, Tjark and Konrad! I'll read the HOL paper, which looks pretty
old, and so is maybe something that everyone just assumes nowadays. I
don't know about those other first-order reasoning
Automated_theorem_provers, or why folks don't use them. My interest
in proof assistants (HOL Light, Isabelle, Coq) is that Tom Hales is
using them to formalize his Kepler conjecture proof.
it tends to puzzle mathematicians with an interest in foundations
who have been taught that everything rests on FOL and ZFC.
Tjark, you understand my confusion! Is something written about this?
I do contend that it's true what mathematicians are taught, but it may
not appear to be true at the technical level that proof assistants
operate on. That's of course fine, but I need to see the underlying
FOL and ZFC, even if the proof assistants aren't coded that way.
Email Gateway (Aug 18 2022 at 20:16):From: Ramana Kumar <rk436@cam.ac.uk>
On Mon, Jun 4, 2012 at 5:44 AM, Bill Richter
<richter@math.northwestern.edu>wrote:
Thanks, Tjark and Konrad! I'll read the HOL paper, which looks pretty
old, and so is maybe something that everyone just assumes nowadays. I
don't know about those other first-order reasoning
Automated_theorem_provers, or why folks don't use them.
Possible reasons include:
1. FOL isn't expressive enough for their problems. It might technically
be able to express something, but not nicely.
2. The automated provers can't solve their problems, at least not
without a lot of help, and that help is tedious to give.
3. Some automated provers don't generate complete explicit proofs, and
so have to be trusted; this is harder than trusting a simple proof checker.
That having been said, I'm under the impression that the world of automated
proving is always getting better. I don't know much about it because I
don't live day-to-day in that world.
Ideally, interactive provers should only benefit from progress in
automation, since automatic tools can be integrated into interactive proof
development environments.
My interest
in proof assistants (HOL Light, Isabelle, Coq) is that Tom Hales is
using them to formalize his Kepler conjecture proof.it tends to puzzle mathematicians with an interest in foundations
who have been taught that everything rests on FOL and ZFC.Tjark, you understand my confusion! Is something written about this?
I do contend that it's true what mathematicians are taught, but it may
not appear to be true at the technical level that proof assistants
operate on. That's of course fine, but I need to see the underlying
FOL and ZFC, even if the proof assistants aren't coded that way.
It's not just a matter of how the proof assistant is coded. The underlying
logic of Isabelle/HOL is not FOL. (There is, of course, Isabelle/ZF, which
does use FOL and the ZF axioms.)
The piece of writing I think you might find enlightening is Andy Pitts's
document on the semantics of HOL.
It is the "Logic" manual available here
http://hol.sourceforge.net/documentation.html.
Note it is for the HOL4 system, not Isabelle/HOL, but since it's mainly
about the logic, HOL, itself, that those proof assistants basically share,
this shouldn't matter too much.
It gives a precise description of the syntax and semantics of HOL. The
semantics is given in terms of set-theoretic models, with which you're
probably more familiar.
I'll be happy to answer any questions about it. I was thinking of giving
you syntax and semantics of FOL and then of HOL so you could see them
compared, but that document is better presented than what I would have
written.
(By the way, FOL formulas can be embedded in HOL.)
--
Best,
Bill
Email Gateway (Aug 18 2022 at 20:18):From: Slawomir Kolodynski <skokodyn@yahoo.com>
There is, of course, Isabelle/ZF, which does use FOL and the ZF axioms
Is there a deep reason to code geometry axioms inside HOL? It seems to me it would be more natural to build Tarski geometry logic based on FOL, in the similar way like ZF logic is built on FOL.
slawekk
http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Email Gateway (Aug 18 2022 at 20:20):From: Ramana Kumar <rk436@cam.ac.uk>
On Sun, Jun 3, 2012 at 12:53 AM, Bill Richter <richter@math.northwestern.edu
wrote:
I'm trying to use my math skills to get into the proof assistant game.
I know all of you are much better than I am at CS, and I would think
that you would all be better than I at mathematical logic as well.
And maybe you are, but I think I understand something that nobody ever
writes, so I wonder if folks do understand this.
I think you'll find that people who use computerised proof technology often
do already have a good understanding of mathematical logic (and
"metamathematics"), including Gödel's theorems.
Mathematical logic studies what you can and can't prove axiomatically
in first order logic (FOL).
I would contend that the field goes further and looks at other logics as
well, including extensions like second-order and higher-order logic, as
well as "restrictions" on first-order logic like non-classical logics
(linear, intuistionistic, modal, ...). Wikipedia has more info:
http://en.wikipedia.org/wiki/Mathematical_logic.
The Goedel Completeness Theorem
http://mathworld.wolfram.com/GoedelsCompletenessTheorem.html says
truth in every model implies an axiomatic proof, and the Goedel
Incompleteness Theorem says you can't write a computer program that
will print out all theorems of a model of the natural numbers:
http://mathworld.wolfram.com/GoedelsFirstIncompletenessTheorem.html
The phrase "all theorems of a model of the natural numbers" would perhaps
better read "all and only true statements about the natural numbers".
To me, theorems are statements with proofs, and models of a statement or a
theory are structures that make that statement or theory true.
The Completeness Theorem says that if a statement is true in every
structure (i.e. every structure models the statement), then the statement
has a proof.
(Implicitly, we first fix a first-order theory, i.e. a set of axioms and a
signature, then only consider statements in the language of that signature,
structures over that signature, and proofs over those axioms. The
Completeness Theorem holds no matter what theory we choose.)
If the set of axioms can be generated by a computer, then all (and only)
the provable statements of a theory can also be generated by a computer.
This is why first-order logic is "semidecidable".
The First Incompleteness Theorem says that if we fix a theory whose axioms
can be generated by a computer, whose signature allows the natural numbers
as a structure, and which proves various statements about the natural
numbers (e.g. Peano's axioms) but doesn't prove every statement (i.e. it is
consistent), then there exists some statement which is true in the natural
numbers but not provable.
Notes: Since the theory proves Peano's axioms but is consistent, the
natural numbers must be a model of this theory. But by the Completeness
Theorem, the unprovable statement cannot be true in all models of this
theory. Therefore the theory must have another "non-standard" model where
the unprovable statement is false.
What you said about a computer program not being able to print all theorems
is not a limitation of computer programs (because a program can always
print out all theorems of a first order theory). It's a limitation of
first-order theories to capture the natural numbers: they always end up
also being true of non-standard models that differ from the natural numbers
but the theory can't tell.
There's a simpler related result I don't know the name of, which says
that given any nice set of FOL axioms, you can write a computer
program to print out all the theorems that follow from them,
i.e. theorems which have axiomatic FOL proofs using these axioms.
Right. I'm not sure this result has any particular name. The "nice set" of
FOL axioms means a "recursively enumerable set".
Mathematicians basically restrict themselves to the FOL ZFC set theory
axioms, and so we can write a computer program that will print out (if
it runs indefinitely) every theorem that mathematicians well ever
prove (unless they adopt new axioms). Turing's proof of the Halting
problem (you can't write a infinite-loop checker) is just a
restatement of the Goedel incompleteness theorem.
The Lambda Calculus comes out of math logic, as it gives a definition of a
recursive
function that's equivalent to Turing-machine definable.The whole point of proof assistants is to make this math logic work!
Nobody's gonna run the simple program that prints out all the theorems
that follow from the FOL ZFC axioms and wait for a good theorem to pop
up. But you folks have written lots of smart proof assistants which
do great work on today's incredibly fast machines.
A bit of clarification: proof assistants usually consist of a proof
checking part and a proof development part. The proof checking part simply
checks that proofs are valid proofs, i.e. they come from the axioms via
inference rules. The proof development part may include tools for
structuring theories and tools for generating proofs automatically or
semi-automatically.
So what do proof assistants (Coq, Isabelle, HOL Light) do? I would
assume they all start with some FOL axioms and then deduce axiomatic
FOL proofs as one discusses in math logic. I contend that the proof
assistants must do that, because (by math logic) they can't do
anything else! And the mathematicians can't do anything else either!
No it's not true, because neither proof assistants nor mathematicians are
restricted to FOL.
Also, none of the proof systems really do any proving (unless you count the
automated components); rather, they enable you to construct a formal proof,
while checking all the time that what you're doing is valid.
In HOL Light and Isabelle/HOL (Isabelle itself is a logical framework that
can be instantiated at many different logics) let you conclude statements
that are either HOL axioms or derived from other theorems via HOL rules of
inference. The Wikipedia page has a list of the inference rules for HOL
Light http://en.wikipedia.org/wiki/HOL_Light. These systems don't actually
construct proofs (by default); rather, they construct "theorem" objects,
and limit the methods for constructing theorems to exactly the rules of
inference, thereby ensuring that whenever you have a theorem object, you
know a proof of it must exist (it was created ephemerally and dynamically
in the object's creation). This is the so-called "LCF approach".
Coq, on the other hand, does construct proofs by default, but in another
logic again: dependent type theory. In this logic, the proofs and the
statements live in the same language.
I'm sure others will be able to fill in more details here if you're
interested...
But I'm puzzled because almost nobody talks this way in the proof
assistant world. Mizar (and Freek's miz3 port to HOL Light) seems
reasonably close to FOL axiomatic proofs. Although I don't know
exactly how close. I have this vague idea that Mizar does axiomatic
FOL proofs with a lot of the tedium automated away, e.g. manually
substituting variables. But I don't know. The things that folks
actually do---HOL, Isar, Pure---I don't understand. I would need to
have them explained in terms of Goedel's field of math logic,
i.e. axiomatic FOL proofs. So I propose that if someone knows the answer,
they tell me, and if nobody knows the
answer, let's run a thread on math logic which will eventually explain
how HOL, Isar, Pure etc relate to Goedel's FOL. I have very little to
contribute to such a thread beyond the note on the LC Y combinator and
Goedel incompleteness below.
Well, perhaps we can continue after you've read about the syntax and
semantics of HOL and let's see if you have more specific questions then.
--
Best,
BillWe can understand Odifreddi's [p 80--1] startling remark that the Y
combinator "embodies the argument used in Russell's paradox" from
Boolos & Jeffries [Ch 14-15].That is, I'll show how the Lambda Calculus Y combinator comes from
Goedel Incompleteness, and how Goedel I sort of comes from Russell's
paradox. In particular, B&J's treatment of the Goedel fixed point
theorem is much clearer than Barendregt's [Thm (Goedel), sec 6.7].** Goedel's fixed point thm => Y combinator **
For any expression B(y) of number theory, B&J [Lem 2, p 173] show
there exists an expression F(x) such that for any expression M(x),Q |- F( #M ) <--> B( #M(#M) )
where Q is the minimal axiom set for number theory [B&J Ch 14], s.t. a
partial function N ---> N is representable in Q iff it's
recursive. I'm denoting Goedel numbers by #.Then letting G = F(#F) and plugging in, we have Goedel's result
Q |- G <--> B( #G )
Well, that gives us the Y combinator, just take out the #s and the
Qs. We want(F M) = (B (M M))
for all M, so we let
F = \m. B (m m)
G = F F
then
G = B Ggiving us the fixed point for B, which we encode as the Y combinator
Y = \b. (\f. f f) (\m. b (m m))
That's the only reasonable motivation I've ever seen for the Y
combinator. And maybe that explains that LC_v requires LC: as you
say, LC_v is for programming, LC is for Math logic. But we need Y in
order to be able to derive the harder Y_v.** Goedel fixed point thm => Goedel I **
Let E be the expression of number theory, E_0 the closed expressions,
or statements. Let Th(N) be the statements that are true in the
standard model of N. We'll write, for statements f in E_0,|= f
if f in Th(N).
Goedel proved that Th(N) is not decidable, meaning there is no
expression B(x) in E such that for any statement f in E_0,|= f if Q |- B(#f)
|= -f if Q |- -B(#f)But this statement implies the more tractable sounding
|= f
[message truncated]
Email Gateway (Aug 18 2022 at 20:20):From: Bill Richter <richter@math.northwestern.edu>
Is there a deep reason to code geometry axioms inside HOL? It seems
to me it would be more natural to build Tarski geometry logic based
on FOL, in the similar way like ZF logic is built on FOL.
That make sense, Slawomir, especially for Tarksi's axioms. On hol
info John Harrison has been helping me to code up my Hilbert axiom
paper using set theory you can do in HOL Light.
Thanks, Ramana, for demonstrating that you understand math logic at
least as well as I do. So I suppose we can assume that folks here in
general understand math logic. I feel that you mainly answered my
question (about the mathematicians's belief of FOL/ZFC primacy) by
recommending Konrad's The HOL System LOGIC manual.
Well, perhaps we can continue after you've read about the syntax and
semantics of HOL and let's see if you have more specific questions then.
Yes, I'll book up and get back to you! I need to learn HOL anyway,
and this manual seems like a good place to understand the foundations.
Email Gateway (Aug 18 2022 at 20:20):From: gottfried.barrow@gmx.com
Define a system of logic as a language with rules of inference to
interpret the language.
Define a language as a set of symbols with a set of rules for combining
the symbols.
Additionally, there is the meta-language which is used to describe and
define the object-language.
Let the choices of the meta-language be Isabelle/FOL or Isabelle/HOL,
and let the object-language be Tarski Geometry.
http://en.wikipedia.org/wiki/Tarski's_axioms
The question becomes this: Can either of these be used as a
meta-language to implement the object-language of Tarski Geometry?
To answer that question we can ask these questions:
1) Do these object-languages have the symbols we need for
Tarski Geometry, and let us combine them in the proper way
to create the language of Tarski Geometry.
2) Do these object-languages have rules of inference that allow
us to interpret the language correctly.
Isabelle/HOL has the standard set of logical connectives and
quantifiers, and it has natural deduction rules of inference. The syntax
it forces on you appears to be compatible with Tarski Geometry. It looks
like Isabelle/HOL can work as a meta-language to describe, define, and
use Tarski Geometry.
But I drop back concerning FOL.
Slawomir, you say that ZF is built on FOL. But the language of
first-order logic is a family of languages. Zermelo-Frankael sets isn't
built on a language of FOL, it is a first-order language, that is, a
language of first-order logic. Conceptually, Isabelle/FOL + Isabelle/ZF
is the first-order language of Zermelo-Frankael sets.
[pg.19, Language, Proof, and Logic, Barwise & Etchemendy]
...we talked about FOL as though it were a single language.
Actually, it is more like a family of languages, all having a
similar grammar and sharing certain important vocabulary items,
known as the connectives and quantifiers. Languages in this family
can differ, however, in the specific vocabulary used to form their
most basic sentences, the so-called atomic sentences.
Please refer to Bilaniuk's free book "A Problem Course in Mathematical
Logic", Def.5.1 Symbols pg.24, Def.5.2 Terms pg. 26, and Def.5.3
Formulas pg.27, though a friendlier definition of the symbols would give
us the full set of logical connectives and both the quantifiers.
http://euclid.trentu.ca/math/sb/pcml/pcml.html
Every first-order language must meet the requirements of the logical
symbols, which are Definition 5.1 items 1 to 5; it's the non-logical
symbols that allow them to be unique, Definition 5.1 items 6 to 8.
For the non-logical symbols, ZF has no constant or function symbols, and
it has membership as the one predicate symbol.
Now I switch to Tarski Geometry. I look at the wiki page, and it tells
me that it can formulated as a first-order language with the predicates
"betweenness" and "congruence".
Okay, but to elaborate on question 2 above, can Isabelle/FOL provide the
predicate "betweenness" to the first-order language of Tarski Geometry?
I go out on a limb now, and I say that first-order languages can only be
given predicates; that is, one language of FOL acting as a meta-language
can't create new predicates when creating a new language of FOL.
I could be wrong in my last paragraph. Regardless, if you're creating
predicates for Tarski Geometry, where the logic you're using is
Isabelle/FOL, aren't you really operating in the realm of "functional
programming"/"Isabelle's meta-logic"/ML/HOL/etc..
Regardless again, Isabelle/HOL appears to have the necessary ingredients
to act as a meta-language for any FOL object-language. When different
logics can be cleanly used as a meta-language to implement a particular
object-language, can it not be a case of "six of one, or a half dozen of
the other"?
There is the issue of minimalism. But if you only had to import
src/HOL/HOL.thy to implement Tarski Geometry, that would be pretty minimal.
I stop here. These have been the comments of a novice speaking from the
peanut gallery.
--GB
Email Gateway (Aug 18 2022 at 20:21):From: Jens Doll <jd@cococo.de>
Hello Bill, Ramana and all,
having printed out your opus as of June/4 and reading it byte by byte,
I'm still struggling with several propositions. The most important one
is the (allegation of a) diagonalization function
Has anyone seen a constructive version of the diagonalization function,
i.e. is (e.g. Cantor's) diagonalization function computable?
Heavy Reasoning,
Jens
Email Gateway (Aug 18 2022 at 20:21):From: Lawrence Paulson <lp15@cam.ac.uk>
I certainly do not want to get dragged into these interminable discussions. However, as a general remark: there is nothing mysterious about diagonalization functions. For example, the one for Russell's paradox is simply {X. X notin X}. Here, of course, the notion of computable is irrelevant, but it's certainly easily defined.
For proving undecidability of the halting problem, the definition is equally simple and it is computable if you assume the halting test itself to be computable, which is the point of the theorem.
Larry
Email Gateway (Aug 18 2022 at 20:21):From: Freek Wiedijk <freek@cs.ru.nl>
Jens:
It is certainly possible to prove in Coq (= constructively,
I hope) that there is no surjection from a set to its
powerset. I am not a regular Coq user so my proof probably
is twice as long as is necessary, and also it feels rather
strange to post a Coq script to an Isabelle mailing list,
but something like
Lemma diagonal : forall A : Type,
~(exists F : A -> (A -> Prop), forall f, exists x, f = F x).
unfold not. intros A [F H]. set (f := fun x => not (F x x)).
elim (H f). clear H. intros x H. assert (H' : f x <-> F x x).
rewrite H. tauto. unfold f in H'. tauto.
Qed.
seems to work.
Freek
Email Gateway (Aug 18 2022 at 20:24):From: Bill Richter <richter@math.northwestern.edu>
Ramana, I've been discussing the issue with Freek, who I'm very
impressed with, as miz3 is holding up very well under the torture
testing my 1300 lines of Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/OpenIntervalHilbertAxiom.ml.
The issue is almost entirely a matter of terminology. I say that the
proof assistant (PA) world ought to explain how to translate the
language of mathematical logic books (e.g. Enderton's) into PA
terminology. In particular there's the vexing issue of the term FOL.
I'm really happy with your understanding of Goedel Incompleteness:
The First Incompleteness Theorem says that if we fix a theory whose
axioms can be generated by a computer,[...]
Yes! And in math logic books, this is called FOL, and the infinite
set of axioms in ZFC fit into what they call axiom schemes. You
understand the infinite axiom biz quite well, as we see again here:
If the set of axioms can be generated by a computer, then all (and
only) the provable statements of a theory can also be generated by
a computer. This is why first-order logic [FOL] is "semidecidable".
Great! That's my meaning of FOL, which you used again here:
Right. I'm not sure this result has any particular name. The "nice set" of
FOL axioms means a "recursively enumerable set".
But now you mystify me by disagreeing with me at the end:
So what do proof assistants (Coq, Isabelle, HOL Light) do? I
would assume they all start with some FOL axioms and then deduce
axiomatic FOL proofs as one discusses in math logic. I contend
that the proof assistants must do that, because (by math logic)
they can't do anything else! And the mathematicians can't do
anything else either!
No it's not true, because neither proof assistants nor
mathematicians are restricted to FOL.
Now I think you switched over to to the (apparently more restrictive)
PA meaning of FOL. I contend that what I said is true, in the
following sense explained commonly in set theory books: Every theorem
proved today by mainstream mathematicians (let's forget large cardinal
axioms) has an FOL proof in ZFC. Of course it would be extremely
inconvenient for mathematicians to write up FOL ZFC proofs! Are we
arguing about what's convenient? I just want to see the big picture
right now, how PAs relate to the FOL math logic which I only
understand at a big picture level anyway.
Email Gateway (Aug 18 2022 at 20:27):From: Bill Richter <richter@math.northwestern.edu>
Makarius, I don't care for the way I wrote last time, and it took me
this long to come up with a nicer way to say it, which is:
I'm trying to use my math skills to get into the proof assistant game.
I know all of you are much better than I am at CS, and I would think
that you would all be better than I at mathematical logic as well.
And maybe you are, but I think I understand something that nobody ever
writes, so I wonder if folks do understand this.
Mathematical logic studies what you can and can't prove axiomatically
in first order logic (FOL). The Goedel Completeness Theorem
http://mathworld.wolfram.com/GoedelsCompletenessTheorem.html says
truth in every model implies an axiomatic proof, and the Goedel
Incompleteness Theorem says you can't write a computer program that
will print out all theorems of a model of the natural numbers:
http://mathworld.wolfram.com/GoedelsFirstIncompletenessTheorem.html
There's a simpler related result I don't know the name of, which says
that given any nice set of FOL axioms, you can write a computer
program to print out all the theorems that follow from them,
i.e. theorems which have axiomatic FOL proofs using these axioms.
Mathematicians basically restrict themselves to the FOL ZFC set theory
axioms, and so we can write a computer program that will print out (if
it runs indefinitely) every theorem that mathematicians well ever
prove (unless they adopt new axioms). Turing's proof of the Halting
problem (you can't write a infinite-loop checker) is just a
restatement of the Goedel incompleteness theorem. The Lambda Calculus
comes out of math logic, as it gives a definition of a recursive
function that's equivalent to Turing-machine definable.
The whole point of proof assistants is to make this math logic work!
Nobody's gonna run the simple program that prints out all the theorems
that follow from the FOL ZFC axioms and wait for a good theorem to pop
up. But you folks have written lots of smart proof assistants which
do great work on today's incredibly fast machines.
So what do proof assistants (Coq, Isabelle, HOL Light) do? I would
assume they all start with some FOL axioms and then deduce axiomatic
FOL proofs as one discusses in math logic. I contend that the proof
assistants must do that, because (by math logic) they can't do
anything else! And the mathematicians can't do anything else either!
But I'm puzzled because almost nobody talks this way in the proof
assistant world. Mizar (and Freek's miz3 port to HOL Light) seems
reasonably close to FOL axiomatic proofs. Although I don't know
exactly how close. I have this vague idea that Mizar does axiomatic
FOL proofs with a lot of the tedium automated away, e.g. manually
substituting variables. But I don't know. The things that folks
actually do---HOL, Isar, Pure---I don't understand. I would need to
have them explained in terms of Goedel's field of math logic,
i.e. axiomatic FOL proofs. So I propose that
if someone knows the answer, they tell me, and if nobody knows the
answer, let's run a thread on math logic which will eventually explain
how HOL, Isar, Pure etc relate to Goedel's FOL. I have very little to
contribute to such a thread beyond the note on the LC Y combinator and
Goedel incompleteness below.
Email Gateway (Aug 19 2022 at 08:51):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
It's lemma A1', not just A1. Its purpose is to turn axiom A1, which is
a sentence, into something more useful, with schematic variables that
can be instantiated. I think I figured out later that A1 [rule_format]
would achieve the same thing, without having to prove lemma A1' separately.
Sorry; it's taken me an awfully long time to get around to this, and
perhaps it's already been answered, but perhaps my answer will be useful
for someone.
Tim
<><
signature.asc
Email Gateway (Aug 19 2022 at 08:51):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
Tarski's axiom of continuity comes in two versions: a first-order axiom
schema, or a single higher-order axiom. If you use the higher-order
axiom, his axiom system is categorical. So, yes, there is a good reason
for using HOL for Tarski's axioms.
Again, sorry for taking so long to make this point.
Tim
<><
signature.asc
Last updated: May 07 2024 at 01:07 UTC