[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

I'm working on an article reader for Java, and the current error I'm seeing
doesn't make sense compared to the spec. That is, my test file,
bool-int.art, shouldn't be valid, although I assume it is. The relevant
lines from the output are:

877::assume                     [p] |- p
1447:843,1444:eqMp              [(p ==> q)] |- (p = (p /\ q))
1450:877,1447:eqMp              [p, (p ==> q)] |- (p /\ q)
1624:1621:subst                 [(p /\ q)] |- q
1627:1450,1624:deductAntisym    [p, (p ==> q)] |- ((p /\ q) = q)
1630:1450,1627:eqMp             [p, (p ==> q)] |- q
9849:698:subst                  [] |- ((((! \x. ((P x) ==> Q)) /\ ((? P)
==> Q)) = (! \x. ((P x) ==> Q))) = ((! \x. ((P x) ==> Q)) ==> ((? P) ==>
Q)))
10205:10187,10204:deductAntisym [] |- (((! \x. ((P x) ==> Q)) /\ ((? P) ==>
Q)) = (! \x. ((P x) ==> Q)))
10206:10205,9849:eqMp           [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==>
Q))
16595:10206:subst               [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==>
Q))
16959:16595:subst               [] |- ((! \x50. ((\y. (x p y) x50) ==> (?
\y. (? \x. (x p y))))) ==> ((? \y. (x p y)) ==> (? \y. (? \x. (x p y)))))
17006:1630:subst                [(! \x. ((\y. (x p y) x) ==> (? \y. (? \x.
(x p y))))), ((! \x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))) ==> ((?
\y. (x p y)) ==> (? \y. (? \x. (x p y)))))] |- ((? \y. (x p y)) ==> (? \y.
(? \x. (x p y))))
17007:16959,17006:deductAntisym [(! \x. ((\y. (x p y) x) ==> (? \y. (? \x.
(x p y))))), ((! \x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))) ==> ((?
\y. (x p y)) ==> (? \y. (? \x. (x p y)))))] |- (((! \x50. ((\y. (x p y)
x50) ==> (? \y. (? \x. (x p y))))) ==> ((? \y. (x p y)) ==> (? \y. (? \x.
(x p y))))) = ((? \y. (x p y)) ==> (? \y. (? \x. (x p y)))))

(The output format shows all theorem-creating steps, labeled by the line in
the file they first appeared, and the theorems they depend on.) I've
trimmed the output just to show the direct ancestors of step 17007, which I
think is incorrect, because the second hypothesis should have been
eliminated but wasn't because the terms

\x50. ((\y. (x p y) x50) ==> (? \y. (? \x. (x p y))))
\x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))

are not alpha-equivalent. The other candidate for the error is step 16959,
where we do the substitution P -> \y. (x p y) and Q -> (? \y. (? \x. (x p
y))) into \x. ((P x) ==> Q), but since x is bound in the original term and
free in P, in accordance with the spec I swap out x -> x50 before doing the
substitution. Is this wrong?

If there are any readers written in an imperative language, that would also
make a good reference. Unfortunately the functional PL examples are
different enough in structure that I have difficulty mentally mapping the
algorithm from one language to another.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141012/51c5ec2d/attachment.html>