I've made some progress and uploaded html files to my GitHub Pages. Here is the link <https://mbstoner53.github.io/bfol/html/mmtheorems.html> .
I derived a natural deduction system. To understand, just look at... 4.2 Natural Deduction for Propositional Calculus <https://mbstoner53.github.io/bfol/html/mmtheorems2.html#mm176b> and 8.1 Natural Deduction for Predicate Calculus . <https://mbstoner53.github.io/bfol/html/mmtheorems9.html#mm832b> I have 20 propositional natural deduction axioms, 12 axioms defining effective non-freeness, 4 axioms defining proper substitution, the usual 4 quantifier introduction and elimination laws, plus the normal axioms for equality and substitution. These axioms correspond almost exactly with textbook rules on natural deduction. They are listed as theorems, but I am able to re-derive the Hilbert axioms I started with, therefore the two systems are scheme-equivalent. On Monday, April 29, 2024 at 1:03:00 AM UTC-4 Marshall Stoner wrote: > Sorry I didn't explain how to view the contents. I've been browsing the > contents I'm creating by generating the html files in a folder with "show > statement * /alt_html" and "write theorem_list /alt_html". It's already a > lot of files, but only adds up to about 10MB at this time. The unicode > typsetting and links all work for just by opening mmtheoremlist.html with > Chrome. I realized some browsers don't support links when accessing a > local folder rather than an official server, which defeats the purpose of > using a browser. I haven't found a way to look at the html database on my > phone for example. VSCode with Live Server probably works though. > > On Sunday, April 28, 2024 at 5:44:39 AM UTC-4 Alexander van der Vekens > wrote: > > * to prefix wwfs with "w_" looks a little bit strange (example: `( w_ph -> > ( w_ps -> w_ch ) )`): is there any reason for such prefixes? > > > The prefixes aren't shown in the HTML output. The variables with prefixes > are just colored differently. I ended up using `t_` prefix for terms since > I thought I might want to use the same lowercase letters for set/number > variables ( I'm calling them object variables ). In the html typsetting > terms are distinguished as green, similar to how classes are distinguished > using a magenta color. I did the same for WFF metavariables for > consistency, though I don't think I will use Greek letters for object > variables. > > > * are the axioms used identical with the axioms of set.mm? Is " The only > major differences ... to set.mm is ax-13. " the only deviation? > > > It's not meant to be the same as set.mm. I'm using terms so I can > introduce Peano Axioms without any set theory. I also specify that object > variables are always distinct. This just feels more intuitive to me than > "bundling". Without terms this would be a problem because definitional > statements need non-distinct arguments to be eliminable (and thus qualify > as conservative extensions). Even without primitive functions, a term can > operate as wild card metavariable that contains an arbitrary single object > variable. Therefore terms are needed for definitional statements. The > only thing missing compared to set.mm seems to be the ability to bundle > quantifier variables. That isn't something that seems to have any > practical use (that I am aware of). > > Another thing is though I used mostly the same Hilbert-style axioms as > set.mm, once I "derive" the natural deduction rules, I use them as axioms > from then on. For example. In chapter 1 and 2 I gather enough from the > Hilbert-style propositional logic to derive a set of 20 "natural deduction > axioms" for propositional logic. These 20 axioms are stated at the > beginning of Chapter 3. From then on statements from chapters 1 and 2, > along with axioms 1-3 (and MP) are no longer referenced. At the beginning > of Chapter 7 I do the same thing with propositional logic, no longer > referencing statements from chapters 5 and 6 (which develop propositional > logic from the Hilbert-style propositional axioms) nor the rest of the > Hilbert style axioms. The idea is that with a small amount of editing, I > can eliminate chapters 1, 2, 5 and 6 and turn the natural deduction > statements into axioms. I believe something similar is done within set.mm > regarding complex numbers. Once the complex numbers are constructed via > the set theory axioms, they are defined from then on through a new set of > axioms such that the set theoretic construction no longer needs to be > referenced. > > Another advantage is the ability to keep track of the usage of the > excluded middle without using an entirely different set of axioms as in > iset.mm. I've also added comments rigorously showing how the "effective > non-freeness" and "proper substitution" predicates relate to the > traditional textbook definitions (chapter 6). This part could be > incorporated into set.mm. > > > * I still cannot see any advantages (except the more formal namings) > compared with set.mm. > > set.mm is better for research since its comprehensive and theorems are > proven with as few axioms as possible. What I'm writing is meant to be > more digestible for learning. The purpose of the formal namings is to > have every statement correspond to a numbered proposition/theorem/lemma in > a pdf book that explains things in a slightly less formal way. More like > the original Principia Mathematica that originally inspired metamath. I > will also try to keep similar statements together and use simple proofs > even if it means using more axioms. I also have longer proofs because I > don't have as many lemmas for the sake of limiting clutter. I can add > utility lemmas in "appendix" sections to make later proofs more efficient. > > Honestly, writing my own database from scratch has helped me understand > how the logic of metamath works. I was lost at first and it has been > rewarding. I'm having fun. > > Anyways, I attached the latest version. > -- 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/228c9ef8-9bb6-4eb2-a2a4-2c4a9d387995n%40googlegroups.com.
