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.
On 8/15/23 06:17, Jeroen van Rensen 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:
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!
--
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/dde4ba61-a4fc-4ada-909c-b7c4d7a82076n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/dde4ba61-a4fc-4ada-909c-b7c4d7a82076n%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/31103853-b814-f33f-7704-d9ef038a0bb4%40panix.com.
