Connection between ultrafilters and maximal consistent sets I have been told by reputable sources that ultrafilters over the set of all formulas in a given logic corresponds to a maximal consistent set of formulas in that logic, and I am trying to wrap my head around why this is so, but I have a few difficulties understanding it. The logic I am considering is a form of modal logic.
The definitions I am working with are as follows

Definition 1 A filter $F$ over a non-empty set $S$ is a subset of $\mathcal{P}(S)$ such that
(a) $S \in F$
(b) if $x,y \in F$ then $x \cap y \in F$
(c) if $x \in F$ and $x \subseteq y \subseteq S$ then $y \in F$.
A filter $F$ is called proper if $F \subsetneq \mathcal{P}(S)$.
Definition 2 An ultrafilter is a proper filter $F$ which satisfies
$$x \notin F \text{ iff } (S \setminus x) \in F$$
for all $x \in \mathcal{P}(S)$.

Now, I understand that, thinking in terms of logic, (b) is equivalent to saying that the set of formulas is closed under $\wedge$, (c) is equivalent to modus ponens, and that the condition on ultrafilters is equivalent to saying that for all formulas, either the formula or its negation is in the set. I also understand that we need a proper filter, because otherwise $\bot$ would be in the set, making it inconsistent.
However, I don't understand what the significance of (a) is. And the thing that is really causing me trouble understanding is that when I think of a maximal consistent set, I think of a set of formulas, but an ultrafilter is a set of sets of formulas, so how can they be equivalent? For example, we need a proper subset to make sure $\bot$ is not in the set, but $\bot$ is already in $S$, and $\bot \in S$. Could someone clarify these issues for me?
Also, since an ultrafilter is a proper filter that is maximal, does it make sense to think of proper filters as consistent sets and ultrafilters as maximal consistent sets?
 A: The entailment relation $\vdash$ makes the set of formulas into a prelattice. As it turns out, $\vdash$ is best thought of as a smaller-than (in the non-strict sense) relation (unfortunately, the more pointy side of the $\vdash$ symbol is on the right, akin to typical greater-than relation symbols). In fact, the basic inference rules of intuitionist logic can be formulated as precisely those making the set of formulas preordered by $\vdash$ a Heyting prealgebra:
$\vdash$ is transitive and reflexive, i.e., a preorder.
$A \wedge B$ is the largest (most general) formula entailing (smaller than) both $A$ and $B$.
$A \vee B$ is the smallest formula larger than both $A$ and $B$.
$B \rightarrow C$ is the largest formula whose meet with $B$ entails $C$.
$\bot$ is the smallest formula.
$\top$ is the largest formula.
As Zhen Lin was saying, filters are defined more generally on lattices; in fact, filters can be defined even on partially ordered sets, though I haven't had occasion to see why they are useful when there is no meet operation defined. The same definitions also work in prelattices and preorders.
If you allow (like Bourbaki, and as I prefer) theories with theorems whose generalizations don't hold (e.g., by not requiring axioms to be sentences, where sentences are defined to be formulas that are free of free variables), then consistent theories correspond to the (proper--it is more standard and my preference to define filters so they are all proper) filters on the set of formulas preordered by $\vdash$, and sets that form a set of axioms of the theory correspond to subbases of it. At any rate, ultrafilters by definition are maximal filters, and so ultrafilters are (the theorems of) maximal theories in the more general Bourbaki sense, which corresponds to maximal consistent sets of formulas. By definition, regardless of the demands on theories, a set of formulas is consistent if and only if it forms a subbasis of a filter. Since maximal consistent sets, being subbases, generate filters, and since filters are themselves subbases of themselves, it follows that maximal consistent sets are the same as the ultrafilters any way you look at it.
But using the modern definition of theory, I'm thinking it should not be said that consistent sets of formulas always generate consistent theories. For instance, is it not the case that $x = y$ and $\exists{x} (x \neq y) $ together generate a filter but not in the modern fashion a consistent theory? Indeed, it's not the case that $x = y \wedge \exists{x} (x \neq y) \vdash \bot$, but if $x =y$ is a theorem, so is (using modern fashion) $\forall{x} (x =y)$, which contradicts $\exists{x}(x \neq y)$. Consistent theories in the modern sense correspond to filters generated by consistent sets of sentences (as opposed to formulas), and are more standardly identified with the set of sentences which are its theorems rather than than with the set of formulas which are its theorems.
For a filter $U$ on a Heyting prealgebra $S$ and $a \in S$, there is a filter extending $U$ containing $a$ if and only if $a \rightarrow \bot \notin U$. It follows that $U$ is an ultrafilter if and only if for each $a \notin U$, $a \rightarrow \bot \in U$.
