Hello! I found out about metamath a few weeks ago and I am astounded about how much we can derive in propositional logic using only ax1 ax2 ax3 and ax-mp
I did eventually learn about how we can't assume [ |- P => |- Q ] => |- (P -> Q) And so I began my journey to understand the deduction theorem until I found the informal proof of the Weak Deduction Theorem. http://us.metamath.org/mpeuni/mmdeduction.html#proof Throughout my journey, I hit two questions that I can't answer by myself. I agree with the entirety of the proof except of this one step (that appeared twice): if A and B are wff that can be contained in F (another wff) so that we can write F(A) and F(B) |- (P -> (A <-> B)) => |- (P -> (F(A) <-> F(B)) It described that we can infer that's true by deriving "by induction on the formula length of F", which I intuitively understand but formally I don't see how it can be proved. I tested it with F(A) = A, F(A) = ¬A, F(A) = (A -> X) and F(A) = (X -> A) (where X can be any wff) By these four tests, we can create any F using ¬ and -> recursively. But once we start using set theory axioms and definitions and expanding to other branches of maths, are we going to have to test F for every new definition? (that is my first question). Once I eventually agree with the informal proof, I am having trouble to relate the informal proof with dedt: http://us.metamath.org/mpeuni/dedt.html which states: ⊢ ((𝜑 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜃 ↔ 𝜏)) The best way I can write that in terms of F, G, A and B is: ⊢ ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F(A)))) → (G(A) ↔ F(B))) The left hand side of this conditional Is pretty much identical to the right hand side of the conditional in line (1) of the informal proof. But I don't seem to understand why the left side implies the equivalence between G(A) and F(B). I know that it's a given that F(B) is true, so by axiom 1, this is clearly true: |- F(B) => |- (G(A) → F(B)) => |- ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F(A)))) → (G(A) → F(B))) But if we want that equivalence, we need to also prove this: |- ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F(A)))) → ( F(B) → G(A) )) (that would be my second question) Thank you very much for reading, I am really astounded by Metamath's library of theorems and its approach to mathematical proofs! -- 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/f7f7e444-d6fa-4b45-81f6-10bfe7c2d74bn%40googlegroups.com.
