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 <di.g...@gmail.com> 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 <
> 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/CAFXXJSupJF%2BGspxMtEJwTakCCAAEx%2BPumccTASmmi681k8hmXA%40mail.gmail.com.
