Models of propositional logic Define a theory of propositional calculus as the set $T$ of axioms (expressed in propositional calculus) and a set of valid symbols.
What I would like to see are some examples of theories in propositional calculus and the respective models - what are they?
Are there any "real life" examples of theories in propositional calculus? (Not just the classical lets model the statement "today is raining" type theories..)
 A: A model of propositional calculus is the same as a Boolean algebra. They have a variety of applications, though mostly related to logic itself.
There's not much for the concept of "theory" to do in propositional calculus, because the only elements of the language that axioms could help giving meaning to are the proposition letters themselves. I suppose there are problem types in lattice and order theory that might in principle be formulated as "propositional theories", but usually it is more convenient to handle them using algebraic or graph-theoretic tools instead.
Later correction, after I got my brain into gear: Finitely axiomatized propositional theories are of paramount importance in computer science, specifically complexity theory. The problem of determining whether a given theory is consistent is known better as the SAT problem, and is the fundamental example of a NP-complete problem. (This is equivalent to determining whether a given formula can be proved from a finite set of axioms, which is the case if and only if the axioms plus the negation of the goal constitute an inconsistent theory).
As a simpler example, you could consider graph reachability -- that is, the problem given a directed graph and distinguished vertices $A$ and $B$ to find out whether there is a path from $A$ to $B$. To phrase this as a propositional theory, choose a proposition letter $\hat V$ for each vertex $V$, whose intuitive meaning is to be "$V$ is reachable from $A$". Now take as axioms the formula $\hat A$ plus $\hat P\to\hat Q$ for each edge $P\to Q$. Then $B$ is reachable exactly when $\hat B$ is a theorem.
On the other hand, this latter example is arguably too simple to really utilize the machinery of propositional logic. It is better suited as an example of a simple generic formal system, where we model the edges as rules of inference rather than axioms.
