Trouble understanding Deduction style

[Jeroen van Rensen]

Hello everyone,

I am reading metamath.pdf and I have a few questions about section 3.9.3 Deduction style, specifically the conversion methods between Td, Ti and T.

T is a statement in closed form (with no hypotheses).

Td is a statement in deduction form (where all hypotheses are implications with the same antecedent).

Ti is a statement in inference form (where all hypotheses don't have the same antecedent).

The section states that is is possible to go from Td to Ti, from Td to T and from T to Ti. I have trouble understanding the first two conversions.

Take for example:

• T: !!q -> q
• Td: p -> !!q |- p -> q
• Ti: !!q |- q
  

From Td to Ti

"To prove some assertion Ti in inference form, given assertion Td in deduction form, there is a simple mechanical process you can use. First take each Ti hypothesis and insert a T. → prefix (“true implies”) using a1i. You can then use the existing assertion Td to prove the resulting conclusion with a T. → prefix. Finally, you can remove that prefix using trud, resulting in the conclusion you wanted to prove."

This is how I understand it:

1. Take !!q as a hypothesis
   !!q
2. Add the prefix "T ->" (true implies)
   T -> !!q
3. Use Td to get:
   T -> q
4. Remove the prefix using trud???

What I don't understand is how you can use trud to go from T -> q to q.

trud states that for wff q, (q -> T) and not in reverse. Am I missing something here?

From Td to T

"To prove some assertion T in closed form, given assertion Td in deduction form, there is another simple mechanical process you can use. First, select an expression that is the conjunction (...∧...) of all of the consequents of every hypothesis of Td. Next, prove that this expression implies each of the separate hypotheses of Td in turn by eliminating conjuncts (there are a variety of proven assertions to do this, including simpl, simpr, 3simpa, 3simpb, 3simpc, simp1, simp2, and simp3). If the expression has nested conjunctions, inner conjuncts can be broken out by chaining the above theorems with syl (see section 3.6).13 As your final step, you can then apply the already-proven assertion Td (which is in deduction form), proving assertion T in closed form."

This is how I understand it:

1. Get the conjuction from all of the consequences of every hypothesis, in my case:
   !!q
2. Prove that !!q |- p -> !!q
   This can easily be done by ax-1 and ax-mp
3. Use Td to prove T???

I have no idea how to finish this proof.

Conclusion

I worked out the steps and I hope someone can tell me what I did wrong or what I missed. An example from set.mm where this is done would also be nice.

Thank you!

[Jim Kingdon]

Thanks for saying something. The reference to trud (cited in your "From Td to Ti" section) is supposed to be mptru .

This has been corrected in git - https://github.com/metamath/set.mm/blob/dde226ae813a3024357bc5b5bccbdda0785c5fe0/mmnatded.raw.html#L277 - but has not been updated on https://us.metamath.org/mpeuni/mmnatded.html yet, presumably due to https://github.com/metamath/metamath-website-scripts/issues/2 concerning website updates.

As for an update to the pdf , that might need to await a new volunteer or a whole lotta patience - the last edition was done by someone who totally doesn't have time for a new project at the moment (if I can be so bold as to say that on his behalf).

As for the "From Td to T" section, first you use https://us.metamath.org/mpeuni/id.html to get !!q -> !!q . Then you expand Td, setting p to !!q so it reads !!q -> !!q |- !!q -> q . This proves T ( !!q -> q ).

As for examples in set.mm, for "From Td to Ti" pretty much any usage of mptru probably is. For "From Td to T", not sure how I'd find one but it would be a section where we define thingd first and then derive a closed-form thing from it.

--
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/dde4ba61-a4fc-4ada-909c-b7c4d7a82076n%40googlegroups.com.

[David A. Wheeler]

> On Aug 15, 2023, at 9:17 AM, Jeroen van Rensen <jeroenv...@gmail.com> wrote:
>
> Hello everyone,
>
> I am reading metamath.pdf and I have a few questions about section 3.9.3 Deduction style, specifically the conversion methods between Td, Ti and T.
>
> T is a statement in closed form (with no hypotheses).
> Td is a statement in deduction form (where all hypotheses are implications with the same antecedent).
> Ti is a statement in inference form (where all hypotheses don't have the same antecedent).
>
> The section states that is is possible to go from Td to Ti, from Td to T and from T to Ti. I have trouble understanding the first two conversions.
>
> Take for example:
> •
> T: !!q -> q
> • Td: p -> !!q |- p -> q
> • Ti: !!q |- q
> From Td to Ti
>
> "To prove some assertion Ti in inference form, given assertion Td in deduction form, there is a simple mechanical process you can use. First take each Ti hypothesis and insert a T. → prefix (“true implies”) using a1i. You can then use the existing assertion Td to prove the resulting conclusion with a T. → prefix. Finally, you can remove that prefix using trud, resulting in the conclusion you wanted to prove."
>
> This is how I understand it:
> •
> Take !!q as a hypothesis
> !!q
> • Add the prefix "T ->" (true implies)
> T -> !!q
> • Use Td to get:
> T -> q
> • Remove the prefix using trud???
> What I don't understand is how you can use trud to go from T -> q to q.
> trud states that for wff q, (q -> T) and not in reverse. Am I missing something here?

Sorry about that! We renamed trud to mptru on Sep 13, 2022.
So you should use mptru instead.

Maybe we should note something in trud.

--- David A. Wheeler

[Jim Kingdon]

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

[Jeroen van Rensen]

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. 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 kin...@panix.com:

[David A. Wheeler]

> On Aug 15, 2023, at 10:15 AM, Jim Kingdon <kin...@panix.com> wrote:
>
> Thanks for saying something. The reference to trud (cited in your "From Td to Ti" section) is supposed to be mptru .
> This has been corrected in git - https://github.com/metamath/set.mm/blob/dde226ae813a3024357bc5b5bccbdda0785c5fe0/mmnatded.raw.html#L277 - but has not been updated on https://us.metamath.org/mpeuni/mmnatded.html yet, presumably due to https://github.com/metamath/metamath-website-scripts/issues/2 concerning website updates.

I expect this to be a temporary situation. I'm working on replacing the scripts with something much simpler that actually completely works. Personal issues have limited the time I've been able to spend on this, but I don't expect it to take too long.

> As for an update to the pdf , that might need to await a new volunteer or a whole lotta patience - the last edition was done by someone who totally doesn't have time for a new project at the moment (if I can be so bold as to say that on his behalf).

I wonder who that could be :-).

It's true I don't have time for a new project at the *moment*, but I think we do eventually need to update the Metamath book. My current plan is to for me to do a mild update, with review by all, and keep Norm's name on the top (since he wrote most of the content). I'm not sure when it'll happen, but I do plan for it to happen eventually.

--- David A. Wheeler

[Marshall Stoner]

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.

[Jim Kingdon]

I'm trying to reduce the pressure on you as best as I am able (given
what you say about personal issues). I totally agree you will solve the
website update problem in due course.

