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.
