A concept: a book that starts by assuming the understanding of the reader and using concepts freely, and as you go on it introduces a simple formal procedure for defining words. As you proceed, more and more words are defined in terms of the basic formal procedure, so that halfway through, half of the words being used are formally defined, and by the end the entire thing is formally defined. Once you’re read through the whole book, you can start it over and read from the beginning with no problem.
I just finished a set theory textbook that felt kind of like that. It started with the extremely sparse language of ZFC: first-order logic with a single non-logical symbol, ∈. So the alphabet of the formal language consisted of the following symbols: ∈ ( ) ∧ ∨ ¬ → ↔ ∀ ∃ x ‘. It could have even started with a sparser formal language if it was optimizing for alphabet economy: ∈ ( ∧ ¬ ∀ x ‘ would suffice. As time passed and you got through more of the book, more and more things were defined in terms of the alphabet of ZFC: subsets, ordered pairs, functions from one set to another, transitivity, partial orders, finiteness, natural numbers, order types, induction, recursion, countability, real numbers, and limits. By the last chapter it was breathtaking to read a sentence filled with complex concepts and realize that every single one of these concepts was ultimately grounded in this super simple formal language we started with, with a finitistic sound and complete system of rules for how to use each one.
But could it be possible to really fully define ALL the terms used by the end of the book? And even if it were, could the book be written in such a way as to allow an alien that begins understanding nothing of your language to read it and, by the end, understand everything in the book? Even worse, what if the alien not only understands nothing of your language, but starts understanding nothing of the concepts involved? This might be a nonsensical notion; an alien that can read a book and do any level of sophisticated reasoning but doesn’t understand concepts like “and” and “or“.
One way that language is learned is by “pointing”: somebody asks me what a tree is, so I point to some examples of trees and some examples of non-trees, clarifying which is and which is not. It would be helpful if in this book we could point to simple concepts by means of interactive programs. So, for instance, an e-book where an alien reading the book encounters some exceedingly simple programs that they can experiment with, putting in inputs and seeing what results. So for instance, we might have a program that takes as input either 00, 01, 10, or 11, and outputs the ∧ operation applied to the two input digits. Nothing else would be allowed as inputs, so after playing with the program for a little bit you learn everything that it can do.
One feature of such a book would be that it would probably use nothing above first-order logical concepts. The reason is that the semantics of second-order logic cannot be captured by any sound and complete proof system, meaning that there’s no finitistic set of rules one could explain to an alien so that they know how to use the concepts involved correctly. Worse, the set of second-order tautologies is not even recursively enumerable (worse than the set of first-order tautologies, which is merely undecidable), so no amount of pointing-to-programs would suffice. First-order ZFC can define a lot, but can it define enough to write a book on what it can define?
I suppose the interaction tool you speak of is partially realized by a compiler, say of Coq, Adga, Mizar or Metamath. It’s actually interesting to read the first long page of the latter, since they so freely describe their process and options in design.
I don’t follow the last paragraph relating to the lack of incompleteness theorem, since the example is about finite inputs. From the example, it sounds like the books return values itself on a semantic implementation. I’m not sure if meta-theorems across logics have a high impact at all, given the amount of interaction queries with the book will be finite too.
Yes! A program that explains how to write itself would be a great example of the type of thing I’m looking for. As for the last paragraph, what I’m trying to say is that there’s an extra difficulty involved in communicating a second-order concept to an alien, compared to a first-order concept. Even if you could teach the alien how formal systems work, you would fail to produce any formal system that characterizes the semantics of that concept. For a first-order concept, you could at least hand them a formal system that details the exact rules for correct usage of the concept.
Good questions.
“First-order ZFC can define a lot, but can it define enough to write a book on what it can define?”
Yes, with the proviso of certain amounts of good will, good intentions and some motivation. Ultimately, the question of the consistency of ZFC is provenly taken on faith! (for if we prove that a certain class M is a model of ZFC…). Thus ZFC is not proper to discuss with people of bad faith who know it because they can repeat after every sentence of ours “all this is on air”.
Thus the writing of such a self compiling in all OS’s book (using a metaphor here) is impossible.
BTW, native language learning takes much more than “pointing” which in this context I believe is meant by you as model showcasing in the sense that e.g. concrete dihedral groups, some symmetries and perhaps S5 is the right way to point to the group axioms and then in an almost mystical way to take the leap to the formality of a group as an L-structure with no relations, one function and one constant. Despite what Montague said, language is a social thing.