Hi, and what about when you do have both T and Ti? Do you know how I then should go to Td?
Op dinsdag 15 augustus 2023 om 19:02:08 UTC+2 schreef [email protected]: > From my understanding the non-trivial case is when you have Ti, but > neither T nor Td. I think most theorems in the set.mm database have a > deductive or closed form somewhere, but you might have to use a proof > assistance tool to search based on the form if the name isn't obvious. > When writing your own theorems/lemmas you should always put an arbitrary > antecedent before every hypothesis so you are always in deductive form. > To use a deductive form theorem you need to first obtain matching > antecedents for each hypothesis used. You can use "a1i" to add antecedents > to the left hand side, then use "imp" or "exp" to convert chained > antecedents into conjunctions that you can change the order of using > commutative and associative properties. > On Tuesday, August 15, 2023 at 11:41:48 AM UTC-4 [email protected] > wrote: > >> Thanks a lot! >> >> Also, the website states: >> >> "As noted earlier, we can also easily convert any assertion T in closed >> form to its related assertion Ti in inference form by applying ax-mp >> <https://us.metamath.org/mpeuni/ax-mp.html>. The challenge, when working >> formally, can sometimes occur when converting some arbitrary assertion T in >> inference form into a related assertion Td in deduction form" >> >> Still, are there some examples or are there general guidelines that will >> help with this process? How would I go about converting Ti to Td in the >> example stated above (or from Ti to T)? >> >> Again, many thanks! >> Op dinsdag 15 augustus 2023 om 17:02:33 UTC+2 schreef [email protected]: >> >>> On 8/15/23 07:49, David A. Wheeler wrote: >>> > Maybe we should note something in trud. >>> >>> Ooh, good idea. I hadn't thought of that as a mitigation. Submitted as >>> https://github.com/metamath/set.mm/pull/3388 >>> >>> >>> -- 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/b3b741b0-9532-486d-9500-de885367f289n%40googlegroups.com.
