?Statement "a3" cannot be unified with step 25.

[Jeroen van Rensen]

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!

[Mario Carneiro]

axiom a3 is missing parentheses around it

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8b8e924f-796a-4e5d-bdf7-36fc7fd08cd4n%40googlegroups.com.

[Jeroen van Rensen]

Thank you!

Op zondag 13 augustus 2023 om 23:41:16 UTC+2 schreef di....@gmail.com: