On Mon, Jul 3, 2023 at 7:31 PM Marshall Stoner <[email protected]> wrote:
> I'm going through the database trying to understand everything from very > first principles. One of my frustrations in trying to follow proofs on the > site is the cryptic naming of theorems and lack of organization of theorems > by usage or importance. I have managed to get through the propositional > logic section and have written up everything I considered prior to the > definition of the biconditional and conjugation. Regarding the naming convention, I do encourage reading https://us.metamath.org/mpeuni/conventions-labels.html . It is certainly not something we expect you to just know without learning it, but it is effective once you know the basic patterns. (It is somewhat similar to vim keybindings in this regard.) As far as organization is concerned, it is primarily organized by topic, with a concession for dependency order when it becomes an issue. Reading set.mm "cover to cover" sounds like quite a daunting task and you can probably start to skim a lot of sections once you get past the first couple theorems that set up the new material to be covered in the section. (Especially in propositional logic and predicate logic, this part is almost entirely composed of utility theorems and once you've seen one you've seen them all.) A better way to find theorems that interest you is to use depth-first search on an interesting theorem, sometimes alternating between following backreferences and using the "related theorems" link to look around in the section. You can also use the "used by" links to travel forward along those links. Basically, treat it as a web of related theorems and definitions, not so much a linear arrangement of chapters. You can interpret it that way to some extent but the sections are probably much too long for a real "book" like experience. But that's just my opinion, everyone has different approaches to learning and YMMV. > It is in the section with theorems regarding "proper substitution" where I > am somewhat lost without additional resources at this point. Substitution > is utilized in order to define classes, which are used extensively later > on, but the motivation behind the theorems and definitions regarding > substitution is lost on me. I cannot find which theorems are important to > build the expected behavior starting with atomic wffs and working up > through induction by adding theorems regarding quantifiers and logical > connectives. There is also nothing distinguishing which proofs are the > most important, plus many theorems that really belong together conceptually > are placed far away form each other on the site as set.mm places theorems > that require fewer axioms much earlier. > The short answer for the motivation for substitution is that we want to define a notion of "replace occurrences of x with y in ph" such that "[ y / x ] ( ( x + 1 ) = 0 /\ A. x x = 5 )" is equivalent to (or "evaluates to" if you prefer to think of it that way) "( ( y + 1 ) = 0 /\ A. x x = 5 )". In other words, the proper substitution of free occurrences of the variable. There is an additional complication for the case when x and y are not disjoint, but ignoring that the key definitional lemma is https://us.metamath.org/mpeuni/sb6.html . (This is covered to some extent in the docstring on https://us.metamath.org/mpeuni/df-sb.html , with specific links to what we consider to be the important theorems and the intended interpretation of the notation. If you think this documentation can be improved, we of course welcome any tweaks you would like to suggest.) Mario Carneiro -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsJE2fQALaz9Xj3tGfiFDUPt2Xk0pO4SFTspXkdg8h24g%40mail.gmail.com.
