On Thursday, 7 August 2014 at 07:53:44 UTC, Ola Fosheim Grøstad
wrote:
On Thursday, 7 August 2014 at 06:04:38 UTC, David Bregman wrote:
On Thursday, 7 August 2014 at 03:54:12 UTC, Ola Fosheim
Grøstad wrote:
«The __assume(0) statement is a special case.»
So, it does not make perfect sense. If it did, it would not
be a special case?
It doesn't have to be a special case if you define it in the
right way - in terms of control flow. Then the interpretation
of assume(false) as unreachable follows quite naturally:
instead of defining assume(x) to mean that x is an axiom,
define assume(x) to mean that P=>x is an axiom, where P is the
proposition that control flow reaches the assume statement.
so assume(false) actually means P=>false, or simply !P
and !P means !(control flow reaches the assume), as desired.
Let's try the opposite way instead:
assume(Q)
if(B1){
if(B2){
}
}
implies:
assume(Q)
if(B1){
assume(B1&&Q)
if(B2){
assume(B1&&B2&&Q)
}
}
So your P in the inner if statement is B1&&B2.
However assume(P&&false) is still a fallacy…
Or?
If you use the definition of assume that I gave, assume(P &&
false) declares the axiom
P => (P && false)
which is again equivalent to !P.
