Proof shows a correct completion status with an open subproof

Question

Proof shows a correct completion status with an open subproof

Closed this issue 6 years ago · 2 comments

Here is an illustration of the problem:

Answer 1 · 2018-12-04T20:30:41.000Z

I think what's going on is that the proof checker looks if the conclusion occurs in the proof on the main scope line. In your case it does -- it's the first premise. (Probably a typo; you wanted the conclusion to be Ex Gx not Ex Fx?). So this is not a bug, unless I misunderstand something.

Answer 2 · 2018-12-04T22:42:30.000Z

Richard is correct. As strange as it seems, this is all intended behavior. It is marked as correct because the conclusion is found in the main proof at line 1. You could have a one-line proof if the conclusion was the premise.

It never marks things wrong for having extra unnecessary steps, even extra unnecessary subproofs. It is interpreting lines 3 and 4 as a complete, albeit unnecessary and unused subproof, which it is.

A case could be made that it should not allow extra unused lines or subproofs at the end, just for clarity's sake, but my own inclination is to leave things consistent.