# Definition:Provable Consequence

## Definition

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

Let $\mathcal F$ be a collection of WFFs of $\mathcal L$.

Denote with $\mathscr P \left({\mathcal F}\right)$ the proof system obtained from $\mathscr P$ by adding all the WFFs from $\mathcal F$ as axioms.

Let $\phi$ be a theorem of $\mathscr P \left({\mathcal F}\right)$.

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

- $\mathcal F \vdash_{\mathscr P} \phi$

Note in particular that for $\mathcal F = \varnothing$, 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:

**$\mathcal F$ proves $\phi$****$\phi$ is provable from $\mathcal F$**

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

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

## Also see

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.3.2$: Definition $3.12$