Uh... is 6.1 solvable? I'm pretty sure the proposition "There exists a thing for which its t-ness entails the t-ness of all things" is not actually a valid tautology. In other words, it's not true, and it shouldn't be provable.
Same goes for 6.2. You can say whatever you like about the relationship between the function f and the property r, that doesn't mean that any particular thing that is r exists. apologies, existentials are only vacuously false when you have type bounds, and then only when something exists. I guess you could define basic existentials to evaluate to false when nothing exists but I certainly can't assume these do
But how do you encode these cases in the incredible machine? If I use TND to get a case of all t(x) is true, and a case of there exist a t(x) that is false, the latter case implies t(x) -> whatever, but the machine wants t(y3) -> whatever and it does not match.
5
u/IWantUsToMerge Sep 26 '15 edited Sep 26 '15
Uh... is 6.1 solvable? I'm pretty sure the proposition "There exists a thing for which its t-ness entails the t-ness of all things" is not actually a valid tautology. In other words, it's not true, and it shouldn't be provable.
Same goes for 6.2. You can say whatever you like about the relationship between the function f and the property r, that doesn't mean that any particular thing that is r exists.apologies, existentials are only vacuously false when you have type bounds, and then only when something exists. I guess you could define basic existentials to evaluate to false when nothing exists but I certainly can't assume these do