> 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. On Tue, Jul 4, 2023 at 2:10 AM Mario Carneiro <[email protected]> wrote: > (This group is manually moderated, so posts may not appear immediately.) > > On Tue, Jul 4, 2023 at 2:04 AM Marshall Stoner <[email protected]> > wrote: > >> 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 <https://1drv.ms/b/s!AuvNPSOQfN3xjKxgB2QVuLZMOT_W5Q?e=FCRy2b> >> On Monday, July 3, 2023 at 11:31:45 PM UTC-4 [email protected] wrote: >> >>> 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. >>> >>> >>> -- >> 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/77ecbdd0-a0e5-4977-aa66-aa772768a651n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/77ecbdd0-a0e5-4977-aa66-aa772768a651n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/CAFXXJSsmtL4qnUPj3MqSFLBmgaXicBwMQ2qLYi%2BYuVSXZ-rbmQ%40mail.gmail.com.
