nLab propositional theory

A propositional theory is a theory expressed in a language of propositional logic. The logic or type of deductive system might be classical, or intuitionistic, or linear, etc., but for the purposes of illustration, we consider below the classical case.

The algebraic point of view on classical propositional theories is that they are presentations of Boolean algebras. The formulas of the underlying language are formal Boolean combinations of atomic formulas; thus these atomic formulas are considered as a set SS which freely generates a Boolean algebra F(S)F(S). The axioms of the theory are a subset AA of such formulas, and the theorems of the theory are those elements of F(S)F(S) that belong to the filter AF(S)\langle A \rangle \hookrightarrow F(S) generated by AA.

Thus A\langle A \rangle can be considered as generating a congruence where ϕ1\phi \equiv 1 for each theorem ϕA\phi \in \langle A \rangle. The corresponding quotient (which we may denote by F(S)/AF(S)/\langle A \rangle) is a Boolean algebra BB which is the Lindenbaum algebra of the theory. In other words, BB has been presented by generators (elements of SS) subject to relations (elements of AA).

Again from the algebraic point of view, a model of the propositional theory is tantamount to a Boolean algebra homomorphism μ:B2={0,1}\mu: B \to \mathbf{2} = \{0, 1\} which assigns a definite truth value in 2\mathbf{2} to each proposition PF(S)P \in F(S), such that all theorems receive the value 11 (are “true”). From the point of view of the presentation, such a model μ\mu amounts to an ultrafilter in F(S)F(S) which extends the filter A\langle A \rangle.

Last revised on February 13, 2016 at 19:32:44. See the history of this page for a list of all contributions to it.