<div dir="ltr"><div>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:<br><br><span style="font-family:courier new,monospace">877::assume                     [p] |- p<br>1447:843,1444:eqMp              [(p ==> q)] |- (p = (p /\ q))<br>1450:877,1447:eqMp              [p, (p ==> q)] |- (p /\ q)<br>1624:1621:subst                 [(p /\ q)] |- q<br>1627:1450,1624:deductAntisym    [p, (p ==> q)] |- ((p /\ q) = q)<br>1630:1450,1627:eqMp             [p, (p ==> q)] |- q<br>9849:698:subst                  [] |- ((((! \x. ((P x) ==> Q)) /\ ((? P) ==> Q)) = (! \x. ((P x) ==> Q))) = ((! \x. ((P x) ==> Q)) ==> ((? P) ==> Q)))<br>10205:10187,10204:deductAntisym [] |- (((! \x. ((P x) ==> Q)) /\ ((? P) ==> Q)) = (! \x. ((P x) ==> Q)))<br>10206:10205,9849:eqMp           [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==> Q))<br>16595:10206:subst               [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==> Q))<br>16959:16595:subst               [] |- ((! \x50. ((\y. (x p y) x50) ==> (? \y. (? \x. (x p y))))) ==> ((? \y. (x p y)) ==> (? \y. (? \x. (x p y)))))<br>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))))<br>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)))))<br></span><br></div>(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<br><br><span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">\x50. ((\y. (x p y) x50) ==> (? \y. (? \x. (x p y))))</span></span></span></span><div><span style="font-family:courier new,monospace"><span style="font-family:courier new,monospace">\x. ((\y. (x p y) x) ==> (? 
\y. (? \x. (x p y))))</span><br><br></span>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?<br><br></div><div>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.<br></div><div><br></div><div>Mario<br></div></div>