Qiaochu, let me see if this answers your question:
Proposition: Suppose $B$ is a cartesian closed category with finite coproducts such that the canonical double dual embedding
$$b \to (b \Rightarrow 0) \Rightarrow 0$$
is an isomorphism (excluded middle). Then $B$ is equivalent (as a category) to a poset, and hence to a Boolean algebra.
Proof: First, in a cartesian closed category with $0$, for any object $b$ there exists a morphism $i: b \to 0$ only if $i$ is an isomorphism. For given $i$, the composite
$$b \stackrel{\langle i, 1_b \rangle}{\to} 0 \times b \stackrel{\pi_2}{\to} b$$
is an isomorphism. But $\pi_1: 0 \times b \to 0$ is an isomorphism since $- \times b$ preserves colimits by cartesian closure. Thus the composite of $i: b \to 0$ followed by the unique map $0 \to b$ is $1_b$. Since $0$ is initial, the composite of $0 \to b$ followed by $i: b \to 0$ is $1_0$. Hence $i$ is an isomorphism. In particular, there can be at most one morphism $b \to 0$ (again by initiality).
Next, for any two objects $b, c$ there can be at most one morphism $b \to c \Rightarrow 0$, since there are in bijective correspondence with morphisms $b \times c \to 0$, of which there is at most one. Finally, taking $c = b' \Rightarrow 0$ and assuming excluded middle, we have that for any two objects $b, b'$ there is at most one morphism $b \to b'$. $\Box$
The property of existence of $b \to 0$ forcing $b$ to be initial is called strictness of the initial object, and I think Mac Lane-Moerdijk prove that an initial object is strict in a cartesian closed category. I know this is in my notes on ETCS.
Edit: Qiaochu's instincts are correct. There is an old tradition in category theory, going back essentially to Lawvere's thesis, whereby one forms syntactic categories associated to theories and to various fragments of logic, and these are typically free categorical structures of various sorts. For example, the theory of groups is the free (initial) category with products containing a group object; the morphisms are well-formed terms in the equational language modulo the equational axioms imposed by the theory. A model of the theory will be a functor which preserves the categorical structure needed to express the logic (finite products in the case of finitary equational theories). A completeness theorem for a certain class of models says that whenever the semantic interpretations of two syntactic terms (or morphisms in the free categorical structure) are equal in each of the models of the class, then the syntactic terms are provably equivalent.
From the viewpoint of categorical logic, such completeness theorems can be seen as embedding or representation theorems. In spirit these go back to the Freyd-Mitchell embedding theorems; for example, each module category is a model of the abelian category axioms, and if a diagram commutes when interpreted in each such model, then it provably commutes on the basis of the abelian category axioms. Or, in categorical logic there is a notion of 'coherent theory' whose syntactic category is effectively its classifying topos, and there is a theorem due to Deligne that such a theory has 'enough points' (which are left exact left adjoints from the classifying topos to the category of sets). This can be interpreted either as saying that the classifying topos of the theory can be faithfully embedded (lex left-adjointly) into a product of copies of $Set$, or as saying that two morphisms are provably equivalent in the theory if their values under any set-theoretic model are equal.
Qiaochu's question has to do with bicartesian closed categories, seen as a natural categorification of the concept of Heyting algebra (the algebraic formalization of intuitionistic propositional logic, as Boolean algebras are the algebraic formalization of classical propositional logic). Here one can form appropriate syntactic categories as free bicartesian closed categories generated by a given set of sorts, or even by a given category of sorts. Now, there is still another tradition in categorical logic, due to Lambek and his school, whereby such free structures are constructed explicitly by taking suitable equivalence classes of formal Gentzen sequent deductions pertaining to the given fragment of logic, which here is intuitionistic propositional logic. The equivalence classes are dictated by naturality considerations and other compatibility conditions, reflecting the key conversions one sees in cut-elimination; see Girard's Proofs and Types. One can consult Manfred Szabo's Algebra of Proofs for a careful description of how this is done for quite a variety of logics, including, I believe, the case Qiaochu is interested in.
Off hand I am not sure what sort of completeness theorems there are for bicartesian closed categories (e.g., is there a faithful structure-preserving functor from a free bicartesian closed category to some power of $Set$? I have a sneaking suspicion finite sets are not enough). But perhaps the answer can be found in Freyd-Scedrov's Categories, Allegories, which contains a wealth or representation/embedding/completeness theorems [one of the great scientific themes of Freyd's career].
Best Answer
Which propositional logic are you asking about? Axioms K (your axiom 1) and S (your axiom 2) are admissible for the implicational fragment of intuitionistic propositional logic, but your axiom 3 is not. Your axiom 3' is redundant and follows from K and S. Short proof: $S(K(S(SKK)))K a b = b a$; apply the Curry–Howard isomorphism. Explicitly:
In fact, if we replace $\lnot A$ by $A \to q$, then the above derives $p \to ((p \to q) \to q)$ from axioms K and S. It's not surprising that this is derivable from K and S alone: it is easy to verify that $\lambda x . \lambda y . y x$ is a lambda term of the required type.