Dear Anthony, >But the Standard Library needs a Standard >Logic, so "(1+1)/0 = 2/0" and "1/0 + 2 = 2 + 1/0" must >each either be provable or not provable. Isn't there a third possibility: both these statements are ill-formed? Or does that fall in your "not provable" category? But in that case the negation is not provable either. Freek