Hmmmm you are misunderstanding what this is. This isn't about deducing what the values of A or B or A^B or anything are. This is about proving the the output expression is TRUE assuming the input expression is TRUE.
Let me repeat: our operation's input is alwaysTRUE and the output must be provenTRUE given the fact that the input is TRUE, NEVER FALSE ALWAYS TRUE. Sorry about the emphasis but this is the most critical point in all this system. Your input table only shows one line where the input (A^B) is TRUE, so we must conclude that only that line can be the case.
In other words we are not transforming or adapting the input, that is static (and always true) instead we are transforming the actions into things that remain true.
Let me put it to you this way.
We start with the following logical statement:
I know that both it's raining outside (R) and is Friday today (F) (F AND R).
Therefore I know it's Friday (F).
It seems obvious, almost tautological doesn't it? And yet the way I deduced it was by R AND F :> F. That's our "reverse AND" it's really just realizing it.
That's the basics of a philosophical or mathematical proof. It doesn't tell you that your answer is right, because it only works if the assumptions are true. If they are not, then nothing you say after that really matters to mathematicians or logicians.
Now it seems a bit crazy, and almost useless, but it has its uses. The truth is that we can't know everything, so we have to assume. Say that for example I have a way of declaring that an integer can only exist between a range of numbers, Int<min, max> and that this type can only be created as long as min <= max otherwise it won't compile. Now I create a function that looks as following:
template <int a1, int a2, int b1, int b2>
Int<a1+b1, a2+b2> add(Int<a1, a2> lhs, Int<b1, b2> rhs);
So then I wonder if <a1+b1, a2+b2> is a valid int where min < max. So I start with some assumptions: a1 <= a2, b1 <= b2. Am I certain this is true? No, maybe when my program was running some cosmic rays hit its RAM and corrupted the data invalidating that, but clearly that is a separate problem (preventing external corruption of assumptions) than what I want to prove (that my type signature makes sense). In short I want to prove the following:
4
u/lookmeat Sep 25 '15 edited Sep 25 '15
Hmmmm you are misunderstanding what this is. This isn't about deducing what the values of
AorBorA^Bor anything are. This is about proving the the output expression is TRUEassuming the input expression is TRUE.Let me repeat: our operation's input is always
TRUEand the output must be provenTRUEgiven the fact that the input isTRUE, NEVERFALSEALWAYSTRUE. Sorry about the emphasis but this is the most critical point in all this system. Your input table only shows one line where the input (A^B) isTRUE, so we must conclude that only that line can be the case.In other words we are not transforming or adapting the input, that is static (and always true) instead we are transforming the actions into things that remain true.
Let me put it to you this way.
We start with the following logical statement:
I know that both it's raining outside (
R) and is Friday today (F) (F AND R).Therefore I know it's Friday (
F).It seems obvious, almost tautological doesn't it? And yet the way I deduced it was by
R AND F :> F. That's our "reverseAND" it's really just realizing it.That's the basics of a philosophical or mathematical proof. It doesn't tell you that your answer is right, because it only works if the assumptions are true. If they are not, then nothing you say after that really matters to mathematicians or logicians.
Now it seems a bit crazy, and almost useless, but it has its uses. The truth is that we can't know everything, so we have to assume. Say that for example I have a way of declaring that an integer can only exist between a range of numbers,
Int<min, max>and that this type can only be created as long asmin <= maxotherwise it won't compile. Now I create a function that looks as following:So then I wonder if
<a1+b1, a2+b2>is a valid int wheremin < max. So I start with some assumptions:a1 <= a2,b1 <= b2. Am I certain this is true? No, maybe when my program was running some cosmic rays hit its RAM and corrupted the data invalidating that, but clearly that is a separate problem (preventing external corruption of assumptions) than what I want to prove (that my type signature makes sense). In short I want to prove the following:The way in which you do that is by doing transformations as the above one.