you have a syntax error in `maj` , it should read |- ( p -> q ) instead of
|- p -> q. With the incorrect statement it won't be able to unify when you
try to apply it.
On Fri, Aug 11, 2023 at 11:45 AM Jeroen van Rensen <
jeroenvanren...@gmail.com> wrote:
> Hello everyone,
>
> I'm new to Metamath and it looks really cool!
>
> I'm trying to prove the following statement (in order to prove p -> p):
>
> |- ( ( p -> ( p -> p ) ) -> ( p -> p ) )
>
> And this is my entire database:
>
> ```
> $c -> ! ( ) wff |- $.
> $v p q r $.
>
> wp $f wff p $.
> wq $f wff q $.
> wr $f wff r $.
>
> wim $a wff ( p -> q ) $.
> wn $a wff ! p $.
>
> a1 $a |- p -> ( q -> p ) $.
> a2 $a |- ( p -> ( q -> r ) ) -> ( ( p -> q ) -> ( p -> r ) ) $.
>
> ${
> min $e |- p $.
> maj $e |- p -> q $.
> mp $a |- q $.
> $}
>
> lem1 $p |- ( ( p -> ( p -> p ) ) -> ( p -> p ) ) $.
> ```
>
> For the proof I use a modus ponens, where the minor part is: p -> ((p ->
> p) -> p), from axiom a1.
>
> The major part I can't get to work. The idea is to use axiom a2,
> substituting p = p, q = p -> p and r = p.
>
> When I try to assign a2 to the right step, I get this message that I don't
> understand:
>
> ```
> MM-PA> assign 6 a2
> ?Statement "a2" cannot be unified with step 6.
> ```
>
> What should I do? How can I substitute a wff (p -> p) for a variable (q)?
>
> --
> 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 metamath+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/23a2913d-c5a1-4c42-a809-5f6dba8aab77n%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/23a2913d-c5a1-4c42-a809-5f6dba8aab77n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsNn_9-h19%2BjWpc6fQ7L4ebf5F-TR%2Bi%2BMwGoRCH95%2BF4g%40mail.gmail.com.
