> On Dec 31, 2023, at 7:32 PM, Jerry James <[email protected]> wrote: > > Greetings, > > Due to some real life events, I had to step away from metamath last year. > First, I want to apologize for ghosting the community on the last couple of > pull requests I made in 2022. I hope you can forgive me for that.
Welcome back!! I had the same problem in the latter part of 2023, where some personal challenges meant I was mostly unavailable & I'm only starting to be able to engage more. We're grateful for whatever time you can apply. > I would like to get involved again. When I stepped away, I was working on > some material related to formal languages. Some modifications to the > existing Word theorems would make that easier. In particular, some theorems > that mention two words in their antecedents require that both words be over > the same alphabet, but the proofs work even if they are not. That is, these > theorems only require that certain objects be words, and the alphabets in > question do not affect the proof. This matters when trying to prove theorems > about, for example, a language composed of words with prefixes from language > 1 and suffixes from language 2, where the two languages are not necessarily > over the same alphabet.\ We've often relaxed requirements on various theorems as they were found unnecessary (unless there was some special rationale, and I don't see one here). I think the same is true for this case. I'm glad you noticed this circumstance & look forward to your work! I'll note that Gödel's Incompleteness Theorem is #6 in the Metamath 100 list <https://us.metamath.org/mm_100.html>. If you make it easier to do proofs related to formal languages, and add more theorems about it, your work might make it easier to complete that theorem. > Unions can be used; e.g., if I have W e. Word S and X e. Word T, then the > existing theorems can be used by specifying that both words are elements of ( > S u. T ). That works, but it irks me that I have to do extra work because > the theorems unnecessarily constrain the alphabets. > > Would the community object if I start removing the same-alphabet constraints > where they are not necessary? I have opened a pull request for the first > such theorem, eqwrd: https://github.com/metamath/set.mm/pull/3731. It looks great! I see several people already reviewed it, all liked it, and it's already been merged. So I think you have your answer :-). This is exactly the process we like! Propose things incrementally so it's easier to review the change, tweak it where appopriate, merge, repeat. Thanks so much. > Wishing everybody a happy new year. Regards, You too! --- David A. Wheeler -- 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/093EC33A-70C8-4CCC-92B4-1B9C00E2071F%40dwheeler.com.
