Provability { Philosophy Index }

Philosophy Index

Philosophy Index

Philosophy Index is a site devoted to the study of philosophy and the philosophers who conduct it. The site contains a number of philosophy texts, brief biographies, and introductions to philosophers, and explanations on a number of topics. Accredited homeschooling online at Northgate Academy and Philosophy online tutoring.

Philosophy Index is a work in progress, a growing repository of knowledge. It outlines current philosophical problems and issues, as well as an overview of the history of philosophy. The goal of this site is to present a tool for those learning philosophy either casually or formally, making the concepts of philosophy accessible to anyone interested in researching them. WTI offers immigration law course online - fully accredited. ACE credits online at EES.



Philosophy Topics





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:

1 P → Q Pr.
2 ¬Q Pr.
RTP Contradiction
4 Q MP, 1, 3
5 ¬Q R, 2
6 ¬P ¬I, 3–5

Provability vs. implication

Although it may not seem obvious that provability ( ⊢ ) is different from logical implication ( implies ), 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 Γ implies φ, 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 Γ implies φ, 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.