Friday, February 13, 2015

No More Free Variables (for now)

Formerly, would accept statements with free variables.  It would bind them all with existential quantifiers.  That seemed to work; it yielded the results I expected for all of the statements I had tried - up until a few days ago, when I found it to fail for some statements.  One such statement is "a=b".  I would expect this to be a contingent statement; true or false depending on whether or not a and b denoted the same object, but the application decided it to be necessarily true.  It's not hard to see why if we expand the statement, as the application does, to be "3b,3a,a=b". There is always an a and a b which are identical in any nonempty universe; they are identical when they are the same object.

So, for now, the application rejects statements that contain free variables.  I'm working on finding a way to decide them correctly.  As soon as I've found one (and I've assured myself that it really is correct), I'll incorporate it into the application and allow free variables once again.

No comments: