Thank you! Op zondag 13 augustus 2023 om 23:41:16 UTC+2 schreef [email protected]:
> axiom a3 is missing parentheses around it > > On Sun, Aug 13, 2023 at 5:30 PM Jeroen van Rensen <[email protected]> > wrote: > >> Hello everyone, >> >> I am trying to prove the following statement: >> >> ! ! p |- p >> >> The formal proof is as follows (the axioms are the same as in set.mm): >> >> 1. ! ! p (Premiss) >> 2. ! ! p -> (! ! ! ! p -> ! ! p) (Axiom 1) >> 3. ! ! ! ! p -> ! ! p (MP 1, 2) >> 4. (! ! ! ! p -> ! ! p) -> (! p -> ! ! ! p) (Axiom 3) >> 5. ! p -> ! ! ! p (MP 3, 4) >> 6. (! p -> ! ! ! p) -> (! ! p -> p) (Axiom 3) >> 7. ! ! p -> p (MP 5, 6) >> 8. p (MP 1, 7) >> >> This is my entire database (irrelevant parts are removed): >> >> ``` >> $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 ) ) ) $. >> a3 $a |- ( ! p -> ! q ) -> ( q -> p ) $. >> >> ${ >> min $e |- p $. >> maj $e |- ( p -> q ) $. >> mp $a |- q $. >> $} >> >> ${ >> dne.1 $e |- ! ! p $. >> dne $p |- p $. >> $} >> ``` >> >> The current proof in the metamath CLI is as follows: >> >> ``` >> 5 min=dne.1 $e |- ! ! p >> 18 min=dne.1 $e |- ! ! p >> 23 maj=a1 $a |- ( ! ! p -> ( $10 -> ! ! p ) ) >> 24 min=mp $a |- ( $10 -> ! ! p ) >> 25 maj=? $? |- ( ( $10 -> ! ! p ) -> $5 ) >> 26 min=mp $a |- $5 >> 27 maj=? $? |- ( $5 -> ( ! ! p -> p ) ) >> 28 maj=mp $a |- ( ! ! p -> p ) >> 29 dne=mp $a |- p >> ``` >> >> I need to assign axiom 3 to line 25 and 27, but when I type `assign 25 >> a3` I get the following error: ?Statement "a3" cannot be unified with step >> 25. >> >> I think the problem is that $10 in line 23 has not yet been resolved. >> >> I hope someone can help me. Thank you! >> >> -- >> 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/8b8e924f-796a-4e5d-bdf7-36fc7fd08cd4n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/8b8e924f-796a-4e5d-bdf7-36fc7fd08cd4n%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/603f2b47-fc98-46ee-8449-7d8c6b92ca70n%40googlegroups.com.
