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.<p>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.<p>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!<p>[0]: Formalizing common sense reasoning for scalable inconsistency-robust information integration using Direct Logic Reasoning and the Actor Model, Carl Hewitt. <a href="https://arxiv.org/pdf/0812.4852.pdf" rel="nofollow">https://arxiv.org/pdf/0812.4852.pdf</a>
> 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).<p>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).
Now, here's a great read. Loved it. I've used tla+ ... I'll give alloy a try too. I'm interested in anything else along these lines.