The commonly used terms for what would become the "sets" were "mannigfaltig (manifold, or as it was rendered by Clifford's translation of Riemann's habilitation, "manifoldness", and which was what Cantor called sets in the paper where he introduced the concept of ordinals) and "inbegriff (tough to translate, but it isn't just "collection" --- this was used in Cantors paper on algebraic numbers)", and "notion (used by Clifford)" and even a "multiplicity". It wasn't until Cantor's 1885 paper on "menge" that sets were clearly defined as collections of definite mathematical objects.

I write this because there is a tendency among mathematicians to rewrite mathematical history so as to make the current accepted practices seem logically inevitable. This is so common that it's largely unnoticed. But the ways we think about mathematics today are the result of historical processes, and are not eternal or necessary.

You can in fact do all of mathematics without a notion of collection --- if you use the notion of "type" (type, concept, notion, kind, sort...). This is almost a distinction without a difference, because the type theoretic theories of sets (where a set is a type for which the identification of elements is a proposition, or in the case of a subset is equated with its membership predicate) is equivalent to the set theoretic theory of sets (where sets are collections). But still, it narrows a students' view of the broadness of mathematics to say that the idea of a collection is necessary to do mathematics.

typo -- missing space

Nice

I would have expected the elimination principle to say that if a has been deduced and ~a has been deduced, then any formula b is a valid deduction. I suppose that doing it that way doesn't build in double negation elimination though.

It's an interesting choice to including parsing as part of the work of doing logic here. It's cool in that it really does convince the reader that these things could be implemented in a computer. But it might be getting in the way of the idea of what a formal proof is supposed to do.

It may be more correct to say: whether any given string of symbols (or however the syntax is presented) constitutes a proof or not. Proofs are, by definition, valid: "A proof is a series of statements, starting with some hypotheses andproceeding by valid inferences to a conclusion."

I've always preferred the Gentzen style presentations to the Fitch ones, but it's not a real issue. I suppose the idea is to have a "proof" be something resembling a file which can be read character by character.

I appreciate the time given to describing how formalizing reasoning is largely a design problem, but I also think it is worth mentioning that there are actually different logics that reach different conclusions --- it's just that one logic is overwhelmingly standard. Ultimately, that's a historical accident, and not a mathematical fact.

This is an instance of the (categorical) induction principle.

I feel that the positive way to say this would be clearer: any WFF is of the forms (a) (b) or (c). (This is, of course, really a hidden way to state the mapping property of the set of WFFs.)

Just in case, let me state that mapping property, both in the set theoretic and in the "type theoretic" styles, so it's clear what I mean.

The set theoretic induction principle says that the set of WFFs is the smallest set containing the atomics and closed under the connectives. Explicitly, if X is a set containing the atomic formulas and closed under the operations, then X contains the set of WFFs.

The type theoretic induction principle says that to construct any mathematical object c assuming as given a WFF F, it suffices to construct c in the cases that F is atomic, that F is of the form ~G for G a WFF, that F is of the form G&H etc.

Why not, the category theoretic way to state this induction principle is that if X is any set and for every atomic a we have an associated element f_0(a) in X and for every x in X we have an element ~x in X and for every x and y in X we have an element x&y in X etc, then there is a unique function assigning each WFF F to an element f(F) of X so that atomics a are assigned to f_0(a), ~F is assigned to ~f(F), etc...

typo

I don't know if you had occasion to describe structural induction before in the book, but by virtue of the fact that the definition of WFFs is inductive (the set of WFFs is the smallest set such that blah, which is to say that the set has a mapping-out property), you can do induction on it right away without needing to encode this through an arbitrary metric.

Why the choice of these symbols rather than the more common "\neg", "\wedge", "\vee"?