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$