Meaning of Provability Symbol ⊢ in Axiomatic Programming Paper [closed]

Question

Closed. This question is off-topic. It is not currently accepting answers.

---

Want to improve this question? Update the question so it's on-topic for Stack Overflow.

Closed 9 years ago.

Improve this question

I'm reading "An Axiomatic Basis for Computer Programming." They use the provability symbol ⊢ in their axioms, e.g.

⊢P {Q} R

Wikipedia describes the use of that symbol as such "x ⊢ y means y is provable from x (in some specified formal system)," but that doesn't seem to fit here. What does the symbol mean?

The paper can be found here: http://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf

Answer 1

In x ⊢ y, x is a set of assumptions, and y is a statement (in the logical system or language you're talking about). "x ⊢ y" says that, in the logical system, if you start with the assumptions x, you can prove the statement y.

Because x is a set, it can also be the empty set. Often this is written with the empty set symbol, as ∅ ⊢ y, but sometimes for brevity it is left out completely, which is what's going on here. Being able to prove it from the empty set of assumptions means that it is just true (or valid). For example, ⊢ p → p.

Hoare's paper talks about a language for describing the behaviour of programs. As Todd points out, "P {Q} R" is (in this language) the statement that, if you run program Q in an initial state where P is true, then R will be true afterwards (iff Q terminates). This is the kind of statement you might want to prove using some assumptions. These assumptions would be things at a higher level than the initial state: for example, if you've already proven a simpler but related P' {Q'} R' statement, you might want to assume it to prove the bigger P {Q} R statement.

Thus "⊢ P {Q} R" says that the statement "P {Q} R" is true, and you don't need to assume anything.

Let's take a stupidly simple example.

⊢ x = 3 {y := x} x = 3 ∧ y = 3

The statement we're proving is: "If x is 3 at the start, and you run the program y := x, then afterwards x will be 3 and y will be 3." You don't need any assumptions to prove this, it follows from the definition of the language. You could go ahead and use this fact as an assumption to prove something else.

x = 3 {y := x} x = 3 ∧ y = 3 ⊢ x = 3 {y := x; z := y} x = 3 ∧ y = 3 ∧ z = 3

Here we've used the simpler statement on the left as an assumption to prove a bigger statement. It's a very silly example, but I hope it shows how to read this. I've made the ⊢ bold to show it is the "top-level" thing in the line, separating the assumptions from the conclusion. Both the left-hand and right-hand sides are statements in Hoare's logic, with P {Q} R, where P and R are logical statements and Q is a program.

Answer 2

⊢P {Q} R

is saying that "P is a precondition for a program Q to produce result R"