Solved it, thank you! Op vrijdag 11 augustus 2023 om 17:48:51 UTC+2 schreef [email protected]:
> Actually you have the same syntax error in a1 and a2, the outermost > implication should be surrounded in parentheses. Since you declared the > implication symbol with parentheses around it they are required for any > implication and cannot be omitted. > > On Fri, Aug 11, 2023 at 11:47 AM Mario Carneiro <[email protected]> wrote: > >> 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 <[email protected]> >> 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 [email protected]. >>> 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9f8a8623-0a16-4326-9b87-2967cf99c234n%40googlegroups.com.
