# 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$

## Also defined as

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

For example, the tableau proof system based on propositional tableaus.

## Also known as

One also encounters phrases like:

**$\FF$ proves $\phi$****$\phi$ is provable from $\FF$**

to describe the concept of **provable consequence**.

A **provable consequence** is also known as a **derivable formula** or a **provable formula**.

## Also see

- Definition:Premise, one can view $\FF$ as the premises used to prove $\phi$

## Sources

- 1998: David Nelson:
*The Penguin Dictionary of Mathematics*(2nd ed.) ... (previous) ... (next):**consequence**:**1.**(**logical consequence**) - 2009: Kenneth Kunen:
*The Foundations of Mathematics*... (previous) ... (next): $\text{II}.10$ Formal Proofs: Definition $\text{II}.10.4$ - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.3.2$: Definition $3.12$