On Wednesday, 6 August 2014 at 19:18:30 UTC, Marc Schütz wrote:
Assume(P) defines that the proposition holds. If it does not
involve variables, then it will be free to move anywhere by
the rules of Hoare-logic (and propositional logic)? If
assume(PI==3.14…) can move everywhere, by the rules, then so
can assume(true==false).
See above. Of course we could define our `assume(P)` to define
`P` as an axiom directly, but this would be much less useful,
because it would have exactly the consequences you write about.
And it would be a lot more consistent, too. Surely you wouldn't
want `assume(x == 42)` to mean "x is always and everywhere
equal to 42", but just "x is equal to 42 when control flow
passes this point".
This is unclear. What I wanted to write is: "It would be more
consistent to use the definition of `assume` that I propose.".
