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/CAFXXJSsen3M%2Bwd_zxOeHK5AC5NoTHH09mMxc19E0iq_mqkYzLA%40mail.gmail.com.
