Definition:Provable Consequence

This page is about provable consequence in the context of proof systems. For other uses, see consequence.

Definition

Let $\mathscr P$ be a proof system for a formal language $\LL$.

Let $\FF$ be a collection of WFFs of $\LL$.

Denote with $\map {\mathscr P} \FF$ the proof system obtained from $\mathscr P$ by adding all the WFFs from $\FF$ as axioms.

Let $\phi$ be a theorem of $\map {\mathscr P} \FF$.

Then $\phi$ is called a provable consequence of $\FF$, and this is denoted as:

$\FF \vdash_{\mathscr P} \phi$

Note in particular that for $\FF = \O$, this notation agrees with the notation for a $\mathscr P$-theorem:

$\vdash_{\mathscr P} \phi$

While this definition of provable consequence is adequate for most proof systems, it is more natural for some of them to define provable consequence in a different way.

One also encounters phrases like:

to describe the concept of provable consequence.

A provable consequence is also known as:

a derivable formula

a provable formula

a logical consequence, but this is mainly used more generally in the context of logical implication.