I'm writing a more "explanatory" database.

[Marshall Stoner]

I organized it into chapters and gave theorems numbers.  This is so they can later accompany a PDF that contains meta-logical justifications explains some things at a higher level. Read the heading for an explanation of the notation I use for axiom / definition / theorem tags.  My long term goal is to write a Gödel numbering system.

So far I've gotten through writing the logic section.  Because I'm trying to be more general, I'm not using the exact same approach as set.mm.  The only major differences seem to be with regard to set.mm's ax-13.  So far I've avoided the need for it by specifying that all ordinary object/set variables are distinct.  I can use term metavariables (which need not be distinct from anything else) for the left side of definitions to make them eliminable.  ax-13 ( and ax-6 without a disjoint specification) don't hold when terms can contain functions such as with the Peano Axioms. For instance, `E. x x = t_t` doesn't hold unless you specify that `t_t` is disjoint from `x`, because `t_t` could be `x + 1` `x = t_t` always false ( I use a prefix 't_' and color green for terms ).  set.mm uses classes where terms would normally be used, but I can't really follow that path if I'm not doing set theory.

I have some more to talk about but would like to see if anyone is interested before I go into more detail.  I attached the file.

[Alexander van der Vekens]

Interesting approach. I just downloaded th *.mm file, and it ican be imported and verified by metamath.exe without problems. Since it is a huge file, I did not have a look at it in detail/at everything, but here are some remarks/questions:

* to prefix wwfs with "w_" looks a little bit strange (example: `( w_ph -> ( w_ps -> w_ch ) )`): is there any reason for such prefixes?

* 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?

* I still cannot see any advantages (except the more formal namings) compared with set.mm.

[Marshall Stoner]

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.  

[Marshall Stoner]

I've made some progress and uploaded html files to my GitHub Pages. 

Here is the link .

I derived a natural deduction system.  To understand, just look at...

4.2 Natural Deduction for Propositional Calculus and

8.1 Natural Deduction for Predicate Calculus .

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.