Provability is a relationship between formulae, or sets of formulae, which states that, given some logical system, some formulae φ can be proved from some set of formulae Γ.
The turnstile symbol ( ⊢ ) is used to indicate the relationship of provability. Formally, we say that:
Γ ⊢ φ
This means that, from the set of formulae Γ, we can prove that φ is true.
For example, we can say that the validity of the argument form modus tollens is provable in a system of classical logic by:
P → Q, ¬Q ⊢ ¬P
In order to establish that this form is indeed provable, we must construct a proof. The following proof uses the rules of inference of natural deduction in order to determine that modus tollens of provable:
Although it may not seem obvious that provability ( ⊢ ) is different from logical implication ( 
), the two indicate a seperate sort of relationship. To say that φ is provable from Γ is to say that one can construct a proof which demonstrates that, using the information present in Γ, we can syntactically derive φ.
On the other hand, to say that Γ implies φ, or Γ φ, is to say that φ logically follows from Γ—that no semantic interpretation (or valuation) makes all of the members of Γ true and φ false.
Highly desirable systems of logic are both sound, meaning that anything provable in the system actually follows, and complete, meaning that everything that follows in the system is actually provable. In a system that is sound and complete, whenever it is the case that Γ ⊢ φ, then Γ φ, and vice-versa.
However, there are logical systems that are unsound, incomplete, or both, meaning that in these systems, some statements can be proven even though they don’t logically follow, and some things logically follow even though we cannot prove them in that system. For this reason it is important to maintain the difference between provability and actual implication.
