$\newcommand\FinSet{\mathit{FinSet}}\newcommand\FinBool{\mathit{FinBool}}\newcommand\FreeFinBool{\mathit{FreeFinBool}}\newcommand\Set{\mathit{Set}}\newcommand\Psh{\mathit{Psh}}$It's well-known that the topos of presheaves on the category $\FinSet$ of finite sets is the classifying topos for boolean algebra objects.
The argument goes like this: By Stone duality, the functor $n \mapsto 2^n$ is an equivalence of categories $\FinSet \simeq \FinBool^{\text{op}}$, where $\FinBool$ is the category of finite Boolean algebras, which are necessarily projective (so we may use $\FinBool$ and $\FreeFinBool$, which is dual to the category $\FinSet_{2^\bullet}$ of sets with cardinality a finite power of $2$, pretty much interchangeably). Since the theory of Boolean algebras is a finitary algebraic theory, finite-product-preserving functors $\FinBool^{\text{op}} \to \mathcal E$ are identified with Boolean algebra objects in $\mathcal E$, for any category $\mathcal E$ with finite products and split idempotents. If $\mathcal E = \Set$, then any finite-product-preserving functor $\FinBool \to \Set$ is automatically flat; the proof uses the fact that every finitely-presentable Boolean algebra is projective. So a geometric morphism $\Psh(\FinSet_{\neq \emptyset}) \to \Set$ is just a Boolean algebra. Then because $\Psh(\FinSet_{\neq \emptyset})$ is a presheaf topos and the theory of Boolean algebras is algebraic, this classifying topos identification extends to all Grothendieck toposes $\mathcal E$.
But what happens when we perturb the input a bit? For example, what happens when we consider presheaves on the category $\FinSet_\ast$ of finite pointed sets? The category $\FinSet_\ast^{op}$ is the idempotent completion of a Lawvere theory $\mathcal T = \FinSet_{\ast,2^\bullet}$ with half as many operations of each arity as the Lawvere theory for Boolean algebras ($2^{2^n - 1}$ instead of $2^{2^n}$). Indeed, by identifying the basepoint of a finite pointed set with $\top$, we can regard $\mathcal T$ as the Lawvere theory whose $n$-ary operations are all Boolean algebra homomorphisms $f: 2^n \to 2^1$ such that $f(\top,\dotsc,\top) = \top$ — i.e. if all inputs are true, the output must also be true. I believe that $\mathcal T$ is generated by the operations $\top, \wedge, \vee, \to$, but I'm not sure what a complete set of relations would be.
As a Lawvere theory, $\mathcal T$ may be rather messy. But we're considering something more refined: a finite-product-preserving functor $A: \mathcal T \to \Set$ is not automatically flat. Flatness is equivalent to requiring that $A$ is a filtered colimit of finitely-generated free algebras. In particular, every finitely-generated subalgebra of $A$ is a subalgebra of a finitely-generated free algebra. It follows that $A$ will satisfy any universal statement satisfied by all finitely-generated free $\mathcal T$-algebras — not just the algebraic ones. I think (but I'm not certain) that the converse is also true — so that $A$ is flat if and only if it satisfies the universal theory of free $\mathcal T$-algebras.
Questions:
What is an axiomatization of the algebraic theory of the logical connectives $\top, \wedge, \vee, \to$ (i.e. the algebraic theory of connectives $f$ such that $f(\top, \dotsc, \top) = \top$, i.e. the equational theory of the structures $\{\top,\bot\}^n$, in the language $(\top,\wedge,\vee,\to)$)?
What is an axiomatization of the universal theory of these logical connectives (i.e.— I think — the theory classified by the presheaf topos $\Psh(\FinSet_\ast)$, i.e. the universal theory of the structures $\{\top,\bot\}^n$, in the language $(\top,\wedge,\vee,\to)$)?
How do these theories compare to the theory of Boolean algebras — what are some examples of algebras or algebra homomomorphisms which don't come from Boolean algebras or homomorphisms thereof? Is there a form of Stone duality for these algebras, and how do the corresponding spaces compare to Stone spaces?
More fundamental than the presheaf toposes $\Psh(\FinSet)$ and $\Psh(\FinSet_\ast)$ are the presheaf toposes $\Psh(\FinSet^{\text{op}})$ and $\Psh(\FinSet_\ast^{\text{op}})$ which classify objects and pointed objects respectively. Unfortunately, these facts don't seem to shed much light on the less fundamental toposes I'm interested in here. For instance, it doesn't seem to be the case that the tensor product of the Lawvere theories $\FinSet^{\text{op}}_\ast$ and $\FinSet$ is $\FinSet_\ast$ — I believe that tensor product is just the terminal Lawvere theory (note that the "op"'s for the Lawvere theories are reversed from the "op"'s for the presheaf categories).
The operations $(\top,\wedge,\vee,\to)$ being considered here are almost the same as the operations of a Heyting algebra — the difference being that a Heyting algebra has a constant $\bot$ as well. So, based on the axioms for a Heyting algebra, here are some guesses:
Guess for (1): The following algebraic axioms, which are satisfied (thanks to Andreas Blass for catching a mistake in the comments below!), might be a complete set of algebraic axioms:
$(\top,\wedge,\vee)$ form an upper-bounded distributive lattice;
$x \to x = \top$;
$x \wedge (x \to y) = x \wedge y$; $y \wedge (x \to y) = y$;
$x \to (y \wedge z) = (x \to y) \wedge (x \to z)$;
$(x \vee y) \to z = (x \to z) \wedge (y \to z)$.
As pointed out by მამუკა ჯიბლაძე in the comments below, we also need the following axiom which goes beyond the Heyting axioms, and is equivalent to the interval $[y,\top]$ being a Boolean algebra with $(-) \to y$ for negation:
- $x \vee (x \to y) = \top$
