Writing a pdf that organizes the introductory logic portion of set.mm.

[Marshall Stoner]

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.

[Mario Carneiro]

On Mon, Jul 3, 2023 at 7:31 PM Marshall Stoner <mbsto...@gmail.com> 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

[Jim Kingdon]

On 7/3/23 15:56, Marshall Stoner wrote:

> have written up everything I considered prior to the definition of the
> biconditional and conjugation.

> . . . will attach and share what I have written so far as soon as I
> know that I am approved for the mailing list. . . .

I'll be curious to see what you came up with and how you organize it. We
have some ways of organizing material on the website, for example "How
to intuitionize classical proofs" at
https://us.metamath.org/ileuni/mmil.html#intuitionize , "Real and
Complex Numbers" at https://us.metamath.org/mpeuni/mmcomplex.html , or
"Algebraic and Topological Structures" at
https://us.metamath.org/mpeuni/mmtopstr.html . All of these link to
relevant theorems but add explanations or give some structure in terms
of how one statement relates to another.

Making pull requests to the web site should now be possible but feel
free to ask if it isn't clear where files go, whether website scripts
need to be changed, etc.

Semi-relatedly, someone recently asked on Mastodon what a good source
for the constructive ordinals is. There have been three suggestions so
far. One is a normal math book (the HoTT book). The other two are
collections of formalized proofs (iset.mm and TypeToplogy). And neither
of the latter two give you an especially good idea of where to find the
ordinal stuff and where to start. It got me thinking about how to make
the material we have easy to read especially in cases where noone has
written a textbook which lays everything out carefully with the purpose
of teaching. Anyway, the thread is
https://mathstodon.xyz/@boarders/110646213816213644 in case anyone is
interested.

[Marshall Stoner]

Thanks.  I was not very specific because I was waiting to make sure I was actually subscribed to the group.  I attached the pdf to show you the idea of what I'm doing.  I would like to provide the quickest and easiest way forward to that start of ZFC theory while still being formally precise.  Like you said, there are far too many theorems to easily convert into a "book form" that includes everything.  I have the propositional logic part figured out for the most part, but predicate logic becomes tricky.  The proofs become long and confusing and it is not always clear that the proofs provided are all the quickest, or even which results are actually useful.  I'm not saying there's anything wrong since the purpose of metamath is not elegance, but simply to document theorems rigorously.  I'm just interested in creating a more understandable "book", using mostly the same syntax and axioms to go along with it.   At least the foundational portion.

