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.
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. Anyways, I will attach and share what I have written so far as soon as I know that I am approved for the mailing list. -- 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/a0f87ea1-1c03-4d2e-aaa4-2bb45a28c287n%40googlegroups.com.
