Knowledge theory has given up the assumption of “privileged concepts” that function as axiomatic foundations to control the logical value of other concepts or propositions. Similarly, you must give up the assumption that there are privileged places, notes of special and knowledge-ensuring quality.
Luhmann cites Richard Rorty's Philosophy and the Mirror of Nature as an example of philosophers abandoning "priviliged concepts". What does this even mean?
Rorty on "Priviliged Concepts"
If we peruse Rorty's book, we find he is attacking Plato's analysis of knowledge as "true, justified belief".
What does Plato mean by this? Well, suppose I have a coin which has one side say "yes" and the other side say "no". I ask a question, flip this coin, and it will always answer truthfully.
Do I gain knowledge by using my magic coin? Plato says no, because the process is entirely unjustifiable. Rorty attacks Plato's idea of justification as ambiguous and vague (and Rorty does make a few good points).
Why does it matter? Well, Neoplatonists believed we could figure out some set of axioms, and then deduce everything in the world. If only we could determine those axioms! But these axioms would have some privilged position, from which all truth flowed. This is, more or less, what Aristotle argued in his Metaphysics book Gamma, Posterior Analytics on the problem of regression, etc.
Rorty takes a nuanced position, which I'm not sure I fully appreciate. I think Rorty argues that we develop some ersatz "first principles" which are tentative (in the sense that we may revise them, under appropriate circumstances). But they are not divine, they are not immutable, they are not universal, they are not innate knowledge. Instead, these "principles" are built out of experience and learning. As we educate ourselves, they become reinforcing or else we amend them.
Analogy with "Position"
Some people have interpreted Luhmann as saying that organizing your Zettels into clusters is bad, and you should just sequentially number them based on position "at the time of incorporation". This fails to appreciate Luhmann's analogy with "privilged concepts" in the analysis of knowledge.
Scott Scheper suggests using a "skeleton" zettelkasten to get started, with some pre-determined slips based off of Wikipedia's outline of knowledge (or some other analogous source). It's curious, because — as Jillian M. Hess observes in her book How Romantics and Victorians Organized Knowledge, page 24 — Melville Dewey began his catalogue system as a remedy to the commonplace method's ambiguity. In other words, Scheper reinvents Dewey's method. This is precisely what Luhmann warns against in his (already cited) essay:
The result of working with this technique for a long time is a kind of second memory, an alter ego with which you can always communicate. It has, similar to our own memory, no pre-planned comprehensive order, no hierarchy, and surely no linear structure like a book. And by that very fact, it is alive independently of its author. The entire note collection can only be described as a mess, but at least it is a mess with a non-arbitrary internal structure.
[Emphasis mine]
Christian Tietze argues the opposite extreme, namely that any use of categories is bad. Instead we should use tags.
When I read 17th and 18th century European philosophy, everyone disagrees with each other because they use the same technical terms but attribute different definitions to them. I mention this because I feel in a similar situation when discussing "tags" versus "categories", and this makes me hesitate to criticize Christian too much — it feels quite likely we are using different terminology for the same concepts.
I think the crucial difference between "tags" and "categories" is that one item may have zero or more tags, but at most one category. In a filing cabinet, I file a piece of paper in exactly one folder, and the analogy would be with one item in a category.
Here I confess I never found tags useful on blogs, and it is even less useful on paper Zettelkasten. I suspect strongly that "register slips" and "the index" are the analogous quantities to "tags", and everyone agrees these are "killer features" to paper Zettelkasten.
I have been using Emacs...for a while now. I've found it useful to automate away common tasks using Lisp functions. One that has been recurring: write the creation date. Using something like datetime2 package in LaTeX (and assuming you're using PDFlatex), then the following command can be used to automatically determine the date and time you started writing:
The other bit of advice I have is to use Yasnippets. It's so much easier to start a new line, enter "d", hit tab, and have it expand to a definition environment (or have "thm" expand to a theorem environment). I have written a few snippets and found them wonderful.
I was asked about the details concerning my Zettelkasten (last time I checked, I had an estimated 7920 slips in it, which motivated the question). I thought I would write them down here with some examples.
The basic workflow boils down to:
Pick some reading material
Read it
Summarize the reading material in "literature notes"
Write some "permanent notes"
Integrate the "permanent notes" in my "zoo" [Zettelkasten]
Think about stuff
Write a manuscript using my permanent notes
Questions tend to crop up while writing a manuscript, which guides my choice of next reading material
Literature Notes
Definition.
A Literature Note is some writing which occurs when reading an article or book. Its contents vary considerably, but are used to create permanent notes. The literature notes are stored in a separate "shoe box".
The content of the literatuer notes varies depending on how familiar I am with the subject, or whether I can "see where it's going". These are written on quarter-slips of printer paper which are 4.25-inches wide and 5.5-inches tall. I also draw a stripe down the "top" using a blue highlighter, so I can see if I accidentally placed one in my Zettelkasten. [I store literature notes in a "bibliography shoe box".]
Figure 1. A [clipped] literature note from Mac Lane's Categories for the Working Mathematician.
If I'm having difficulty with some portion of an article or book, I sometimes look for other explanations, and insert "citations" to them. (Basically, a sentence like, "I honestly cannot follow [author] here, but I found [other reference] useful, specifically [section].")
Note I usually write small, and this is kinda large for my writing: it's about 3/16 inches, or 0.5 centimeters, for a line's height. I do not place lined paper behind the slip as I write, so it can get pretty curvy by accident.
The back of the literature notes include bibliographic information, and when I read it. This may include a "counter" for long chapters, which is just something like "(part 3 of N)". For technical articles, I also include the journal information. The idea is, if I completely lose access to my computer and papers, I can look up the source material again. Consequently, I give as much bibliographic information as possible.
Figure 2. The back of the literature note from figure 1.
I can refer to my literature notes when writing a permanent note, but I do not permit myself to refer to the original source when writing permanent notes. If I find I need to refer to the original source, I take that to mean my literature note-taking process was lacking somehow.
There are times when, for example, I read a source particularly from one perspective. (E.g., "How can this article about quantum hydrodynamics be used in this particular calculation I'm trying to do?") Later on, I realize there was some important aspect I neglected to take notes on (e.g., "Oh, that article about quantum hydrodynamics revived the 'particle model tradition' of Stokes, I totally missed that."). In that case, I re-read the article or book, and because I note when I read it on the back...it acts like a note to "future me" that there was some material I missed in the reading.
(And, for the record, I organize the literature notes by author-year-title.)
Permanent Notes
Definition.
A Permanent Note is some writing which is given an ID number, a "title", and some content; it is stored in the Zettelkasten.
Most of my notes are mathematical in nature, or written in a "mathematical style". I mean to say, I write them using "mathematical registers" to classify the sort of statement (theorem, example, definition, remark, etc.) and a summary of the result. Then the body of the slip of paper contains more precise details.
Figure 3. An example of a permanent note [front side].
I write on printer paper cut into quarters, so this is 5.5-inches wide and 4.25 inches tall. When writing on the paper, I have a college-ruled lined paper behind the quarter slip (which is why it appears so straight and clean).
ID Numbering. I should mention the ID number (the "6.1.2/3b" in the upper left-hand corner) has the following BNF grammar:
The "folder part" encodes the generic subject of the slip. For example, "6.1.2" is the folder part for the slip given. Here "6" refers to "Mathematical analysis", "6.1" refers to "Real analysis", and "6.1.2" refers to sequences of real numbers. Observe, the folder part moves from more general ("Real analysis") to the more specific; this is characteristic of all "folders" in my Zettelkasten.
The "file part" encodes the placement of a slip "inside" a "folder". The idea is that I'm sending "telegrams" to an intelligent (but completely ignorant) colleague. My colleague has never heard of real analysis (or anything else besides arithmetic and spelling). I need to order my telegrams somehow. The first attempt is to use Threads, just a sequence of numbers.
But when I want to discuss further an aspect of a thread (like, I want to pause and give a "sub-thread" consisting of examples), then I need to Branch off a slip to talk about some specific aspect. A single slip may have zero or more branches. I indicate a branch by writing a letter. Usually "a" is reserved for examples (unless there is a critical remark necessary to clarify something), then "b" is reserved for theorems about a concept.
For the example given, there is some fibbing here. That is to say, the ID number should really be "6.1.2/3b1". Why? Because letters act like different "flavors" of decimal separations. There shouldn't be any privilege to them (e.g., "a" is not more important than "b", there is no sense of priority, etc.). I haven't added any further theorems concerning "6.1.2/3", so I lazily truncated the ID number of the example to "6.1.2/3b".
Title. The title is usually of the form:
⟨title⟩ ::= ⟨register⟩ ". " ⟨summary⟩
As a mathematician, I habitually write "definition", "theorem", "proof", "remark", "example", etc., in an abbreviated form ["defn", "thm", "pf", "rmk", "ex", respectively]. Then I write a human readable summary of the result, like "Convergent sequences are bounded".
I previously mentioned introducing a "code" register when writing literate programs, and discussed the content of such notes.
Recently, I have also been experimenting with writing notes on history, and I have found registers of little use there. So your mileage may vary.
Figure 4. Another example of a permanent note [front side]. NOTE: all links are written in red ink (using non-red ink was a bad idea).
Also worth mentioning, the first "folder" is about my Zettelkasten's conventions. An example slip from this "folder" is given in Figure 4.
Content of a permanent note. This is pretty subjective, and varies considerably. For mathematics, I have a great luxury here since every "register" is a separate slip.
I have found it useful for propositions [lemmas, theorems, corollaries, etc.] to give a "proof sketch" below the theorem statement. If there is some justification for a step, it's a branch off the slip.
Examples are just special kinds of propositions, and the emphasis of its content is the proof.
I can give some concrete "tricks" to writing permanent notes, they both boil down to relating new material to existing content already in the Zettelkasten.
Example: Creating examples. A useful exercise is to go back to examples existing in my Zettelkasten, and try to use it as an example of the new material. For instance, I have the "symmetries of the tetrahedron" as an example of a group. When reading figure 1, I may pose the question: can we express the symmetries of the tetrahedron as a universal arrow? (Not in any obvious way, but there are other gadgets which may be a universal arrow, so I keep looking.) When I find an example [call it a "widget"], I create a new permanent note entitled "Ex: widget (Universal Arrow)", the first sentence is "A widget [link] is a universal arrow." The "[link]" refers back to the original slip which first discussed the "widget".
Usually this process is more "subconscious" than actually flipping through every slip in my Zettelkasten. With the universal arrow example, I usually know an example would be an algebraic gadget, so I can restrict my focus to the "Abstract algebra" folder; even then, I can restrict attention to a few "subfolders".
Example: Translating content. Another way to approach creating permanent notes is to "translate" old material from a different domain to whatever I just read. For example, I learned the Krull-Schmidt theorem for rings and modules. But currently I am studying finite group theory. Could I frame an analogous theorem for groups?
Convention: formal proof sketches. I try to write the mathematical proofs using Wiedijk's Mathematical Vernacular, which is a synthesis of formal proof steps while leaving the terms and formulas informal. I also write "big step proofs", or what Wiedijk calls formal proof sketches.
Back of permanent notes. On the back side of a permanent note is a list of references which were used for the slip. They are lists to where one could find the same result in the literature which I've read, and refer to entries in my "bibliography apparatus".
Integration into the Zettelkasten. Usually, I study a book or article, write a number of permanent notes without any ID number. Only after I have extracted all the information needed from my source, I begin to think about how to integrate the new permanent notes into my Zettelkasten.
Sometimes the order of material in a book is "backwards" (it happens a lot in physics), so the corresponding permanent notes are in reverse order. Less frequently, the material needs to be partitioned to separate parts of the Zettelkasten. There has not been a time when the material is "completely disconnected" from each other, in the sense that they are added to different threads.
Gorenstein, Lyons, and Solomon (and friends) have been writing a consolidated proof for the classification theorem for finite simple groups...since 1994. In fact, it's still a work in progress. How big will it be?
At present, there is an expected additional 4 volumes coming (according to David Roberts's answer on Mathoverflow). Performing a linear regression on the number of pages in terms of the volume number, we can make a prediction. Here's the R code doing this:
This gives us a better fit (adjusted R-squared of 0.908) with a better error estimate (with 95% probability, it will be 6080 pages give or take 40 pages).
Tl;dr2: the classification of finite simple groups can be expected to be around 6080±40 pages long.
I've been re-reading John Harrison's Handbook of Practical Logic and Automated Reasoning (a wonderful book), with an eye towards writing notes for my Zettelkasten.
What I have done, out of habit, is I've reworked the code in Standard ML (as opposed to OCaml). I've added a "register" (mathematicians would recognize them as "theorem environments" in LaTeX) for source code, and the template for writing such notes on a 5.5 inch by 4.25 inch (A6) slip of paper looks like:
[id number]
Code [name of chunk]
[English summary of the code, or the algorithm, or...]
⟨[name of chunk]⟩≡
[Standard ML code here]
Just replace the bracketed italicized text (including the brackets) with your own text. I do write a horizontal line separating the "code block" from the "text block", and underline the "Code" part of the title.
I follow the general heuristics Knuth suggests for literate programming, even using the names of code chunks in angled braces as if they were statements. Following some of the early handwritten documents on Standard ML, I underline keywords like "if", "then", "else", "case", "fun", etc., in the code block.
While reading Harrison's book, I add unit tests, write up examples, etc. This isn't done "in the abstract", I actually type the code up on a computer (e.g., here is my implementation of most of the propositional logic code).
One advantage to this is that we can prove properties about the code snippet in branches off the code zettel. Another advantage, giving a good human-level summary of the code snippet helps greatly with Harrison's book, since the techniques from chapter 3 make another appearance in chapter 6 (i.e., 300 pages later) and I forget some of the nuances surrounding the implementation ("Is skolem called before or after nnf?"), I can just glance at the snippets for guidance.
Another useful aspect of using a Zettelkasten for studying theorem provers is that it facilitates blending notes from multiple books seamlessly. I noticed this accidentally, when I was unsatisfied with Harrison's description of Herbrand universes, then started reading Chang and Lee's Symbolic Logic and Mechanical Theorem Proving (1973) description of Herbrand universes.
There are other aspects of Zettelkasten which seems uniquely suitable for studying theorem provers, but I digress.
I'm experimenting with using a Zettelkasten for literate programming "by hand" more generally, which is a bizarre but fascinating experience, especially when exploring monads in Standard ML.
Anyways, I just wanted to make note of this quirky note-taking system for literate programming.
1.
Suppose we have successfully formalized the classification theorem for
finite simple groups in your favorite theorem prover (Lean, HOL, Coq,
Mizar, whatever). In a century's time (or several centuries from now),
do you think your theorem prover will still be around and backwards
compatible? If not, what good would the formalization be?
1.1.Remark (Concerns have been partially realized).
We stress, despite the concerns raised being hypothetical and distant,
they have been partly realized already. The Automath project's
efforts to translate Landau's Foundations of Analysis would have
been lost to history but for Freek Wiedijk's heroic efforts. Or, hitting
closer to home for many, Lean 3 broke compatibility with Lean 2; and, as
I understand it, there still remains a large quantity of Lean 2
libraries not yet ported. Worse, Lean 4 broke compatibility with Lean 3,
and the Xena project's library has not yet ported to Lean 4. The idea
that we would encode mathematical knowledge in one single theorem prover
seems riskier than encoding it in natural language. Why not try to have
the best of both worlds?
2. Readable Proofs.
One of the roles for proofs in mathematics is
communication. Hence we need something analogous to the notion of
"readable code" in programming: readable proofs. Consider the
following proof, tell me what it does (no cheating!):
prove
('!p q. p * p = 2 * q * q ==> q = 0',
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM 'EVEN') THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN 'm:num' SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL ['q:num'; 'm:num']) THEN
POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;
Or the following:
Proof.
rewrite EL2 with (p_prime := p_prime) (p_odd := p_odd) by (omega || auto).
rewrite EL2 with (p_prime := q_prime) (p_odd := q_odd) by (omega || auto).
rewrite m1_pow_compatible. rewrite <- m1_pow_morphism.
f_equal. rewrite <- QR6. unfold a. unfold b. auto.
rewrite <- Zmult_0_r with (n := (p - 1) / 2).
apply Zmult_ge_compat_l. omega. omega.
Qed.
I honestly wouldn't guess the first example had to do with proving
${\sqrt{2}\notin\mathbb{Q}}$, nor would I have imagined the second had to do with
the law of quadratic recipricocity. (The first in HOL Light, the second
in Coq.) What do you suppose mathematicians of the 25th century would
think of these proofs? Would our efforts formalizing mathematics in a
theorem prover yield fruit akin to Euclid's Elements, or would it
be more indecipherable than Russell and Whitehead's Principia?
Hence, I would like to assess the following question:
3.Puzzle.What qualities make a proof "readable"?
4. Sources.
We're not in the wilderness on this matter. Some very smart people have
thought very hard about this question. But we haven't progressed much in
the past few decades, compared to designing programming languages. We
all seem to draw waters from the same well.
Andrzej Trybulec created Mizar [10] specifically for
readability. Over the years, Mizar went from an abstract idea to a
concrete realization, iteratively improving its input language to make
it resemble a working mathematician's proofs. A cynical critic may
deride Mizar as merely natural deduction in Pascal syntax, but that
concedes the point: it's readable and understandable on its own, without
relying on the computer to tell us the "proof state" and remaining
goals in a proof. (Empirically, it turns out that Mizar reflects how
mathematicians write, based on a cursory glance at 40k articles;
see Josef Urban's email
to the Mizar mailing list.)
(For our earlier examples, I personally think that Mizar's proof of the theorem of quadratic recipricocity, Th49 of int_5.miz, while long, is clear and readable...even if I don't fully understand Mizar. Similarly, the proof that $\sqrt{2}\notin\mathbb{Q}$ is the first theorem in irrat_1.miz. It's longer than I would find in a textbook, as are all formal proofs, but I have no difficulty making sense of it.)
The other major source of inspiration, I think, is Mark Wenzel's Isar
front-end for Isabelle [13] (and enlightening
discussion of a prototype [12]). Here the system
emerges bottom-up, as discussed in §3.2 of Wenzel's
thesis [13]. Other theorem provers attempted to
simply copy/paste Isar commands, but apparently they never caught on. I
suspect this is due to copying the superficialities, rather than drawing
upon the underlying principles, produced an awkward input language.
There are other sources worth perusing, like Zammit's "Structured Proof
Language" [17] among others. We also mention Isar
inspired many prototypes to adapt Mizar-style proofs to other theorem
provers (Corbineau's Czar [2], Giero and Wiedijk's MMode [3],
Harrison's Mizar Mode for HOL [4]).
Also worth mentioning is ForTheL[11] which
emerged from the Soviet SAD theorem prover [9], possibly
a future input language for Lean.
I especially want to point out ForTheL[11] as a stand-out, partly because it was designed behind the Iron Curtain, and partly because it's more of a controlled language which resembles natural language.
5. Declarative proofs.
One bit of terminology, John Harrison [5] calls
the structured proof style "declarative style proofs", which seems
fine. Some fanatics of the procedural camp dislike the term. Giero and
Wiedijk [3] point out the
differences between procedural and declarative styles are:
a procedural proof generally run backward (from goal to the
assumptions), whereas declarative proofs run mostly forwards (from the
assumptions to the goal);
a procedural proof generally does not have statements containing
the statements which occur in the proof states, whereas declarative
proofs do;
a procedural proofs have few proof cuts, whereas declarative
proofs have nearly one cut for each proof step.
It turns out these qualities do make a difference on the
readability of a proof script. But this is a bit like trying to learn an
author's writing style by examining the statistics of the author's
writing, like "Average number of words per sentence" or "Average
number of syllables per word".
6. Natural deduction, vernacular.
A key insight worth discussing further is that declarative/structured
proofs emerge from the natural deduction calculus. Curiously,
Jaśkowski [6] (who invented natural deduction
independent of, and earlier than, Gentzen) does this in his original
paper. Wiedijk [15] considers this avenue using a formal
grammar for the proof steps, leaving notions like "term" and
"formula" [i.e., the heart of a proposition/theorem] informal.
So far, so good; but this has been predominantly first-order logic. How
do we articulate readable proofs for type theory?
7.
We construct proof steps for a declarative proof style by assigning
"keywords" to rules of inference in natural deduction.
The problem with trying to find a readable proof format from natural
deduction for type theory is, well, there are a lot more inference rules
in the calculus of constructions (as opposed to, say, first-order
logic).
The Lean4 developers have unwittingly started the road to reinventing
lambda-typed lambda calculus, which has fewer rules and ostensibly could
be encoded into a declarative proof style input.
8.
One linguistic avenue may be found in de Bruijn's "mathematical
vernacular" [1], which then evolved into
WTT [7].
8.1.Remark (Soft typing).
What's worth noting is de Bruijn [1] states
in §1.17, "In particular we have a kind of meta-typing (the 'high
typing', see Section 3.6) in the language, whereas most other systems
would have such things in the metalanguage." We now call such 'high
typing' either 'soft typing' [16], or 'semi-soft
typing' [8].
9.
Another avenue would be to weaken existing structured proof formats, so
they become independent of foundations (e.g., instead of writing
"${x\in\mathbb{N}}$", we would write "${x}$ be a natural number" — type
theory provers would translate this into "${x{:}\mathbb{N}}$", and set theory
provers would translate this into "${x\in\mathbb{N}}$" as before).
If GNU Hurd's failures have taught us anything about engineering, it's
that "a bird in the hand is worth two in the bush." That is to say,
it's wiser to take an existing working framework, and modify it
slowly until it becomes what we want.
10. Conclusion?
If this post seems less-than-satisfying, that's probably because I've
only identified a problem.
No solutions have been offered. That's because this is a hard problem
somewhere between language design (very hard) and mathematical logic.
Since we lack a robust framework for designing languages, this is far
more of an art than science.
Although we have fewer than a half-dozen examples of declarative proof
styles (really, maybe 3?), we have some avenues of exploration. But the
design space may be much larger than we realize: we just lack the tools
to describe it adequately.
One closing thought I'd pass off, though, is that type theorists encode
logic in a rather protracted manner. It may be that structured proofs for
type theory would be forced to "compile down" into many more steps, or maybe
we just haven't adequately found a way to connect type theory to working
mathematics.
See also F.3 of Selected Papers on Automath for a revised
version of this manuscript.
Pierre Corbineau,
"A Declarative Language For The Coq Proof Assistant".
In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, Types for Proofs and Programs, International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised Selected Papers,
volume 4941 of Lecture Notes in Computer Science, pages 69–84. Springer, 2007.
https://kluedo.ub.uni-kl.de/frontdoor/deliver/index/docId/2100/file/B-065.pdf
Mariusz Giero and Freek Wiedijk,
"MMode: A Mizar Mode for the proof assistant Coq".
Technical report, ICIS, Radboud Universiteit Nijmegen, 2004.
https://www.cs.ru.nl/ freek/mmode/mmode.pdf
John Harrison,
"A Mizar Mode for HOL".
In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '96, volume
1125 of LNCS, pages 203–220. Springer, 1996.
https://www.cl.cam.ac.uk/ jrh13/papers/mizar.html
Fairouz Kamareddine and Rob Nederpelt,
"A refinement of de Bruijn's formal language of mathematics".
Journal of Logic, Language, and Information13, 3 (2004), pp.287–340
Markus Wenzel,
"Isar — a Generic Interpretative Approach to Readable Formal Proof
Documents".
In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs'99, LNCS 1690, (c) Springer, 1999.
https://www21.in.tum.de/ wenzelm/papers/Isar-TPHOLs99.pdf
Markus Wenzel,
"Isabelle/Isar — a versatile environment for human-readable formal
proof documents".
PhD thesis,
Institut für Informatik, Technische Universität München, 2002.
https://mediatum.ub.tum.de/doc/601724/601724.pdf
1.Definition. Let ${G}$ be a group; denote its group structure as the tuple ${(G,e_{G},\star_{G},\iota_{G})}$ where ${\iota_{G}}$ is the inverse operator, ${e_{G}}$ is the identity element, ${\star_{G}}$ is the binary composition operator.
We define a Subgroup of ${G}$ to consist of a subset ${H\subseteq G}$ equipped with ${G}$'s group structure, i.e.,
the binary operation restricted to ${H}$, ${\star|_{H}\colon H\times H\to G}$
the inverse operator ${\iota|_{H}\colon H\to H}$
the identity element from ${G}$, ${e_{G}\in H}$
such that
the group composition is closed on ${H}$, i.e., ${\{h_{1}\star|_{H}h_{2}|h_{1},h_{2}\in H\}\subseteq H}$
group inversion is closed in ${H}$, i.e., ${\iota|_{H}(H)\subseteq H}$
the usual group properties holds for this group structure induced on ${H}$.
If further ${H\neq G}$, we call ${H}$ a Proper Subgroup of ${G}$.
1.1.Remark. We denote ${H<G}$ if ${H}$ is a proper subgroup of ${G}$, and ${H\leq G}$ if ${H}$ is a generic subgroup of ${G}$.
2.Example (Trivial subgroups). For any group ${G}$, there are always two subgroups available: ${G}$ itself, and the trivial subgroup ${\mathbf{1}}$ consisting of only the identity element. Since these subgroups come "for free", we call them Trivial Subgroups.
3.Example (Subgroups of dihedral group). Let ${n\in\mathbb{N}}$ be greater than 2. Recall the dihedral group ${D_{n}}$ consists of rotations by ${2\pi/n}$ radians and reflections. We have two subgroups (at least): one generated by rotations alone, the other generated by reflections alone.
The subgroup of rotations is a finite group consisting of ${n}$ elements. It's a cyclic group, isomorphic to ${\mathbb{Z}/n\mathbb{Z}}$.
The subgroup of reflections is less exciting. There are two elements in it: reflection about the ${x}$-axis, and the identity transformation. This is a cyclic subgroup of order 2, isomorphic to ${\mathbb{Z}/2\mathbb{Z}}$.
4.Example (NON-Example: subset alone insufficient). Consider modular arithmetic ${\mathbb{Z}/p\mathbb{Z}}$ for some prime ${p}$. This is a group consisting of a set ${\{0,1,\dots,p-1\}}$ equipped with addition modulo ${p}$, inversion maps ${m}$ to ${-m\equiv p-m\bmod{p}}$.
Although the underlying set is a subset of the additive group ${\mathbb{Z}}$, the addition operation is a different function. Consequently, the group structure on ${\mathbb{Z}/p\mathbb{Z}}$ is not equal to the group structure on ${\mathbb{Z}}$. The moral: being a subset alone is insufficient.
5.Example (Symmetric group). Let ${n\in\mathbb{N}}$. The symmetric group ${S_{n}}$ consists of permutations of the set ${\Omega_{n}=\{1,2,\dots,n\}}$. We can consider ${k\leq n}$, and then we have ${S_{k}\leq S_{n}}$ by restricting to permutations of the subset ${\Omega_{k}\subseteq\Omega_{n}}$.
6.Example. Recall the general linear group ${\mathrm{GL}(n,\mathbb{R})}$ is the group of ${n\times n}$ invertible matrices over the real numbers, using matrix multiplication as its binary operator, and matrix inversion for its group inverse. Also recall the determinant
$$ \det\colon\mathrm{GL}(n,\mathbb{R})\to\mathbb{R}^{\times} \tag{1}$$
is a group morphism. Its kernel is a subgroup, called the Special Linear Group, denoted
$$ \mathrm{SL}(n,\mathbb{R})=\{M\in\mathrm{GL}(n,\mathbb{R})|\det(M)=1\}. \tag{2}$$
The reader can check it is closed under matrix multiplication and matrix inversion.
7.Example. Let ${G}$ be any group. If ${g_{1},g_{2}\in G}$, then their commutator is the element ${[g_{1},g_{2}]=g_{1}g_{2}g_{1}^{-1}g_{2}^{-1}\in G}$. We can construct the Commutator Subgroup of ${G}$, denoted ${[G,G]}$ or (more commonly but more confusingly) by ${G'}$ in the literature, by considering the subgroup generated by commutators of elements of ${G}$. Then an arbitrary element of the commutator subgroup looks like
$$ {} [g_{1},g_{2}][g_{3},g_{4}](\dots)[g_{2n-1},g_{2n}]\in[G,G] \tag{3}$$
and we use multiplication from ${G}$.
1. Exercises
Exercise1. Let ${H_{1}}$, ${H_{2}\leq G}$. Is ${H_{1}\cap H_{2}}$ a subgroup of ${G}$?
Exercise2. Let ${H_{1}}$, ${H_{2}\leq G}$. Is ${H_{1}\cup H_{2}}$ a subgroup of ${G}$?
Exercise3. Let ${\varphi\colon G\to K}$ be a group morphism. Is the image of ${\varphi}$ a subgroup of ${K}$?
If ${H<K}$, is its preimage under ${\varphi}$ a subgroup of ${G}$?
Exercise4. Prove or find a counter-example: if ${G}$ is a cyclic group, then every subgroup is cyclic.
2. Normal Subgroups
8. The special linear group is a rather special situation (no pun intended). We can prove that, for any ${M\in\mathrm{SL}(n,\mathbb{R})}$ and for any ${T\in\mathrm{GL}(n,\mathbb{R})}$, we have ${XMX^{-1}\in\mathrm{SL}(n,\mathbb{R})}$. Really? Look, take its determinant:
$$ \begin{split} \det(XMX^{-1})&=\det(X)\det(M)\det(X)^{-1}\\ &=\det(M)=1. \end{split} \tag{4}$$
Its a property shared by the kernel of any group morphism ${\varphi\colon G\to H}$, we'd have ${k\in\ker(\varphi)}$ and ${g\in G}$ satisfy ${\varphi(gkg^{-1})=\varphi(g)\varphi(k)\varphi(g)^{-1}=\varphi(k)=e_{H}}$. This gives us a particular kind of subgroups.
9.Definition. Let ${G}$ be a group. A Normal Subgroup of ${G}$ consists of a subgroup ${H\leq G}$ such that
Closed under conjugation by group elements: for any ${h\in H}$ and for any ${g\in G}$, we have ${ghg^{-1}\in H}$.
9.1.Remark. Care must be taken for the normality property: all we ask is for ${ghg^{-1}\in H}$, not that ${ghg^{-1}=h}$.
9.2.Remark (Notation). We denote a normal subgroup ${N}$ of ${G}$ by ${N \triangleleft G}$, and ${N \trianglelefteq G}$ if ${N}$ is a proper normal subgroup of ${G}$. There are a couple ways of remembering which way the triangle points: one is that we just turn the subgroup notation ${N\leq G}$ into a triangle, the other is that it "snitches" on (i.e., points to) the normal subgroup.
10.Example. The trivial subgroups are trivially normal.
11.Example. For the Dihedral group ${D_{n}}$, we have a couple subgroups (one generated by rotations, the other generated by reflections). Is one of them normal?
The rotation subgroup is generated by ${r}$ and satisfies ${r^{n}=1}$. The reflection subgroup is generated by ${s}$ and satisfies ${s^{2}=1}$. Together, they have ${s\circ r^{k}\circ s=r^{-k}}$. This implies the rotation subgroup is normal.
Is the reflection subgroup normal?
12.Theorem. Let ${G}$ be a group. If ${G}$ is Abelian, then every subgroup ${H\leq G}$ is normal.
Proof: Assume ${G}$ is Abelian. Let ${H\leq G}$ be an arbitrary subgroup of ${G}$, let ${g\in G}$ and ${h\in H}$ be arbitrary group elements. Then conjugation looks like ${g+h-g=h}$. Hence ${H}$ is a normal subgroup of ${G}$ by Definition 9. ∎
13.Example (Converse to Theorem 12 is false). Consider the quaternion group ${Q_{8}}$ generated by ${i^{4}=j^{4}=k^{4}=(ijk)^{2}=1}$ and so ${ij=k}$, ${jk=i}$, ${j=ki}$. We really have only 8 elements in ${Q_{8}}$: ${1}$, ${-1}$, ${i}$, ${-i}$, ${j}$, ${-j}$, ${k}$, ${-k}$. But we only need two of the "purely imaginary" elements (${i}$, ${j}$, ${k}$) to generate the entire group.
The proper subgroups would be generated from one complex generator, or from ${-1}$. We claim they are all normal. The case of ${\{\pm1\}<Q_{8}}$ is obviously normal, since ${x(-1)x^{-1}=-1}$ for any ${x\in Q_{8}}$.
The reasoning for proper subgroups generated by one imaginary element resembles one another, so let's consider the subgroup generated by ${i}$. Then we see
$$ jij^{-1}=-jk=-i \tag{5}$$
and
$$ j^{3}ij^{-3}=(-j)i(j)=i. \tag{6}$$
Similarly we'd find, from ${i^{3}=-i}$, that
$$ ji^{3}j^{-1}=i \tag{7}$$
and
$$ j^{3}i^{3}j^{-3}=-i. \tag{8}$$
Thus the subgroup generated by ${i}$ is closed under conjugation from all elements from ${Q_{8}}$.
Really? Well, any generic element in ${Q_{8}}$ looks like ${i^{m}j^{n}}$. Its inverse would be ${(i^{m}j^{n})^{-1}=j^{-n}i^{-m}}$. So conjugation by these elements would amount to multiplying the element ${i^{\ell}}$ from the subgroup by some ${i^{q}}$. But that's okay: elements of the form ${i^{q}}$ belong to the subgroup anyways.
14.Theorem. If ${\varphi\colon G\to H}$ is a group morphism, then ${\ker(\varphi)}$ is a normal subgroup of ${G}$.
15.Theorem. Let ${G}$ be a group. Every normal subgroup ${N\triangleleft G}$ is the kernel of some group morphism.
15.1.Remark. We do not yet have the technology to prove this, yet, but it is true. Basically, we construct a morphism by taking ${g\in G}$ and mapping it to cosets ${gN=\{gn\in G|n\in N\}}$. The difficulty we have is that the image of this mapping is the collection of left cosets of ${N}$, which may or may not be a group. Further, it was rather arbitrary mapping it to left cosets of ${N}$: why not map ${g}$ to ${Ng=\{ng\in G|n\in N\}}$? Wouldn't these be distinct (i.e., not equal) mappings?
3. Exercises
Exercise5. Find the normal subgroups of the symmetric group ${S_{n}}$.
Exercise6. Let ${G}$ be a group, ${H\triangleleft G}$ be a normal subgroup, and ${N\triangleleft H}$ be a normal subgroup of ${H}$. Is ${N}$ a normal subgroup of ${G}$?
Exercise7. Let ${G}$ be a group, recall the commutator subgroup from Example 7 that ${[G,G]}$ is a subgroup of ${G}$. Prove or find a counter-example: the commutator subgroup is a normal subgroup of ${G}$.
Exercise8. Let ${\varphi\colon G\to H}$ be a group morphism, ${N\triangleleft G}$ be a normal subgroup. Is ${\varphi(N)}$ a normal subgroup of ${G}$? Consider the cases when ${\varphi}$ is injective, and when ${\varphi}$ is surjective.
Exercise9. Let ${\varphi\colon G\to H}$ be a group morphism, and ${N_{H}\triangleleft G}$ be a normal subgroup. Is the preimage ${\varphi^{-1}(N_{H}) = \{g\in G|\varphi(g)\in N_{H}\}}$ a normal subgroup of ${G}$? Is it even a subgroup?
I've been writing terse notes using something like the ISO-2145 standard. Could some TeX macros be written to support writing such notes? Of course!
Like amsart's subsections and subsubsections, I wanted my sections to be "runin style" (i.e., an unindented paragraph with a leading number, possibly with some label in bold, which is separated by vertical space from the previous paragraph). Following Knuth's WEB macros, I use \M to create a new unlabeled "section", and \N{label} to create a new labeled "section". These macros increment the section number, makes the section number (and label, if present) in bold, and does not indent the section's first paragraph.
But I wanted to allow arbitrary depths for "section numbers". What I did was treat the section number like a stack. When I wanted to work on a new subsection level, I call \M[1] (or, for labeled subsections, \N[1]{My label for the new subsection.}).
If I want to "ascend" back to the parent section, I call \M[-1] (and \N[-1]{...}) which will pop the section stack, then increment the top of the stack.
Should I want to move more than one level up or down, I simply call \M[n] (or \N[n]{...}) for any nonzero integer n. If called with n=0, then it's treated as \M (and \N{...}, resp.).
Retrospective
If I were to do this all over again, I would probably use different variable names (for example, I would probably use \chunkctr instead of \section for the counter name). But I just wanted to see if it was possible.
Also, this code could work in LaTeX, but needs some small modifications. (Well, mostly dealing with making \chunkctr a bona fide counter, so \refstepcounter could use its magic for referencing things properly.)
I guess if I wanted to be fully general, I would have some additional parameters to allow customizing the vertical spacing for separating the sections, the horizontal space between the section number and the next symbol, etc.
Code and Worked Example
\newcount\section
\section=0
% technically, sectionDepth is not needed, but it's to avoid popping off
% "too many sections"
\newcount\sectionDepth \sectionDepth=0
% \secprefix will be redefined to append the current section number
% followed by a period
\def\secprefix{}
% \pushSection simply appends "\the\section." to \secprefix's current value
\def\pushSection{
\global\advance\sectionDepth by1
\let\sectmp\secprefix
\xdef\secprefix{\sectmp\the\section.}
}
% update \secprefix from "a.b.(...).c.d" to "a.b.(...).c"
% and set \section to "d" (as a number)
\def\popSection{
\def\newPrefix{}
\global\advance\sectionDepth by-1
\def\updatePrefix##1.##2\endUpdate{
\ifx\relax##2 % if we are at the last number
% globally set \secprefix to be the leading (n-1) section numbers
\xdef\secprefix{\newPrefix}
% globally set \section to be the last section number from \secprefix
\global\section=\number##1
\else
\xdef\newPrefix{\newPrefix##1.}
\updatePrefix##2\endUpdate
\fi}
\ifx\secprefix\relax % if \secprefix is empty
\else
\expandafter\updatePrefix\secprefix\relax\endUpdate
\fi
}
\def\thesection{\secprefix\the\section.}
\def\stepSec{\global\advance\section by1}
\def\downOne{
\pushSection
\global\section=0
}
\def\upOne{
\popSection
}
\newcount\secIter \secIter=0
% \up ascends back to one of the parent sections, ascending #1 levels
\def\up#1{ % #1 is a negative integer
\ifnum\sectionDepth>0%
\secIter=#1%
\multiply\secIter by-1
% but \sectionDepth is a non-negative integer, so transform it
\ifnum\secIter>\sectionDepth%
\global\secIter=\sectionDepth
\fi%
\loop
\ifnum\secIter>0
\upOne
\advance\secIter by-1
\repeat%
\fi%
}
% down appends #1 subsections to the given section number
\def\down#1{ % #1 is a positive integer
\global\secIter=#1%
\loop
\ifnum\secIter>0
\downOne
\advance\secIter by-1
\repeat%
}
% move up or down #1 layers, does nothing if #1 is zero
\def\adjustSection#1{\ifnum#1<0\up{#1}\else{\ifnum#1>0\down{#1}\fi}\fi}
% \M is used for unlabeled paragraphs
\def\Mlabel{\medbreak\noindent\ignorespaces%
{\bf\thesection\ignorespaces}\enspace\ignorespaces}
\def\Mnone{\stepSec\Mlabel}
\def\Mmany[#1]{\adjustSection{#1}\Mnone}
\def\xM{\ifx\tmp[\expandafter\Mmany\else\Mnone\fi}
\def\M{\futurelet\tmp\xM}
% \N is used for labeled paragraphs
\def\Nlabel#1{\medbreak\noindent\ignorespaces%
{\bf\thesection\ignorespaces\enspace#1\ignorespaces}\enspace\ignorespaces}
\def\Nnone#1{\stepSec\Nlabel{#1}}
\def\Nmany[#1]#2{\adjustSection{#1}\Nnone{#2}}
\def\xN{\ifx\tmp[\expandafter\Nmany\else\Nnone\fi}
\def\N{\futurelet\tmp\xN}
\M
This is a test to see if this works.
\M I hope it works.
\M[1]
And this should be \S{2.1}, I hope.
\N[1]{Claim:} This should be \S{2.1.1}.
\M[-1]
This should be \S{2.2}.
\M[3]
This should be \S{2.2.0.0.1}, I hope?
\N[-3]{Theorem.}%
This is \S3, yes?
\M[-1]
No, this is \S3.
\bye
Addendum: in LaTeX
It turns out to be a straightforward generalization to LaTeX:
\documentclass{article}
\usepackage{fullpage}
\newcounter{chunk}
\def\setSection#1{\setcounter{chunk}{#1}}
\def\stepSec{\refstepcounter{chunk}}
% technically, sectionDepth is not needed, but it's to avoid popping off
% "too many sections"
\newcount\sectionDepth \sectionDepth=0
% \secprefix will be redefined to append the current section number
% followed by a period
\def\secprefix{}
\renewcommand\thechunk{\secprefix\arabic{chunk}.}
% \pushSection simply appends "\arabic{chunk}." to \secprefix's current value
\def\pushSection{
\global\advance\sectionDepth by1
\let\sectmp\secprefix
\xdef\secprefix{\sectmp\arabic{chunk}.}
}
% update \secprefix from "a.b.(...).c.d" to "a.b.(...).c"
% and set \chunk counter to "d" (as a number)
\def\popSection{
\def\newPrefix{}
\global\advance\sectionDepth by-1
\def\updatePrefix##1.##2\endUpdate{
\ifx\relax##2 % if we are at the last number
% globally set \secprefix to be the leading (n-1) section numbers
\xdef\secprefix{\newPrefix}
% globally set \chunk to be the last section number from \secprefix
\setSection{\number##1}
\else
\xdef\newPrefix{\newPrefix##1.}
\updatePrefix##2\endUpdate
\fi}
\ifx\secprefix\relax % if \secprefix is empty
\else
\expandafter\updatePrefix\secprefix\relax\endUpdate
\fi
}
\def\downOne{\pushSection\setSection{0}}
\def\upOne{\popSection}
\newcount\secIter \secIter=0
% \up ascends back to one of the parent sections, ascending #1 levels
\def\up#1{ % #1 is a negative integer
\ifnum\sectionDepth>0%
\secIter=#1%
% but \sectionDepth is a non-negative integer, so transform it
\multiply\secIter by-1
\ifnum\secIter>\sectionDepth%
\global\secIter=\sectionDepth
\fi%
\loop
\ifnum\secIter>0
\upOne
\advance\secIter by-1
\repeat%
\fi%
}
% down appends #1 subsections to the given section number
\def\down#1{ % #1 is a positive integer
\global\secIter=#1%
\loop
\ifnum\secIter>0
\downOne
\advance\secIter by-1
\repeat%
}
\def\adjustSection#1{\ifnum#1<0\up{#1}\else{\ifnum#1>0\down{#1}\fi}\fi}
%% \M is used for unlabeled paragraphs
\newcommand\M[1][0]{\adjustSection{#1}\medbreak%
\stepSec\noindent\ignorespaces%
\textbf{\thechunk\ignorespaces}\enspace\ignorespaces}
%% \N is used for labeled paragraphs
\newcommand\N[2][0]{\adjustSection{#1}\medbreak%
\stepSec\noindent\ignorespaces%
\textbf{\thechunk\ignorespaces\enspace#2\ignorespaces}\enspace\ignorespaces}
\begin{document}
\M
This is a test to see if this works.
\M I hope it works.
\M[1]
And this should be \S{2.1}, I hope.
\N[1]{Claim:} This should be \S{2.1.1}.
\M[-1]
This should be \S{2.2}.
\M[3]
This should be \S{2.2.0.0.1}, I hope?
\N[-3]{Theorem.}%
This is \S3, yes?
\M[-1]
No, this is \S3.
\M[0] This should be \S4.
\N[0]{Corollary.} This is \S5?
\end{document}
F. Wiedijk, "Mizar's Soft Type System." In: K. Schneider & J. Brandt (eds.), Theorem Proving in Higher Order Logics 2007, LNCS 4732, 383-399, 2007; pdf
Cezary Kaliszyk, Florian Rabe, "A Survey of Languages for Formalizing Mathematics". arXiv:2005.12876, 19 pages
I mention these papers as worth reading, for a couple reasons: first, they discuss an example of what a "higher level of abstraction" actually looks like; second, Kaliszyk and Rabe's paper complements Avigad's paper quite well.
2. Definition. Recall that type theory works by making typing judgements part of the metalanguage. A Soft Type System introduces typing judgements as propositions (and types as predicates) in the object language.
2.1. Example. For a concrete example of soft types in predicate logic, a dependent type with $n$ parameters is represented as an $n+1$-ary predicate $T(x, c_{1}, \dots, c_{n})$ interpreted as $x : T~c_{1}\dots c_{n}$. Subtyping is interpreted as $\forall x, S(x)\implies T(x)$ to assert $S$ is a subtype of $T$, and so on.
2.2.Remark (Soft Types in Type Theory). This is not limited to "non-type theoretic foundations". For example C-Corn in Coq uses a version of a soft type system, as a means to increase the level of abstraction.
2.3. I bring this up because soft types increase the level of abstraction for formalizing mathematics. It's a non-obvious step, which approximates mathematical practice, and demonstrates the sort of "extensibility" I think the next generation of provers may need. Amazingly enough, it can encode the axiom of choice (see, e.g., slides about the [type] usage in Mizar for encoding choice).
3. Mathematical Language. The only addendum I have to add from my last post is just a reference to Kaliszyk and Rabe's paper. It works in a "dual" manner to Avigad's paper, trying to think about a "pseudocode" for formalizing mathematics by surveying what different provers do.
The only qualm I have with their paper is precisely addressed by Avigad's paper: it's useful to give a lot of "small snippets" when trying to think about designing a language. Working in the abstract is, well, abstract. And hard.
If you wrote a program and compiled it for one architecture, but I worked on a computer with a different architecture, then you couldn't share your program with me: you had to send me your source code, and hopefully I had a compiler for the language you used, then I could compile your program for my computer.
2. Theorem Provers. The situation with theorem provers reminds me of the situation with competing CPU architectures in the '80s and '90s. If you wrote a proof in Lean (or Coq or HOL or...), and I work with Coq (or HOL or anything else), then I can't verify your proof in my system. Worse: I can't even "compile it" to my theorem prover. I would have to rewrite it from scratch.
2.1. Terminology. I'm going to generically refer to proof checkers, interactive theorem provers, and automatic theorem provers under the umbrella term Prover. This is non-standard, but the field is so small that any choice would be non-standard.
3. "Generations" of Provers. For the sake of clarity, I think it's useful to introduce a notion of "Generations of Provers", analogous to generations of programming languages.
"First generation provers" include: Automath, Metamath, possibly Twelf, and others lacking automation (or auto-generation of infrastructure, like inductive types which [when defined] introduce an induction principle). First generation provers require you do this manually.
"Second generation provers" range from LCF to HOL, Coq, and Lean (and, I would argue, Mizar). There is some degree of automation, the proof assistant does some of the heavy lifting for you, but you may be required to explicitly state some proof steps.
And that's where we are today: after about 70 years, we've got two "generations" of provers. (This isn't too bad, considering how few people have worked on theorem provers and proof assistants.) We emphasize that "generation" is used metaphorically for the "level of abstraction" afforded by the prover.
4. Hitting a moving target. Unlike the situation facing CPU architects or programming language designers, we who think about theorem provers are trying to formalize an evolving language (mathematics).
We could berate mathematicians for not using theorem provers. But then we have our "tower of Babel" problem, where your prover can't talk to mine. (Fanatics Evangelists resolve this problem by insisting on using their "one true Prover", but that's unrealistic and unmerited.)
A better alternative would be to try to come up with the "next generation" of provers. This is easy to say, hard to accomplish. And mathematicians would just say, "Well, can't we make it like LaTeX with custom macros for proving results?" Again: easier said than done.
Designing a language is very hard, even with simple requirements. But a step towards the next generation would be (I believe Freek Wiedijk pointed this out in some article) analogous to how compilers "eat in" a high level language, process it, and then "spit out" assembly. What's the "assembly language" of mathematics? Some first generation prover, like Metamath or Automath.
5. Designing a mathematical language. The way we have learned to design a programming language (from many years of trial and error): write many small programs in the proposed language, and in comments specify the intended outcome. This strategy applies to provers, as well: write down many examples of mathematics [definitions, theorems, proofs or proof sketches] in the hypothetical prover's vernacular, and comment on what it should be doing.
There is much freedom when designing a new prover's vernacular, and it's easy to "cheat". Simply say, "...and somehow the prover will magically do the following: ...".
Perhaps we can turn this on its head, and begin thinking about how to do mathematics as a controlled natural language? This is how I stumbled into theorem proving, running across Freek Wiedijk's note "The Mathematical Vernacular".
6. Semiformal mathematics: controlling the vernacular.
I just started jotting these ideas down when I came across Jeremy Avigad's interesting recent paper, "The design of mathematical language". Although I agree with much of the paper, and I especially praise the use of "many small examples from mathematical literature" to guide the discussion, I thought it was limited in exploring the "design space" and eager to accept Lean's design decisions.
For example, consider the definition of a "normal subgroup". Are we defining an adjective ("normal") or a type modifier (since "subgroup" is a type, a "normal subgroup" would be a subtype of "subgroup") or a new type with implicit coercions (any "normal subgroup" is automatically a "subgroup", and satisfy the properties that a subgroup would have)?
Another undiscussed dimension to mathematical definitions (as a domain specific language) would be examining the "stuff, structure, and properties" idea of Baez and Dolan. This template gives us a lot "for free", and can be made somewhat "independent of foundations" by using objects in toposes. It's a small thing, but seldom discussed among provers.
The discussion also lacked adequate examples from applied mathematics (which, for me, would be things like weak solutions to PDEs, or theorems about regularity of PDEs, or something like that...my mind is focused on the Navier-Stokes equations). Granted, this is a domain where many mathematicians flinch and say, "Ouch, this is an unpleasant field." I do not intend it as a criticism, but an observation.
6.1. Analysis, Synthesis. The next natural step in Avigad's paper would be to move from analyzing examples to synthesizing some semi-formal "vernacular".
I honestly don't have a "semi-formal vernacular" at hand to present, but I have been using something similar to Wiedijk's vernacular for the past year. Since April or so of 2021, I have been transcribing my notes into a Zettelkasten (i.e., onto A6 size slips of paper). Proofs and proof sketches have been written using a slight variant of Wiedijk's vernacular.
It works fine for proofs, and forces me to fill in missing steps (or at least, make note of them). But I think proofs as a domain-specific language don't require much thought: we've had very smart people think about it for a century, and they came up with pretty good ideas (natural deduction, judgements, etc.). Now my task boils down to coming up with the right "reserved keywords" corresponding to the proof steps found in mathematical logic.
For definitions, in Field theory and Galois theory, most definitions don't neatly fit the "stuff, structure, properties" mould. This is great! Now I have some ready-to-present examples where it fails, namely whenever a definition looks like: "We call a gadget $G$ Hairy if [hairy property] holds." This occurs a lot in field theory and Galois theory. It also forces me to think deeply about what "species" of definition this is, and what's "really being defined" here.
6.2. Future of Provers? The short answer is, I don't know. The next steps may be to think about the "next generation" of provers, and try to move towards a "foundation independent framework" which resembles how working mathematicians actually operate.
But I think it's wrong-headed to say, as Leslie Lamport put it, mathematicians are "doing proofs wrong" because it resembles Euclid (and Euclid is old, thus bad). It's probably equally as misguided as suggesting that the design of the input language for provers is irrelevant, as any compiler designer will tell you, since this alienates the user-base and hinders adoptation.
Taken together, this suggests we need to make provers resemble "ordinary mathematics" as published and practiced by working mathematicians. Thus investigations along the lines of Avigad's article is well worth pursuing.
My intuition tells me that the third or fourth generation of Provers will resemble compilers, accepting more human intelligible input, producing "assembly code"-like output for a particular foundations of mathematics. Changing foundations would be a "one liner", if that. But what does the input language look like? That's hard to say.
1. There is some "Kabuki theater" whenever introducing a new mathematical gadget, thanks to category theory: we have our new gadget, then we could ask about morphisms (very important), "subgadgets", and universal constructions (products, quotients, etc.). The exciting thing, as in Kabuki theater, is the order and manner of presentation.
2.Definition. Let ${G}$ and ${H}$ be groups. We define a Group Morphism to consist of a function ${\varphi\colon G\to H}$ of the underlying sets such that
group operation is preserved: for any ${g_{1}}$, ${g_{2}\in G}$, we have ${\varphi(g_{1}g_{2})=\varphi(g_{1})\varphi(g_{2})}$;
identity element is preserved: if ${e_{G}\in G}$ is the identity element of ${G}$ and ${e_{H}\in H}$ is the identity element of ${H}$, then ${\varphi(e_{G})=e_{H}}$;
inverse is preserved: for any ${g\in G}$, ${\varphi(g^{-1})=\varphi(g)^{-1}}$.
2.1.Remark. Older texts refer to group morphisms as "group homomorphisms". After category theory became popular and part of the standard curriculum, the "homo-" prefix was dropped because group morphisms live in the same category, so it was redundant.
3.Example. One "low hanging fruit" for morphism examples is the identity morphism. We should check, for any group ${G}$, the identity function ${\mathrm{id}\colon G\to G}$ is a bona fide group morphism.
We see it preserves the group operation. For any ${g_{1}}$, ${g_{2}\in G}$, we have ${\mathrm{id}(g_{1}g_{2})=g_{1}g_{2}}$ by definition of the identity function. But this is also equal to ${\mathrm{id}(g_{1})\mathrm{id}(g_{2})}$. Thus the group operation is preserved.
The identity element is preserved ${\mathrm{id}(e_{G})=e_{G}}$.
Inversion is also preserved ${\mathrm{id}(g^{-1})=g^{-1}=\mathrm{id}(g)^{-1}}$ for any ${g\in G}$.
Thus taken together, it follows the identity mapping satisfies the axioms of a group morphism.
4.Example. Let ${G}$ be any group, and consider ${\mathbb{Z}}$ equipped with addition as a group. For each ${g\in G}$, we have a group morphism ${\varphi\colon\mathbb{Z}\to G}$ sending ${1\in\mathbb{Z}}$ to ${g\in G}$. Is this really a group morphism?
We can check that the properties are (or, ought to be) satisfied. If the group operation is preserved, then ${\varphi(1+1)=\varphi(1)\varphi(1)=g^{2}}$ and more generally, for any ${m\in\mathbb{Z}}$, we have ${\varphi(m+1)=\varphi(1)^{m}=g^{m}}$.
For the identity element being preserved, that means ${\varphi(0)=e_{G}}$, which is fine: it corresponds to ${g^{0}=e_{G}}$.
Group inverses would be ${\varphi(-m)=\varphi(m)^{-1}=(g^{m})^{-1}}$. And we know this is precisely the same as ${g^{-m}}$.
5.Example. Consider the group ${\mathrm{GL}(2,\mathbb{R})}$ and the multiplicative group ${\mathbb{R}^{\times}}$ of nonzero real numbers. Then the determinant
$$ \det\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}^{\times} \tag{1}$$
is a group morphism. Let us prove it!
We see, for any matrices ${M}$, ${N\in\mathrm{GL}(2,\mathbb{R})}$ we have
$$ \det(MN)=\det(M)\det(N). \tag{2}$$
This is a familiar fact in linear algebra. But for us, it tells us the group operation is preserved.
The identity element must be mapped to the identity element. We see the identity matrix ${I\in\mathrm{GL}(2,\mathbb{R})}$ has ${\det(I)=1}$. Thus the determinant preserves the group identity element.
As far as the group inverse, well, this follows from previous results, right? After all, if ${M\in\mathrm{GL}(2,\mathbb{R})}$, then ${M^{-1}\in\mathrm{GL}(2,\mathbb{R})}$, and
$$ I = M^{-1}M \tag{3}$$
so
$$ \det(M^{-1}M)=\det(M^{-1})\det(M)=1 \tag{4}$$
and thus by division
$$ \det(M^{-1})=\det(M)^{-1}. \tag{5}$$
Thus the group inverse operator is preserved.
6.Definition. Let ${\varphi\colon G\to H}$ be a group morphism. We define the Kernel of ${\varphi}$ to be the pre-image of the identity element of ${H}$: \begin{equation*} \ker(\varphi)=\{g\in G|\varphi(g)=e_{H}\}. \end{equation*}
7.Example. For the group morphism ${\det\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}^{\times}}$, the kernel would be
$$ \ker(\det)=\{M\in\mathrm{GL}(2,\mathbb{R})|\det(M)=1\}. \tag{6}$$
That is to say, it consists of matrices with unit determinant. Observe, this is a group under matrix multiplication: if two matrices have unit determinant, their product has unit determinant; the identity matrix is in the kernel; and it's closed under inverses. This is an important group called the Special Linear Group, denoted ${\mathrm{SL}(2,\mathbb{R})}$.
1. Properties of Morphisms
8.Proposition. Let ${\varphi\colon G\to H}$ be a group morphism. If ${g\in G}$ is any element, then ${\varphi(g^{-1})=\varphi(g)^{-1}}$.
Proof: Let ${g\in G}$ (so ${\varphi(g)\in H}$). We find ${\varphi(g\cdot g^{-1})=\varphi(g)\varphi(g^{-1})=e_{H}}$, thus multiplying on the left by ${\varphi(g)^{-1}}$ gives the result. ∎
9.Proposition. Let ${\varphi\colon G\to H}$ be a group morphism. If ${g\in G}$ is any element and ${n\in\mathbb{Z}}$ is any integer, then ${\varphi(g^{n})=\varphi(g)^{n}}$.
Proof: Per cases since ${n<0}$ or ${n=0}$ or ${n>0}$. The ${n=0}$ case is obvious.
For ${n>0}$, by induction. The base case ${n=1}$ gives ${\varphi(g^{1})=\varphi(g)^{1}}$, which is obvious. Assume this holds for arbitrary ${n}$. Then the inductive case ${n+1}$ is
$$ \varphi(g^{n+1})=\varphi(g^{n}g)=\varphi(g)^{n}\varphi(g)=\varphi(g)^{n+1}. \tag{7}$$
Thus we have proven the result for non-negative ${n}$.
For negative ${n\in\mathbb{Z}}$, the proof is analogous. ∎
10.Theorem. The composition of group morphisms is a group morphism. More explicitly, if ${\varphi\colon G\to H}$ and ${\psi\colon H\to K}$ are group morphisms, then ${\psi\circ\varphi\colon G\to K}$ is a group morphism.
11.Theorem. Let ${\varphi\colon G\to H}$ be a group morphism. If ${\ker(\varphi)=\{e_{G}\}}$, then ${\varphi}$ is injective.
Proof: Assume ${\ker(\varphi)=\{e_{G}\}}$. Let ${g_{1}}$, ${g_{2}\in G}$ be completely arbitrary. (We want to show if ${\varphi(g_{1})=\varphi(g_{2})}$, then ${g_{1}=g_{2}}$.) Assume ${\varphi(g_{1})=\varphi(g_{2})}$. Then ${\varphi(g_{1})\varphi(g_{2})^{-1}=e_{H}}$ by multiplying both sides on the right by ${\varphi(g_{2})^{-1}}$. And ${\varphi(g_{1})\varphi(g_{2}^{-1})=\varphi(g_{1}\cdot g_{2}^{-1})=e_{H}}$. Thus ${g_{1}\cdot g_{2}^{-1}\in\ker(\varphi)}$ by definition of the kernel. But we assumed the only member of the kernel was identity element. Thus ${g_{1}\cdot g_{2}^{-1}=e_{G}}$, and moreover ${g_{1}=g_{2}}$. Hence ${\varphi}$ is injective. ∎
2. Exercises
Exercise1. Let ${G}$ be a group, ${n\in\mathbb{N}}$ be a fixed positive integer. Prove or find a counter-example: ${\varphi\colon G\to G}$, sending ${g}$ to ${\varphi(g)=g^{n}}$ is a group morphism.
Exercise2. Prove or find a counter-example: the matrix trace ${\mathop{\rm tr}\nolimits\colon\mathrm{GL}(2,\mathbb{R})\to\mathbb{R}}$ is a group morphism.
Exercise3. Is the exponential function on the real numbers a group morphism ${\exp\colon\mathbb{R}\to\mathbb{R}^{\times}}$?
Exercise4. Is the matrix exponential a group morphism ${\exp\colon\mathrm{Mat}_{2}(\mathbb{R})\to\mathrm{GL}(2,\mathbb{R})}$? [Hint: $\mathrm{Mat}_{2}(\mathbb{R})$ has its group operation be matrix addition. Is this preserved?]
This is a note for myself as I review my notes on finite groups, Lie groups (both the classic infinite ones and the finite simple groups of Lie type), Lie algebras, and specifically the typography for them.
First, no one agrees completely, and everyone's conventions is slightly different. What I mean by this: although everyone agrees, e.g., that the An family of Lie algebras refers to the same thing, some people use serif font for the "A", others use bold, some italicize, others do not, etc. Each field uses its own notation with good reason, but I think we can standardize notation a bit better in group theory.
I'm inclined to follow Robert Wilson's conventions from his book The Finite Simple Groups (2009).
Families of Groups
Families of Simple Lie groups: use upright, teletype font for the family and "math italics" for the subscript if it's a variable, e.g., $\mathtt{A}_{n}$, $\mathtt{B}_{5}$, $\mathtt{C}_{m}$, $\mathtt{D}_{n^{2}}$, $\mathtt{E}_{8}$
Exceptional Finite Simple Groups of Lie Type: don't treat the formatting as special, so, e.g., the Steinberg groups would be ${}^{2}A_{n}(q^{2})$, ${}^{2}D_{n}(q^{2})$, ${}^{2}E_{6}(q^{2})$, ${}^{3}D_{4}(q^{3})$.
Sporadic simple group: these should be made upright, e.g., the Suzuki group is $\mathrm{Suz}$, the Matthieu groups look like $\mathrm{M}_{11}$, the Conway groups $\mathrm{Co}_{1}$ and $\mathrm{Co}_{2}$, and so on. BUT the exception to this rule is that the Monster group is written $\mathbb{M}$ and the Baby Monster $\mathbb{B}$.
Alternating, Cyclic, Symmetric group. These are just written as $A_{n}$, $C_{n}$, or $S_{n}$. The dihedral group, too, is $D_{n}$.
Classical Lie Groups: Here there is a double standard. For classical Lie groups over the reals or complex numbers, we write something of the form $\mathrm{GL}(n, \mathbb{F})$, $\mathrm{SL}(n, \mathbb{F})$, $\mathrm{U}(n, \mathbb{F})$, $\mathrm{SU}(n, \mathbb{F})$, $\mathrm{O}(n, \mathbb{F})$, $\mathrm{SO}(n, \mathbb{F})$, $\mathrm{Sp}(n)=\mathrm{USp}(n)$ for the compact Symplectic group, $\mathrm{Sp}(2n,\mathbb{F})$ for the generic Symplectic group.
The finite groups corresponding to these guys are written a little differently in my notes: the $n$ parameter is pulled out as a subscript, because frequently we write $q$ instead of $\mathbb{F}_{q}$ for finite fields...and then looking at $\mathrm{SL}(8,9)$ is far more confusing than $\mathrm{SL}_{8}(9)$. Thus we have $\mathrm{GL}_{n}(q)$, and so on.
Projective classical groups: the projective classical groups are prefixed by a "P", not a blackboard bold $\mathbb{P}$. E.g., $\mathrm{PSL}_{2}(7)$. At present, the projective orthogonal group wikipedia page seems to agree with this convention.
Operations
For finite groups: the Atlas of finite groups seems to have set the standard conventions for finite groups, Wilson changes them slightly. We'll find $G = N{:}H$ for the semidirect product $G = N \rtimes H = H\ltimes N$. Also $A\mathop{{}^{\textstyle .}}\nolimits B = A{\,}^{\textstyle .} B$ for a non-split extension with quotient $B$ and normal subgroup $A$, but no subgroup $B$. And $A{.}B$ is an unspecified extension.
Lie algebras. Writing notes on paper, for a given Lie group $G$, I write $\mathrm{Lie}(G)$ as its Lie algebra. (It turns out to be a functor...neat!) If I have to write Fraktur by hand, I approximate it using Pappus's caligraphy tutorial.
We will introduce the machinery necessary for defining a smooth manifold.
1.1. Charts
1.Definition. Let ${X\subset M}$ be some set. An ${n}$-dimensional Chart consists of
an open subset ${U\subset\mathbb{R}^{n}}$
a map ${\varphi\colon U\to X}$
such that ${\varphi}$ is an appropriate isomorphism (for topological manifolds, it is a homeomorphism; smooth manifolds require a diffeomorphism; and so on).
2.Remark. We call ${\varphi\colon U\to X}$ a Parametrization of ${X}$, and ${\varphi^{-1}\colon X\to U}$ a Local System of Coordinates.
3.Remark. Since ${\varphi}$ is an isomorphism, the literature mixes up using ${U\to X}$ and ${X\to U}$. Milner uses ${\varphi\colon U\to X}$, but John Lee uses the opposite convention.
4.Definition. Let ${(U,\varphi)}$, ${(V,\psi)}$ be two charts. We say they are Compatible if
the set ${(\varphi^{-1}\circ\psi)(V)\subset U}$ is an open set;
the set ${(\psi^{-1}\circ\varphi)(U)\subset V}$ is an open set;
the map ${\psi^{-1}\circ\varphi\colon\varphi^{-1}(\psi(V))\to\psi^{-1}(\varphi(U))}$ is smooth; and
the map ${\varphi^{-1}\circ\psi\colon\psi^{-1}(\varphi(U))\to\varphi^{-1}(\psi(V))}$ is smooth.
In particular, the charts are compatible if ${\varphi(U)\cap\psi(V)=\emptyset}$ is disjoint.
5.Remark. We refer to the maps ${\psi^{-1}\circ\varphi}$ as Transition Functions. The condition of smooth is ${C^{\infty}(\mathbb{R}^{n})}$, but different manifolds have different conditions (we could have ${C^{k}}$ charts, or ${C^{0}}$ charts, or analytic ${C^{\omega}}$ charts, or...).
In the older literature (e.g., Kobayashi and Nomizu's Foundations of Differential Geometry), the collection of transition functions form a gadget called a Pseudogroup.
6.Remark. We abuse notation, and could be more explicit by writing
$$ \psi^{-1}\circ\varphi\colon\varphi^{-1}(\varphi(U)\cap\psi(V))\to\psi^{-1}(\varphi(U)\cap\psi(V)) \tag{1}$$
▸ Exercise1. Prove chart compatibility is an equivalence relation.
1.2. Atlases
7.Definition. Let ${M}$ be a set. An (${n}$-dimensional) Atlas consists of a collection ${\{(U_{\alpha},\varphi_{\alpha})\mid\alpha\in A\}}$ of ${n}$-dimensional charts on ${M}$ such that
Pairwise compatible: for any ${\alpha}$, ${\beta\in A}$ the charts ${(U_{\alpha},\varphi_{\alpha})}$ and ${(U_{\beta},\varphi_{\beta})}$ are compatible.
8.Definition. Two ${n}$-dimensional atlases on ${M}$, ${\mathcal{A}}$ and ${\mathcal{B}}$, are called Equivalent if their union ${\mathcal{A}\cup\mathcal{B}}$ is also an atlas. That is to say, if any chart of ${\mathcal{A}}$ is compatible with any chart of ${\mathcal{B}}$.
9.Remark. Remember: charts are compatible, but atlases are equivalent.
10.Lemma. Let ${\mathcal{B}}$ be an atlas, let ${(U,\varphi)}$ and ${(V,\psi)}$ be two charts not contained in ${\mathcal{B}}$. If ${(U,\varphi)}$ is compatible with every chart of ${\mathcal{B}}$, and if ${(V,\psi)}$ is compatible with every chart of ${\mathcal{B}}$, then ${(U,\varphi)}$ is compatible with ${(V,\psi)}$.
11.Theorem. Equivalence of atlases is an equivalence relation.
Proof: Let ${\mathcal{A}}$, ${\mathcal{B}}$, ${\mathcal{C}}$ be arbitrary atlases on ${M}$.
Reflexivity: ${\mathcal{A}}$ is equivalent to itself, since by definition any pair of charts in ${\mathcal{A}}$ are compatible.
Symmetry: let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent atlases, then ${\mathcal{B}}$ and ${\mathcal{A}}$ are equivalent atlases.
Transitivity: this is the nontrivial part. Let ${\mathcal{A}}$ and ${\mathcal{B}}$ be equivalent atlases, and ${\mathcal{B}}$ be equivalent to ${\mathcal{C}}$. Then transitivity follows by considering arbitrary charts ${(U,\varphi)\in\mathcal{A}}$ and ${(V,\psi)\in\mathcal{C}}$, then applying Lemma 10.
Thus "equivalence of atlases" forms an equivalence relation. ∎
12.Proposition. The collection of atlases on a given set ${M}$ is a set, not a proper class.
Proof: The class of atlases is a subcollection of
$$ \mathcal{X}=\mathcal{P}\left(\bigcup_{U\in\mathcal{P}(\mathbb{R}^{n})}\mathop{\rm Hom}\nolimits(U,M)\right) \tag{2}$$
where ${\mathop{\rm Hom}\nolimits(U,\mathbb{R}^{n})}$ is the collection of (appropriately smooth, or continuous, or holomorphic, or...) functions from ${U}$ to ${M}$. By ZF axioms, ${\mathcal{X}}$ is a set. ∎
1.3. Manifolds
13.Definition. Let ${M}$ be a set, let ${\mathcal{A}}$ be an ${n}$-dimensional atlas on ${M}$. We call a subset ${B\subset M}$ Open (with respect to ${\mathcal{A}}$) if for any chart ${(U,\varphi)\in\mathcal{A}}$ the preimage ${\varphi^{-1}(B)}$ is open (in ${U}$, and thus open in ${\mathbb{R}^{n}}$). In particular, the images ${\varphi(U)}$ are open.
14.Theorem. If two atlases ${\mathcal{A}_{1}}$ and ${\mathcal{A}_{2}}$ on ${M}$ are equivalent, then a subset ${B\subset M}$ is open with respect to ${\mathcal{A}_{1}}$ if and only it is open with respect ${\mathcal{A}_{2}}$.
15.Remark. This theorem shows an equivalence class of atlases on ${M}$ makes ${M}$ a topological space. We may therefore meaningfully speak about topological properties of ${M}$ (like compactness, connectedness, and so forth).
16.Corollary. Let ${\mathcal{A}}$ be an ${n}$-dimensional atlas for ${M}$. Then the collection of open sets with respect to ${\mathcal{A}}$ form a topology on ${M}$.
17.Definition. Let ${M}$ be a fixed set. A ${n}$-Dimensional Differential Structure (or ${n}$-Dimensional Smooth Structure) on ${M}$ consists of an equivalence class ${\mathfrak{D}}$ of ${n}$-dimensional atlases on ${M}$ such that
Second-Countable: ${\mathfrak{D}}$ contains an at most countable atlas;
Hausdorff: for any distinct ${p,q\in M}$, there exists disjoint open neighborhoods ${U,V\subset M}$ such that ${p\in U}$ and ${q\in V}$.
18.Remark (Smooth Structure using a Maximal Atlas). Equivalence classes are awkward to work with, and so it is more popular to consider maximal atlases. An atlas ${\mathcal{A}}$ is maximal if it contains all charts compatible with every chart in ${\mathcal{A}}$. Given an equivalence class ${\mathfrak{A}}$ of atlases, we may obtain a maximal atlas by considering
$$ \mathcal{A}_{\text{max}} = \bigcup_{\mathcal{A}\in\mathfrak{A}}\mathcal{A}. \tag{3}$$
This may be used instead of an equivalence class of atlases in defining a differential structure, provided the second-countable axiom is reworded as: ${\mathcal{A}_{\text{max}}}$ contains an at most countable subatlas.
19.Remark (Convenient Fiction). No one actually constructs either a maximal atlas or a differential structure. We typically construct a smooth atlas on ${M}$, then announce we are working with the differential structure containing our atlas. Thus maximal atlases and, to some degree, differential structures are a convenient fiction.
20.Definition. A (Smooth) ${n}$-Dimensional Manifold consists of a set ${M}$ equipped with an ${n}$-dimensional differential structure.
21.Puzzle. Is this definition correct? By this, I mean: is an "${n}$-Dimensional Differential Structure" actually structure (in the sense of "stuff, structure, and properties")?
