From a7b761c015f0b639377f17138d1c281c3ad11575 Mon Sep 17 00:00:00 2001 From: amackay Date: Sun, 16 Aug 2020 13:00:39 +0930 Subject: [PATCH 1/3] Fix many minor issues, mostly grammatical --- metamath.tex | 75 +++++++++++++++++++++++++--------------------------- 1 file changed, 36 insertions(+), 39 deletions(-) diff --git a/metamath.tex b/metamath.tex index 375d7da..050975f 100644 --- a/metamath.tex +++ b/metamath.tex @@ -1034,7 +1034,7 @@ \subsubsection{Overview} Metamath provides you with the ability to immediately follow and dissect proofs even in totally unfamiliar areas. -Of course, just being able follow a proof will not necessarily give you an +Of course, just being able to follow a proof will not necessarily give you an intuitive familiarity with mathematics. Memorizing the rules of chess does not give you the ability to appreciate the game of a master, and knowing how the notes on a musical score map to piano keys does not give you the ability to @@ -1267,7 +1267,7 @@ \subsubsection{A Personal Note} \subsubsection{Note on Bibliography and Index} The Bibliography usually includes the Library of Congress classification -for a work to make it easier for you to find it in on a university +for a work to make it easier for you to find it on a university library shelf. The Index has author references to pages where their works are cited, even though the authors' names may not appear on those pages. @@ -1394,7 +1394,7 @@ \subsubsection{Note Added February 25, 2019}\label{note201902} \subsubsection{Note Added March 7, 2019}\label{note201903} -This added a description of the Matamath language syntax in +This added a description of the Metamath language syntax in Extended Backus--Naur Form (EBNF)\index{Extended Backus--Naur Form}\index{EBNF} in Appendix \ref{BNF}, added a brief explanation about typecodes, inserted more examples in the deduction section, @@ -1622,7 +1622,7 @@ \subsection{Is Mathematics ``User-Friendly''?} but you can write a passable program when necessary to suit your needs. Even more important, you know that you can look at anyone else's Pascal program, no matter how complex, and with enough patience figure out exactly how it works, -even though you are not a specialist. Pascal allows you do anything that a +even though you are not a specialist. Pascal allows you to do anything that a computer can do, at least in principle. Thus you know you have the ability, in principle, to follow anything that a computer program can do: you just have to break it down into small enough pieces. @@ -2442,7 +2442,7 @@ \subsection{Rigor} Metamath has no hard-wired knowledge of what constitutes a wff built into it; instead every wff must be explicitly constructed based on rules defining wffs that are present in a database. Thus a single step in an ordinary formal -proof may be correspond to many steps in a Metamath proof. Despite the larger +proof may correspond to many steps in a Metamath proof. Despite the larger number of steps, though, this does not mean that a Metamath proof must be significantly larger than an ordinary formal proof. The reason is that since we have constructed the wff from scratch, we know what the wff is, so there is @@ -2797,7 +2797,7 @@ \subsection{Automated Theorem Provers}\label{theoremprovers} consider investigating the book {\em Automated Reasoning: Introduction and Applications} \cite{Wos}\index{Wos, Larry}. This book discusses -how to use {\sc otter} in a way that can +how to use {\sc otter} in a way that is not only able to generate relatively efficient proofs, it can even be instructed to search for shorter proofs. The effective use of {\sc otter} (and similar tools) @@ -2870,7 +2870,7 @@ \subsection{Proof Verifiers}\label{proofverifiers} time rather than making a large, organized database easily available to the user. Metamath is one way to help close this gap. -By itself Metamath is a mostly a proof verifier. +By itself Metamath is mostly a proof verifier. This does not mean that other approaches can't be used; the difference is that in Metamath, the results of various provers must be recorded step-by-step so that they can be verified. @@ -3216,7 +3216,7 @@ \subsection{A History of the Approach Behind Metamath} condensed detachment is more or less limited to propositional calculus\index{propositional calculus}. The concept has been extended to first-order logic\index{first-order logic} in \cite{Megill}\index{Megill, -Norman}, making it is easy to write a small computer program to verify proofs +Norman}, making it easy to write a small computer program to verify proofs of simple first-order logic theorems.\index{condensed detachment!and first-order logic} @@ -4020,7 +4020,7 @@ \section{A Trial Run}\label{trialrun} (at one time you had to add the \texttt{/essential} qualifier in the \texttt{show proof} command to get this view, but this is now the default). -You can could use the \texttt{/all} qualifier in the \texttt{show +You could use the \texttt{/all} qualifier in the \texttt{show proof} command to also show the explicit construction of expressions. The \texttt{/renumber} qualifier means to renumber the steps to correspond only to what is displayed.\index{\texttt{show proof} @@ -4268,7 +4268,7 @@ \section{Your First Proof}\label{frstprf} We are now going to describe an obscure feature that you will probably never use but should be aware of. The Metamath language allows empty symbol sequences to be substituted for variables, but in most formal -systems this feature is never used. One of the few examples where is it +systems this feature is never used. One of the few examples where it is used is the MIU-system\index{MIU-system} described in Appendix~\ref{MIU}. But such systems are rare, and by default this feature is turned off in the Proof Assistant. (It is always allowed for @@ -4567,7 +4567,7 @@ \section{Logic and Set Theory}\label{logicandsettheory} tries to summarize what mathematicians think about when they work with the axioms. -Logic is a set of rules that allow us determine truths given other truths. +Logic is a set of rules that allow us to determine truths given other truths. Put another way, logic is more or less the translation of what we would consider common sense into a rigorous set of axioms.\index{axioms of logic} Suppose $\varphi$, @@ -4585,7 +4585,7 @@ \section{Logic and Set Theory}\label{logicandsettheory} extends propositional calculus by also allowing us to discuss statements about objects (not just true and false values), including statements about ``all'' or ``at least one'' object. -For example, predicate calculus allows to say, +For example, predicate calculus allows us to say, ``if $\varphi$ is true for all $x$, then $\varphi$ is true for some $x$.'' The logic used in \texttt{set.mm} is standard classical logic (as opposed to other logic systems like intuitionistic logic). @@ -5011,7 +5011,7 @@ \subsubsection{Metamath representation} The Metamath axiom system for predicate calculus extends Tarski's system to eliminate this difficulty. The additional -``auxilliary'' axiom +``auxiliary'' axiom schemes (as we will call them in this section; see below) endow Tarski's system with a nice property we call metalogical completeness \cite[Remark 9.6]{Megill}\index{Megill, Norman}. @@ -5200,7 +5200,7 @@ \subsection{Other Axioms} Again, we only use this axiom when we need to. You are only likely to encounter or use this axiom if you are doing category theory, since its use is highly specialized, -so we will not list the Tarsky-Grothendieck axiom +so we will not list the Tarski-Grothendieck axiom in the short list of axioms below. Can there be even more axioms? @@ -6439,7 +6439,7 @@ \subsection{Definitions for Set Theory}\label{setdefinitions} \noindent Define the ordinal predicate\index{ordinal predicate}, which is true for a class that is transitive and is well-ordered by the epsilon relation. Similar to -definition on p.~468, Bell and Machover. +the definition on p.~468, Bell and Machover. \vskip 0.5ex \setbox\startprefix=\hbox{\tt \ \ df-ord\ \$a\ } @@ -7949,7 +7949,7 @@ \subsection{Deduction Style}\label{deductionstyle} We now prefer to write assertions in ``deduction form'' instead of writing a proof that would require use of the standard or weak deduction theorem. -We call this appraoch +We call this approach ``deduction style.''\index{deduction style} It will be easier to explain this by first defining some terms: @@ -8724,7 +8724,7 @@ \subsection{A Note on the ``Compact'' Proof Format} The Metamath program will display proofs in a ``compact''\index{compact proof} format whenever the proof is stored in compressed format in the database. It -may be be slightly confusing unless you know how to interpret it. +may be slightly confusing unless you know how to interpret it. For example, if you display the complete proof of theorem \texttt{id1} it will start off as follows: @@ -8979,7 +8979,7 @@ \subsection{Basic Syntax} The type declared by a \texttt{\$f} statement for a given label is global even if the variable is not (e.g., a database may not have \texttt{wff P} in one local scope -nd \texttt{class P} in another). +and \texttt{class P} in another). A {\bf simple \$d statement}\index{\texttt{\$d} statement!simple} consists of \texttt{\$d}, followed by two different active variables, @@ -9931,7 +9931,7 @@ \subsection{The \texttt{\$f} after quantifiers like for-all ($\forall$) and there-exists ($\exists$). \item \texttt{class} : An expression that is a syntactically valid class expression. - All valid set expressions are also valid class expression, so expressions + All valid set expressions are also valid class expressions, so expressions of sets normally have the \texttt{class} typecode. Use the \texttt{class} typecode, \textit{not} the \texttt{setvar} typecode, @@ -10841,9 +10841,9 @@ \section{The Anatomy of a Proof} \label{proof} Therefore, by default the \texttt{show proof}\index{\texttt{show proof} command} command does not show the syntax construction. -Historically \texttt{show proof} command +Historically the \texttt{show proof} command \textit{did} show the syntax construction, and you needed to add the -\texttt{/essential} option to hide, them, but today +\texttt{/essential} option to hide them, but today \texttt{/essential} is the default and you need to use \texttt{/all} to see the syntax constructions. @@ -10882,8 +10882,8 @@ \subsection{The Concept of Unification} \label{unify} Mandatory hypotheses must be pushed on the proof stack in the order in which they appear. In addition, each variable must have its type specified -with a \texttt{\$f} hypothesis before it is used -and that each \texttt{\$f} hypothesis +with a \texttt{\$f} hypothesis before it is used, +and each \texttt{\$f} hypothesis must have the restricted syntax of a typecode (a constant) followed by a variable. The typecode in the \texttt{\$f} hypothesis must match the first symbol of the corresponding RPN stack entry (which will also be a constant), so @@ -11115,7 +11115,7 @@ \subsubsection{Link to bibliographical reference}\index{citation}% \subsubsection{Parentheticals}\label{parentheticals} -The end of a comment may include one or more parenthicals, that is, +The end of a comment may include one or more parentheticals, that is, statements enclosed in parentheses. The Metamath program looks for certain parentheticals and can issue warnings based on them. @@ -11344,7 +11344,7 @@ \subsubsection{Typesetting Comment - \LaTeX} the token and the \LaTeX\ definition of the token, respectively, These \LaTeX\ definitions are used by the Metamath program -when it is asked to product \LaTeX output using +when it is asked to produce \LaTeX output using the \texttt{write tex} command. \subsubsection{Typesetting Comment - {\sc html}} @@ -11364,7 +11364,7 @@ \subsubsection{Typesetting Comment - {\sc html}} Note that in {\sc HTML} there are two possible definitions for math tokens. This feature is useful when an alternate representation of symbols is desired, for example one that -uses Unicode entities and another uses {\sc gif} images. +uses Unicode entities and another that uses {\sc gif} images. There are many other typesetting definitions that can control {\sc HTML}. These include: @@ -11393,7 +11393,7 @@ \subsubsection{Typesetting Comment - {\sc html}} code for a link back to the home page. The \texttt{htmlvarcolor} is code for a color key that appears at the bottom of each proof. The file specified by {\em filename} is an {\sc html} file that is assumed to -have a \texttt{} tag for each bibiographic +have a \texttt{} tag for each bibliographic reference in the database comments. For example, if \texttt{[Monk]}\index{\texttt{\char`\[}\ldots\texttt{]} inside comments} occurs in the comment for a theorem, then \texttt{} must @@ -12031,7 +12031,7 @@ \subsection{Adding Constraints on Definitions} Second, we run a definition soundness check specific to \texttt{set.mm} or databases similar to it. (through the \texttt{definitionCheck} macro). -Some \texttt{\$a} statements (including all ax-* statemnets) +Some \texttt{\$a} statements (including all ax-* statements) are excluded from these checks, as they will always fail this simple check, but they are appropriate for most definitions. @@ -12047,7 +12047,7 @@ \subsection{Adding Constraints on Definitions} \item Every variable in the definiens should not be distinct -\item Every dummy variable in the definiendum +\item All dummy variables in the definiendum are required to be distinct from each other and from variables in the definiendum. To determine this, the system will look for a "justification" theorem @@ -12070,7 +12070,7 @@ \subsection{Summary of Approach to Definitions} metatheorems to establish that they are not creative. Instead of building such complications into the Metamath language itself, -the basic Metmath language and program simply treat traditional +the basic Metamath language and program simply treat traditional axioms and definitions as the same kind of \texttt{\$a} statement. We have then built various tools to enable people to verify additional conditions as their creators believe is appropriate @@ -12328,7 +12328,7 @@ \subsection{\texttt{set height} Command}\index{\texttt{set Syntax: \texttt{set height} {\em number} Metamath assumes your screen height is 24 lines of characters. If your -screen is taller or shorter, this command lets you to change the number +screen is taller or shorter, this command lets you change the number of lines at which the display pauses and prompts you to continue. \subsection{\texttt{beep} Command}\index{\texttt{beep} command} @@ -12843,7 +12843,7 @@ \section{Creating Proofs}\label{pfcommands}\index{Proof Assistant} not everyone finds that effective. {\em Important:} -The \texttt{undo} command if very helpful when entering a proof, because +The \texttt{undo} command is very helpful when entering a proof, because it allows you to undo a previously-entered step. In addition, we suggest that you keep track of your work with a log file (\texttt{open @@ -13036,10 +13036,7 @@ \subsection{\texttt{set empty\_substitution} Command}\index{\texttt{set example.) Note that empty substitutions are always permissible in proof verification (VERIFY PROOF...) outside the -Proof Assistant. (See the MIU system in the Metamath book for an example -of a system needing empty substitutions; another example would be a -system that implements a Deduction Rule and in which deductions from -empty assumption lists would be permissible.) +Proof Assistant. It is better to leave this \texttt{off} when working with \texttt{set.mm}. Note that this command does not affect the way proofs are verified with @@ -13271,7 +13268,7 @@ \subsection{\texttt{delete} Command}\index{\texttt{delete} command} An alternative is to salvage your last \texttt{save new{\char`\_}proof} by exiting and reentering the Proof Assistant. For this to work, keep a log file open to record your work -and to do \texttt{save new{\char`\_}proof} frequently, especially before +and do \texttt{save new{\char`\_}proof} frequently, especially before \texttt{delete}. \texttt{delete floating{\char`\_}hypotheses} will delete all sections of @@ -13836,7 +13833,7 @@ \chapter{Sample Representations} \hyperref[df-eu]{\texttt{df-eu}} & There exists exactly one; $\exists ! x \varphi$ is true iff - there is at least one $x$ where $\varphi$ is true. \\ + there is exactly one $x$ where $\varphi$ is true. \\ \texttt{\{ y | phi \}} & $ \{ y | \varphi \}$ & \hyperref[df-clab]{\texttt{df-clab}} & The class of all sets where $\varphi$ is true. \\ @@ -14352,7 +14349,7 @@ \subsection{Statements} means that each variable occurring in a statement's logical hypotheses or assertion must have an associated variable-type hypothesis or ``type declaration,'' in analogy to a computer programming language, where a -variable must be declared to be say, a string or an integer. The requirement +variable must be declared to be, say, a string or an integer. The requirement that $\forall e,f\in T \, e_1 \ne f_1$ for $e\neq f$ means that each variable must be associated with a unique constant designating its variable type; e.g., a From 7cae10ca9b0109886d7eba82fdfc162f930e20fa Mon Sep 17 00:00:00 2001 From: amackay Date: Sun, 16 Aug 2020 13:01:39 +0930 Subject: [PATCH 2/3] Errata.md: Duplicate output on page 103 --- errata.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/errata.md b/errata.md index 34fa2a3..bc1c3d6 100644 --- a/errata.md +++ b/errata.md @@ -16,6 +16,9 @@ dated 2019-06-02: * Section 3.3.2 and 3.3.3 headings (page 71) - the headings go past the intended margin (though they're quite readable). * Section 3.9.3 (page 97) - "appraoch" should be "approach". +* Section 3.10 (page 103 and 104) - the output of "show statement ax-1/full" + seems to be shown twice (once at the end of page 103, and once at the top of + page 104). * Section 4.3 (page 138) - there is a superfluous comma: "... option to hide, them, but today ...". * Section 4.3.1 (page 139) - "used and that each $f hypothesis have" From 505b93b703fe21a80bdd14106ed466305cffee5b Mon Sep 17 00:00:00 2001 From: amackay Date: Mon, 17 Aug 2020 14:36:15 +0930 Subject: [PATCH 3/3] Update errata.md to include recently fixed issues --- errata.md | 62 ++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 52 insertions(+), 10 deletions(-) diff --git a/errata.md b/errata.md index bc1c3d6..c0dd6f4 100644 --- a/errata.md +++ b/errata.md @@ -1,35 +1,71 @@ # Errata The following are errata for the Metamath 2019 ("Second Edition") book -dated 2019-06-02: +dated 2019-06-02. Issues marked with an asterisk (*) have not yet been +fixed in the repository version of the book. +* Preface (page x) - "able follow a proof" should be "able to follow a proof". +* Preface (page xiv, Note on Bibliography and Index) - "find it in on" should + be "find it on". * Preface (Note Added March 7, 2019) - Matamath --> Metamath -* Section 1.4.2 (page 32, paragraph 3) - +* Section 1.1.1 (page 4) - "allows you do" should be "allows you to do". +* Section 1.1.6 (page 20) - "may be correspond" should be "may correspond". +* Section 1.3.2 (page 27) - "a way that can not only able to" should be "a way + that is not only able to". +* Section 1.3.4 (page 28) - "is a mostly a proof verifier" should be "is mostly + a proof verifier". +* *Section 1.4.2 (page 32, paragraph 3) - there's an extraneous ")" after the term set.mm. -* Section 2.4 (page 52) and further shows this text after some assign commands: +* Section 1.4.4 (page 34) - "making it is easy" should be "making it easy". +* Section 2.3 (page 49) - "You can could use" should be "You could use". +* *Section 2.4 (page 52) and further shows this text after some assign commands: "To undo the assignment, DELETE STEP ... and INITIALIZE, UNIFY if needed." This text is no longer shown. When the first edition of the book was written, metamath.exe didn't have the 'undo'/'redo' commands (added in 2013; see 'help undo'), so hints were provided by some commands for how to undo them manually. These hints are no longer displayed since they are no longer needed. -* Section 3.3.2 and 3.3.3 headings (page 71) - the headings go past +* Section 2.4 (page 53) - "examples where is it used" should be "examples + where it is used". +* Section 3.1 (page 60) - "allow us determine" should be "allow us to + determine". In the same paragraph, "allows to say" should be "allows us to + say". +* Section 3.2.2 (page 67) - "auxilliary" should be "auxiliary". +* Section 3.2.4 (page 70) - "Tarsky-Grothendieck" should be + "Tarski-Grothendieck". +* *Section 3.3.2 and 3.3.3 headings (page 71) - the headings go past the intended margin (though they're quite readable). +* Section 3.4.3 (page 82) - "Similar to definition on" should be "Similar + to the definition on". * Section 3.9.3 (page 97) - "appraoch" should be "approach". -* Section 3.10 (page 103 and 104) - the output of "show statement ax-1/full" - seems to be shown twice (once at the end of page 103, and once at the top of +* *Section 3.10 (page 103 and 104) - the output of "show statement ax-1/full" + is shown twice (once at the end of page 103, and once at the top of page 104). -* Section 4.3 (page 138) - there is a superfluous comma: - "... option to hide, them, but today ...". +* Section 3.10.1 (page 109) - "may be be slightly" should be "may be + slightly". +* Section 4.1.3 (page 114) - "scope nd" should be "scope and". +* Section 4.2.5 (page 127) - "are also valid class expression" should be "are + also valid class expressions". +* Section 4.3 (page 138) - "Historically `show proof` command did" should be + "Historically the `show proof` command did". + There is also a superfluous comma: "... option to hide, them, but today ...". * Section 4.3.1 (page 139) - "used and that each $f hypothesis have" should be "used, and each $f hypothesis must have". +* Section 4.4.1 (page 142) - "parenticals" should be "parentheticals". +* Section 4.4.2 (page 146) - "asked to product" should be "asked to produce", + "and another uses" should be "and another that uses", and "bibiographic" + should be "bibliographic". +* Section 4.5.3 (page 155) - "statemnets" should be "statements", and + "Every dummy variable in the definiendum are required to" should be + "All dummy variables in the definiendum are required to". * Section 4.5.4 (page 155) - "Metmath" should be "Metamath". -* Chapter 5 mentions the minimize command, but does not describe it +* *Chapter 5 mentions the minimize command, but does not describe it in detail. A future version of the book might describe it in more detail. +* Section 5.2.9 (page 161) - "lets you to change" should be "lets you change". * Section 5.6 (page 168) - In "The undo command if very helpful", the "if" should be "is". * Section 5.6.3 `set empty_substitution` Command (page 171) - - there's a duplication and the first bracketed text could be removed. + there's a duplication and the second bracketed text could be removed. It says: "(An example where this must be on would be a system that implements a Deduction Rule and in which deductions from @@ -40,4 +76,10 @@ dated 2019-06-02: a system needing empty substitutions; another example would be a system that implements a Deduction Rule and in which deductions from empty assumption lists would be permissible.)" +* Section 5.6.11 (page 174) - "and to do `save new_proof` frequently" should be + "and do `save new_proof` frequently". +* Appendix A (page 184) - Part of the description of the uniqueness quantifier + is "there is at least one x". It should be "there is exactly one x". +* Appendix C (page 192) - "declared to be say, a string" should be "declared + to be, say, a string".