Funny, coincidentally I recently read a paper [0] arguing (among other things) that truth values should be completely removed--that for software engineering they are largely useless and cause mistakes.
The argument goes that a True False value will "mean" different things in a context, but then when trying to model a complex entity there are inevitably leakages of definitions.
For formal verification of existing Boolean logic, however, it reasons that "verifying" our truth values would be very helpful, by exploring and modeling the state space that is made up by the composition of multiple booleans. This is very interesting in that regard!
[0]: Formalizing common sense reasoning for scalable inconsistency-robust information integration using Direct Logic Reasoning and the Actor Model, Carl Hewitt. https://arxiv.org/pdf/0812.4852.pdf
> The argument goes that a True False value will "mean" different things in a context
Well, it is the same with numbers anytime they mean something in the real world. One would have to add "unit types" to numbers and check that x + y causes a type error when a "nr. of humans" is added to a "nr. of rainy days", to give an example. If that is represented by adding two integers there won't be an error. In software comparing apples and oranges works fine as long as you use numbers...
Database generated IDs are a great example. We often use integers because it is convenient - but there's no reason you should be able to add two together.
Yeah, but type systems are not fool proof. eg: I've seen plenty of Java code which blindly passes String objects around that eventually get parsed into json/int/long/etc. At that point, the type system has been silently circumvented.
"Nothing is foolproof given a sufficiently talented fool."
> CNF we would not say the Englishman lives in the red house we would say either the owner of the house is NOT the Englishman OR the house is red (which effectively means the same thing).
Effectively, maybe. Somebody might object that those two clauses (NOT the Englishman OR the house is red) can't be satisfied both at the same time - because not only the Englishman lives in the red house, also nobody else also lives there. So it's also true "NOT the Englishman IMPLIES the house is NOT red", "house is NOT red IMPLIES NOT the Englishman", neither of which is derivable from the original clause (CNF allows regular, "mathematical" understanding).
The argument goes that a True False value will "mean" different things in a context, but then when trying to model a complex entity there are inevitably leakages of definitions.
For formal verification of existing Boolean logic, however, it reasons that "verifying" our truth values would be very helpful, by exploring and modeling the state space that is made up by the composition of multiple booleans. This is very interesting in that regard!
[0]: Formalizing common sense reasoning for scalable inconsistency-robust information integration using Direct Logic Reasoning and the Actor Model, Carl Hewitt. https://arxiv.org/pdf/0812.4852.pdf