# Definition:Theory

## Definition

Let $\LL$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\LL$.

Let $\FF$ be a set of $\LL$-formulas.

Then $\FF$ is an **$\LL$-theory** if and only if, for every $\phi \in \LL$:

- $\FF \models_{\mathscr M} \phi \implies \phi \in \FF$

where $\models_{\mathscr M}$ denotes $\mathscr M$-semantic consequence.

### Theory of Set of Formulas

Let $\FF$ be a set of $\LL$-formulas.

Then the **$\LL$-theory of $\FF$**, denoted $\map T {\FF}$ is the set:

- $\set {\phi \in \LL: \FF \models_{\mathscr M} \phi}$

where $\models_{\mathscr M}$ denotes $\mathscr M$-semantic consequence.

## Also defined as

Some sources do not impose on a **theory** the restriction of being closed under $\mathscr M$-semantic consequence.

Then, **theory** is just a term describing an arbitrary set of $\LL$-formulas.

On $\mathsf{Pr} \infty \mathsf{fWiki}$, it was decided that the version with semantic consequence will be called **theory**.

In other sources, it always needs to be carefully inspected if a **theory** is considered to be closed under semantic consequence.

## Also known as

In cases where the language $\LL$ is obvious, one usually speaks of a **theory**.

## Also see

## Sources

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