On Mon, Mar 15, 2021 at 2:13 PM Gustavo Gonçalves <[email protected]>
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
--
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/CAFXXJSvztGhjns40WESW-WfKMYDYEWrf3nQEoWnsH1rCSboEuA%40mail.gmail.com.