Your plan for the metamath book sounds right to me - I think we should
keep basically the same book with just a few tweaks as needed for things
no longer accurate and the like, rather than try to revisit in any big
way what the scope of the book is. I think you would indeed be the best
person to do it if you are able and willing at some suitable time.

[Thierry Arnoux]

On 15/08/2023 20:40, Jeroen van Rensen wrote:

Hi, and what about when you do have both T and Ti? Do you know how I then should go to Td?

That's the case where you would use the "weak deduction theorem", ~dedth. The comment in dedth has a short explanation, and this is described in more details in https://us.metamath.org/mpeuni/mmdeduction.html.

The first example I found in  set.mm is ~bnd2d, which is derived from bnd2 using this technique.

BR,
_
Thierry

[Jeroen van Rensen]

Thank you! Sorry I just deleted my post because I realized the answer myself.

Op dinsdag 15 augustus 2023 om 20:51:38 UTC+2 schreef Thierry Arnoux:

[Thierry Arnoux]

In practice it's rarely used, as we state the majority of theorems either in closed form or in deduction form, but from a theoretical/learning standpoint it's interesting to know it's possible - and that's why it will be of interest to you!

Actually I see many theorems using it are from the deprecated Hibert Space Explorer (parts 18 and 19).

--

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/3456b89a-4e60-4724-880a-6024b655f5fbn%40googlegroups.com.