Just skimming what I've wrote so far should explain what I'm doing (feel free to tell me if there are mistakes, if you notice).  At some point I will probably start adding more "proof recipes" to be able to make the proofs more compact.  If I was ever to convert my own syntax (which I'm still trying to figure out) to a meta-math database, the "recipes" could be generated procedurally on the fly and added to the database where needed.  The point is I'm trying to write everything in a way such that it could be procedurally converted to a metamath database.

I will try to hack away more at the proper substitution section.  I'm mainly interested covering as many theorems as needed to show that the definition is equivalent to a recursively defined definition with literal substitution.  That is where I'm stuck.  I believe I have enough to do this for the "effectively not free" definition, as the necessary theorems that could be strung together into an equivalent recursively definition obvious.  I'm having trouble finding the equivalent theorems in the proper substitution case.  Hopefully this clears things up.  I don't need answers right away.  I'm just exploring at this point.

[Marshall Stoner]

I wanted to share the pdf I've written so far but it didn't send and I lost what I wrote.  I guess attachments aren't allowed.  I'll post a link instead.

pdf file

[Mario Carneiro]

(This group is manually moderated, so posts may not appear immediately.)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/77ecbdd0-a0e5-4977-aa66-aa772768a651n%40googlegroups.com.

[Mario Carneiro]

> I will try to hack away more at the proper substitution section.  I'm mainly interested covering as many theorems as needed to show that the definition is equivalent to a recursively defined definition with literal substitution.  That is where I'm stuck.  I believe I have enough to do this for the "effectively not free" definition, as the necessary theorems that could be strung together into an equivalent recursively definition obvious.  I'm having trouble finding the equivalent theorems in the proper substitution case.  Hopefully this clears things up.  I don't need answers right away.  I'm just exploring at this point.

Okay, this helps somewhat with understanding the motivation. If you want to prove that substitution is equivalent to the recursive definition, you will need cases for every formula constructor. There are a few alternative methods to do that, metatheorems phrased in slightly different ways all of which are equivalent. In order of how well supported they are:

1. Implicit substitution. These are theorems that say `( ph -> F(x1, ..., xn) = F(y1, ..., yn) )` given `( ph -> x1 = y1 )`, ..., `( ph -> xn = yn )`.

2. Not free: These are theorems that say `F/ z F(x1, ..., xn)` given `F/ z x1`, ..., `F/ z xn`.

3. Explicit substitution: These are theorems that say [ a / b ] F(x1, ..., xn) = F([ a / b ] x1, ..., [ a / b ] xn).

These are to be interpreted with `=` being used to mean either `<->` or `=` as appropriate. The statements for binders are also somewhat different; this is the prototypical form for regular class or wff operators.

Your theorem is most similar to (3), but it is also the least well supported in terms of theorems for every constructor. (That is, you aren't going to find a theorem saying that a random non-foundational definition like df-lly commutes with explicit substitution.) However, (1) has essentially full support in the library - there is a theorem of the described form for basically every definition, so if you can rewrite the goal such that it is in terms of implicit substitution, then you can apply that metatheorem and it all works.

In this case, you want to say that `[ y / x ] P(x)` is equivalent to `P(y)`, where `P(x)` represents any propositional formula containing free occurrences of `x`. To do this, we would apply theorem https://us.metamath.org/mpeuni/sbie.html , which reduces the goal to a case of (1) and a case of (2). (It is possible to avoid a dependence on metatheorem (2) as well, by alpha renaming all bound occurrences of x in P(y) to something else, so that P(y) syntactically contains no occurrences of x and theorem ~nfv applies. Proving that such an alpha rename is legal is a recursive application of (1).)

The metatheorem (1) is worked out for all the primitive constructors in the section https://us.metamath.org/mpeuni/mmtheorems36.html#mm3566s ; using those theorems you can prove that the implicit substitution metatheorem holds for any formula built up from those primitives, and then it is a short hop using theorems like ~sbie to get other forms of it involving explicit substitution, not free, alpha renaming, or other things.

[David A. Wheeler]

> On Jul 3, 2023, at 10:58 PM, Marshall Stoner <mbsto...@gmail.com> wrote:
>
> Thanks. I was not very specific because I was waiting to make sure I was actually subscribed to the group. I attached the pdf to show you the idea of what I'm doing. I would like to provide the quickest and easiest way forward to that start of ZFC theory while still being formally precise. Like you said, there are far too many theorems to easily convert into a "book form" that includes everything.

It's up to you, but one possibility would be create a document in the set.mm repo
with the name `mmSOMETHING.raw.html`. These are just normal HTML files, but anything in
`...` is processed by metamath-exe to generate nicer-looking HTML for the equations.
This is how we generate, for example, mmcomplex.raw.html - this is processed and
turned into mmcomplex.html for use as a final document. There's no obligation to use
that mechanism, but you might find it useful.

I've thought about creating a "tour guide" of sorts that points out and explains the highlights
(without going into the details of *every* theorem) - it sounds like you might have a somewhat
similar goal. If it's in the set.mm repo, it can be updated along with the rest of set.mm.

--- David A. Wheeler

[Marshall Stoner]

> 1. Implicit substitution. These are theorems that say `( ph -> F(x1, ..., xn) = F(y1, ..., yn) )` given `( ph -> x1 = y1 )`, ..., `( ph -> xn = yn )`.

> 2. Not free: These are theorems that say `F/ z F(x1, ..., xn)` given `F/ z x1`, ..., `F/ z xn`.

> 3. Explicit substitution: These are theorems that say [ a / b ] F(x1, ..., xn) = F([ a / b ] x1, ..., [ a / b ] xn).

> These are to be interpreted with `=` being used to mean either `<->` or `=` as appropriate. The statements for binders are also somewhat different; this is the prototypical form for regular class or wff operators.

Thanks!  This info is helpful.  It is the relationship between theorems of type 1 and 3 that has me somewhat confused.  It seems like allowing bundled variables is what causes a lot of complexity in a few proofs.  My philosophy would be to keep variables distinct except for special cases where it might be necessary or helpul ( not quite sure what all those cases are, but they mostly seem to involve substitution and axioms 12 and 13 from my partial understanding ).  I understand that allowing bunded variables makes proof checking faster, but I'd rather avoid it wherever that is the *only* reason, mainly because it just seems less intuitive to me than distinct variables.

> Your theorem is most similar to (3), but it is also the least well supported in terms of theorems for every constructor. (That is, you aren't going to find a theorem saying that a random non-foundational definition like df-lly commutes with explicit substitution.) However, (1) has essentially full support in the library - there is a theorem of the described form for basically every definition, so if you can rewrite the goal such that it is in terms of implicit substitution, then you can apply that metatheorem and it all works.

I'm pretty confident I can figure this part out.

> In this case, you want to say that `[ y / x ] P(x)` is equivalent to `P(y)`, where `P(x)` represents any propositional formula containing free occurrences of `x`. To do this, we would apply theorem https://us.metamath.org/mpeuni/sbie.html , which reduces the goal to a case of (1) and a case of (2). (It is possible to avoid a dependence on metatheorem (2) as well, by alpha renaming all bound occurrences of x in P(y) to something else, so that P(y) syntactically contains no occurrences of x and theorem ~nfv applies. Proving that such an alpha rename is legal is a recursive application of (1).)

This is the part I need to study more.  Thanks again.

[Marshall Stoner]

Though I do have programming experience, it's been a long time.  I need to learn how to work with github (something I plan to do anyways for other work).  

The kind of application that would really interest me would be one that can utilize routines to construct instances of meta-theorems in raw metamath language.  I figure this would reduce the visibility of a lot of boilerplate steps needed employ very instinctual steps like simple substitutions and antecedent rearrangement / matching for natural deduction.  In most metamath proofs it seems most of the difficulty in reading comes from the amount of boilerplate that isn't easy to immediately recognize as such.  There are a lot of specialized logic theorems to make proofs shorter, but being shorter doesn't make them easier to understand as you end up jumping down deeper and deeper into a wormhole of sub-theorems and lose track of the big picture, in the logical sense.

What I'm writing is not directly connected with meta-math, but something that I feel could help explain it better for novices and could be made to match up easily.

[Jim Kingdon]

On 7/4/23 14:45, Marshall Stoner wrote:

> It seems like allowing bundled variables is what causes a lot of
> complexity in a few proofs.  My philosophy would be to keep variables
> distinct except for special cases where it might be necessary or helpul

Specifying distinct variables most of the time is the way I would tend
to write proofs. I'm not sure I can think of any case where you need to
specify two different set variables without a distinctness constraint.
Of course with a class variable and a set variable you need to omit the
distinctness constraint where the class is in terms of that variable.
Example: if A is "( x + 1 )" and a theorem has A and x in it, then there
can't be a distinctness constraint between A and x . I guess a formula
variable and a set variable are similar Example: if ph is "x > 5" then
ph and x are not distinct.

[Jim Kingdon]

On 7/4/23 15:07, Marshall Stoner wrote:

> What I'm writing is not directly connected with meta-math, but
> something that I feel could help explain it better for novices

I'd advise you to follow where the inspiration leads you. If you end up
with something which has a lot of metamath notation and reference to
metamath theorems by name, that's great, and may indeed be helpful to
put on the web site in one form or another if you want to contribute it
in that fashion. If what you want to do (in terms of how it makes sense
to present the material or whatever) ends up diverging more from
metamath in detail and ends up being more of a general logic textbook,
that's cool too.

[Marshall Stoner]

Thank you.  I am thinking of using duplicating everything I write in text with the metamath language, but I think I'd prefer to build my own version of set.mm with my own proofs and also axiom and theorem names that match the text numbering and naming system.  I can link to the equivalent result in set.mm for the important theorems.  It would be nice to learn how to do this.  

I also do not have a degree in logic and might need help with using proper terminology, but I will only be cover the deductive system (what's needed for metamath).  This is a hobby.  I have read some of the material and the site and have a few references of my own.  The Stanford Encyclopedia of Philosophy has a good online introductory article called Classical Logic.  

[Marshall Stoner]

To Jim.

I feel like a big problem with metamath is that it just isn't satisfying without some foundational understanding of mathematical logic.  Sure, you can follow proofs and see that each step is justified by digging down 100 layers, but it's not pretty.  For motivation on how to construct proofs from scratch and feel confident, you really need to understand classical logic from a higher perspective.  Sure, there are tools that fill in the gaps for you, but I'm the kind of person that really needs to understand all the nuts and bolts to feel good about something.  It's also hard to convince myself that I understand a topic if I am not able to explain it to others.  Writing a pdf is the way I'm learning.

I think I might need to invest in a better text.  I've been trying to read Introduction to Mathematical Logic by Mandelson (because I found it for free), but can't stand the layout.  The author does nothing to make important definitions stand out and the proofs are all jammed into a single paragraph and not always worded well either.  I do have a good text on ZFC set theory ("Axiomatic Set Theory" by Suppes) and have taken a class on that a long time ago.  It just isn't super formal and doesn't cover logic or proof theory at all.  I'd like to find a better introduction to logic but I'd hate to buy a clone of Mendelson.  It's tough to tell how good a text is based on reviews.

On Tuesday, July 4, 2023 at 7:08:50 PM UTC-4 kin...@panix.com wrote:

[David A. Wheeler]

> On Jul 16, 2023, at 9:04 PM, Marshall Stoner <mbsto...@gmail.com> wrote:

> I do have a good text on ZFC set theory ("Axiomatic Set Theory" by Suppes) and have taken a class on that a long time ago. It just isn't super formal and doesn't cover logic or proof theory at all. I'd like to find a better introduction to logic but I'd hate to buy a clone of Mendelson. It's tough to tell how good a text is based on reviews.

It's not exactly what you're looking for, but you might find this paper interesting, which tries to justify the ZFC axioms:

Believing the Axioms. Penelope Maddy. The Journal of Symbolic Logic, Vol.53,No.2.(Jun.,1988),pp.481-511.
https://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf

It sounds like you're looking for something similar for predicate and propositional logic.

--- David A. Wheeler

[Ken Kubota]

My recommendation is Peter B. Andrews’ textbook from 2002, as mentioned here: https://owlofminerva.net/files/fom_2018.pdf#page=2

In terms of expressing mathematics naturally I haven’t seen anything better, although it is still simple type theory (without type variables).

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/48543c4c-282a-4f69-b408-e8e7796de91an%40googlegroups.com.

[Johnathan Mercer]

That Figure is a gem - thanks for sharing!

{typed with my thumbs}

On Jul 17, 2023, at 11:31 AM, Ken Kubota <ma...@kenkubota.de> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/84FD024B-ED9D-4952-BE13-924F3EE42258%40kenkubota.de.

[Ken Kubota]

You are welcome.

Page references for [Andrews, 2002] are available here: https://www.owlofminerva.net/files/formulae.pdf#page=825

____________________________________________________

Ken Kubota
https://doi.org/10.4444/100

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/A84EED97-36B5-4BDD-8CEC-8B93F84515C4%40gmail.com.