Informal proof of Weak Deduction Theorem vs dedt

[Gustavo Gonçalves]

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!

[Mario Carneiro]

On Mon, Mar 15, 2021 at 2:13 PM Gustavo Gonçalves <gusg...@gmail.com> wrote:

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).

It's a nontrivial property that does not come for free, at least the way set.mm is set up. It follows by induction provided that every term constructor satisfies the property, but as you point out there are quite a lot of term constructors in set.mm, most of which are definitions. For definitions, to make progress we expand the definition into an expression that does not contain the definition using the definitional axiom. This requires that the definitional axiom be stated in a very particular way, that is checked by mmj2's definition checker, to ensure that this is always possible.

So the overall method is this: we can prove the equality theorem for each individual term constructor (these are *eqd theorems) in a mechanically generated way based on the definition itself, which reduces the problem to the term constructors that have no definition, aka primitive constructors. In set.mm the primitive constructors are:

* negation: -. ph
* implication: ( ph -> ps )

* forall: A. x ph

* class abstraction: { x | ph }

* equality for classes: A = B

* elementhood for classes: A e. B

The equality theorems for these constructors are respectively: notbid, imbi12d, albidv, abbidv, eqeq12d, eleq12d. Should another primitive term constructor be added, we would need to also add an axiom to ensure that it also satisfies equality, like ax-9.

 

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:

⊢ ((𝜑 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜃 ↔ 𝜏))

As an aside, it's much simpler to look at dedth instead, which uses an explicit "if" expression instead of a combination of logical operators. I think there were some plans to add "ifp" to set.mm but I guess it didn't make it into the statement of this theorem.

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)))

Actually, in the language of the proof on that page, I believe that it is supposed to correspond to

⊢ ((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (G(A) ↔ G((A ∧ F) ∨ (B ∧ ¬ F)))),

that is, step (10). This is the part of the proof that needs to be supplied externally, i.e. via a hypothesis to dedt, because it is an instance of the meta-theorem |- ((A <-> B) -> (G(A) <-> G(B)) where we take B to be ((A ∧ F) ∨ (B ∧ ¬ F)).

Tthe other assumption is step (9), which is intended to be proven using the |- F ==> |- G meta-assumption. That is, |- G((A ∧ F) ∨ (B ∧ ¬ F)) follows from |- F((A ∧ F) ∨ (B ∧ ¬ F)) by the meta-assumption. To prove this, there is one more key lemma, elimh:

((𝜑 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜒 ↔ 𝜏)),
((𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜃 ↔ 𝜏)),
𝜃

⊢ 𝜏

 

which we can substitute in the current setting to:

((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),
((B ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),
F(B)

⊢ F((A ∧ F) ∨ (B ∧ ¬ F))

The first two hypotheses are clearly instances of the substitution metatheorem, and the third assumption is a hypothesis: |- F(B) is provable by assumption, so |- F((A ∧ F) ∨ (B ∧ ¬ F)) and hence |- G((A ∧ F) ∨ (B ∧ ¬ F)) as desired.

Mario Carneiro

[Mario Carneiro]

On Mon, Mar 15, 2021 at 3:02 PM Mario Carneiro <di....@gmail.com> wrote:

which we can substitute in the current setting to:

((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),
((B ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),
F(B)

⊢ F((A ∧ F) ∨ (B ∧ ¬ F))

Amendment:

((A ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(A) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),

((B ↔ ((A ∧ F) ∨ (B ∧ ¬ F))) → (F(B) ↔ F((A ∧ F) ∨ (B ∧ ¬ F)))),
F(B)

⊢ F((A ∧ F) ∨ (B ∧ ¬ F))

 

[Benoit]

On Monday, March 15, 2021 at 8:02:23 PM UTC+1 di....@gmail.com wrote:

As an aside, it's much simpler to look at dedth instead, which uses an explicit "if" expression instead of a combination of logical operators. I think there were some plans to add "ifp" to set.mm but I guess it didn't make it into the statement of this theorem.

It is currently http://us.metamath.org/mpeuni/bj-dedthm.html

I'd be happy to move it to Main.

Benoît

[Norman Megill]

On Monday, March 15, 2021 at 4:36:39 PM UTC-4 Benoit wrote:

On Monday, March 15, 2021 at 8:02:23 PM UTC+1 di.... wrote:

As an aside, it's much simpler to look at dedth instead, which uses an explicit "if" expression instead of a combination of logical operators. I think there were some plans to add "ifp" to set.mm but I guess it didn't make it into the statement of this theorem.

It is currently http://us.metamath.org/mpeuni/bj-dedthm.html

I'd be happy to move it to Main.

 

I think you should go ahead and move it there.  Maybe we should replace the (very confusing) con3th proof with your bj-con3thALT and update the mmdeduction.html page accordingly.

Off and on I've been playing with some weak deduction theorem ideas in my mathbox.  dedths + elimhyps provide a very compact statement of the w.d.t. using explicit substitution notation.  Unfortunately proofs using it can be significantly longer - compare renegclALT to renegcl.  (Longer proofs seem to be a general characteristic of proofs involving explicit substitutions, which is why we almost always use implicit substitutions, i.e. substitutions implied by hypotheses like |- ( x = y -> ( ph <-> ps ) ) in cbvalv.)

Another experiment was deriving the deduction form http://us2.metamath.org/mpeuni/nfunidALT.html directly from the inference form nfuni.  This didn't use the w.d.t. as we usually state it;  I was exploring possible alternatives to w.d.t. that might provide shorter proofs.  In this case, the proof of nfunidALT from nfuni ends up being slightly shorter than the proof of nfunid, which starts from a definition of union and also requires that the deduction form for the definition pieces already be proved.

Norm