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.
