> On Aug 15, 2023, at 9:17 AM, Jeroen van Rensen <[email protected]>
> 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
--
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/4522FE76-8345-4DE9-A7D3-59D02A6FC0BC%40dwheeler.com.
