Hi!
I started my quest towards IMO 1972 B2 by formalizing a simple
induction problem (just for fun): `( N e. NN -> 3 || ( ( 4 ^ N ) + 5 )
)`[0] and made some good progress towards demonstrating the following
lemma:
```
imo72b2lem.1 |- ( ph -> F : RR --> RR )
imo72b2lem.2 |- ( ph -> G : RR --> RR )
imo72b2lem.3 |- ( ph -> A e. RR )
imo72b2lem.4 |- ( ph -> B e. RR )
imo72b2lem.5 |- ( ph -> ( ( F ` ( A + B ) ) +
( F ` ( A - B ) ) ) =
( 2 x. ( ( F ` A ) x. ( G ` B ) ) ) )
imo72b2lem.6 |- ( ph -> A. x e. RR ( abs ` ( F ` x ) ) <_ 1 )
imo72b2lem |- ( ph -> ( ( abs ` ( F ` A ) ) x.
( abs ` ( G ` B ) ) )
<_ sup ( ( abs " ( F " RR ) )
, RR , < ) )
```
One thing I'm stuck on is the following: In a natural deduction
setting, how does one demonstrate an existence assuming a witness?
Basically, in order to be able to work with the `sup ( ( abs " ( F "
RR ) ) , RR , < )`, I want to go from `imo72b2lem.6` to:
```
|- ( ph -> E. c e. RR A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```
>From natded[1] the starting point seems to consist in applying
spesbcd[2], but I'm unclear on how to breach the difference between
`E. c ph` and `E. c e. A ph` as it does not seem to exist an
equivalent for the latter? Even assuming this problem solved, I'm also
at a loss attempting to prove the following given `imo72b2lem.6`:
```
|- ( ph -> [. 1 / c ]. A. x e. RR ( abs ` ( F ` x ) ) <_ c )
```
Thank you very much for your help on this!
-stan
[0]
https://github.com/spolu/set.mm/commit/c82772aadfe13d17c722b0724526a3a72d79864c#diff-12dc1484b058d1ee6cb68a74194d66c7R641305
[1] http://us.metamath.org/mpeuni/natded.html
[2] http://us.metamath.org/mpeuni/spesbcd.html
On Fri, Feb 28, 2020 at 5:17 PM Benoit <[email protected]> wrote:
>
> > One question for which I'm looking guidance is on using quantifiers or not.
>
> That's a very important question, and I hope someone with more experience
> will be able to shed some insight. In particular, if one has a hypothesis,
> say, "E. x ph", then it is common to see in textbooks things like "Let y be
> such that ph(y). Then [subproof], so [conclusion which does not depend on y].
> Therefore, [that conclusion]." I would formalize it in set.mm by using the
> "deduction style" and prepending "[. y / x ]. ph" as an antecedent to each
> line of the subproof. Maybe there are better strategies ?
>
> > As an example, I believe the following are all valid but presumably
> > drastically influence the proof strategy?
> > $e |- ( ph -> -. A. z e. RR ( F ` z ) = 0 ) $.
> > $e |- ( ph -> E. z e. RR ( F ` z ) =/= 0 ) $.
> > $e |- ( ph -> C e. RR ) $. $e |- ( 0 < ( abs ` ( F ` C ) ) ) $.
> > $e |- ( ph -> C e. RR ) $. $e |- ( ( F ` C ) =/= 0 ) $.
>
> I believe the first version (the one I used) is closest to what we mean by "F
> is not identically 0". The equivalence (in classical logic) with the second
> version is direct, using ~rexnal. I think it would be easier but "cheating"
> to use the third or fourth version (see above).
>
> Benoît
>
> --
> 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/957b9c68-04bf-414b-8149-07d0801ca962%40googlegroups.com.
--
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/CACZd_0zP3JcM75txu%3DuzyW4g1h9KT%3DNhw4%2BsgRDickqc53dmmg%40mail.gmail.com.
