Return to Answer

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

EDIT: I may as well add a paring down of the definition now. Another (equivalent) way to define a Boolean logos is as a category with finite limits, a right adjoint to pullback of subobjects along any morphism, and an initial object, such that certain maps constructed out of this structure have inverses (explained below). The category BoolLog has these as 0-cells, functors preserving finite limits, initial objects, and right adjoints to subobject-pullback as 1-cells, and arbitrary natural transformations as 2-cells; as before, the Hom-categories BoolLog[B, Set] are the categories of models of B and elementary embeddings between them. The requirement for preservation of initial objects destroys many of the completeness/cocompleteness properties for models which we might otherwise have expected from universal algebra; e.g., there won't necessarily be finite limits of models or "free" (i.e., initial) models.

There are two isomorphism conditions to complete this definition of a Boolean logos: 1) the unique maps from an initial object to its product with any other object should be isomorphisms [i.e., products distribute over 0-ary coproducts], and 2) from the previous structure, it follows that the subobjects of any object form a cartesian closed preorder with an initial object. In these preorders, the initial objects should be dualizing [which suffices to make these Boolean algebras].

I didn't add conditions to force Boolean logoses to represent complete theories, but that's easy enough: this happens just in case the only subobjects of the terminal object are the unique maps into it from itself and the initial object. And, of course, consistency amounts to asking for these two maps to be distinct; equivalently, the terminal category is the unique Boolean logos representing an inconsistent theory.

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

EDIT: I may as well add a paring down of the definition now. Another (equivalent) way to define a Boolean logos is as a category with finite limits, a right adjoint to pullback of subobjects along any morphism, and an initial object, such that certain maps constructed out of this structure have inverses (explained below). The category BoolLog has these as 0-cells, functors preserving finite limits, initial objects, and right adjoints to subobject-pullback as 1-cells, and arbitrary natural transformations as 2-cells; as before, the Hom-categories BoolLog[B, Set] are the categories of models of B and elementary embeddings between them. The requirement for preservation of initial objects destroys many of the completeness/cocompleteness properties for models which we might otherwise have expected from universal algebra; e.g., there won't necessarily be finite limits of models or "free" (i.e., initial) models.

There are two isomorphism conditions to complete this definition of a Boolean logos: 1) the unique maps from an initial object to its product with any other object should be isomorphisms [i.e., products distribute over 0-ary coproducts], and 2) from the previous structure, it follows that the subobjects of any object form a cartesian closed preorder with an initial object. In these preorders, the initial objects should be dualizing [which suffices to make these Boolean algebras].

I didn't add conditions to force Boolean logoses to represent complete theories, but that's easy enough: this happens just in case the only subobjects of the terminal object are the unique maps into it from itself and the initial object. And, of course, consistency amounts to asking for these two maps to be distinct; equivalently, the terminal category is the unique Boolean logos representing an inconsistent theory.

EDIT2: Whoops, also, in both definitions, I forgot to add the Beck-Chevalley condition: for every object A, the right adjoint to subobject pullback along the projection A x - $\rightarrow$ - should be a natural transformation (from Sub(A x -) to Sub(-)).

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

EDIT: I may as well add a paring down of the definition now. Another (equivalent) way to define a Boolean logos is as a category with finite limits, a right adjoint to pullback of subobjects along any morphism, and an initial object, such that certain maps constructed out of this structure are isomorphism (explained below). The category BoolLog has these as 0-cells, functors preserving finite limits, initial objects, and right adjoints to subobject-pullback as 1-cells, and arbitrary natural transformations as 2-cells; as before, the Hom-categories BoolLog[B, Set] are the categories of models of B and elementary embeddings between them. The requirement for preservation of initial objects destroys many of the completeness/cocompleteness properties for models which we might otherwise have expected from universal algebra; e.g., there won't necessarily be finite limits of models or "free" (i.e., initial) models.

There are two isomorphism conditions to complete this definition of a Boolean logos: 1) the unique maps from an initial object to its product with any other object should be isomorphisms [i.e., products distribute over 0-ary coproducts], and 2) from the previous structure, it follows that the subobjects of any object form a cartesian closed preorder with an initial object. In these preorders, the initial objects should be dualizing [which suffices to make these Boolean algebras].

I didn't add conditions to force Boolean logoses to represent complete theories, but that's easy enough: this happens just in case the only subobjects of the terminal object are the unique maps into it from itself and the initial object. And, of course, consistency amounts to asking for these two maps to be distinct; equivalently, the terminal category is the unique Boolean logos representing an inconsistent theory.

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

EDIT: I may as well add a paring down of the definition now. Another (equivalent) way to define a Boolean logos is as a category with finite limits, a right adjoint to pullback of subobjects along any morphism, and an initial object, such that certain maps constructed out of this structure have inverses (explained below). The category BoolLog has these as 0-cells, functors preserving finite limits, initial objects, and right adjoints to subobject-pullback as 1-cells, and arbitrary natural transformations as 2-cells; as before, the Hom-categories BoolLog[B, Set] are the categories of models of B and elementary embeddings between them. The requirement for preservation of initial objects destroys many of the completeness/cocompleteness properties for models which we might otherwise have expected from universal algebra; e.g., there won't necessarily be finite limits of models or "free" (i.e., initial) models.

There are two isomorphism conditions to complete this definition of a Boolean logos: 1) the unique maps from an initial object to its product with any other object should be isomorphisms [i.e., products distribute over 0-ary coproducts], and 2) from the previous structure, it follows that the subobjects of any object form a cartesian closed preorder with an initial object. In these preorders, the initial objects should be dualizing [which suffices to make these Boolean algebras].

I didn't add conditions to force Boolean logoses to represent complete theories, but that's easy enough: this happens just in case the only subobjects of the terminal object are the unique maps into it from itself and the initial object. And, of course, consistency amounts to asking for these two maps to be distinct; equivalently, the terminal category is the unique Boolean logos representing an inconsistent theory.

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

I'm not sure if this is exactly the sort of thing you are looking for, but call a category a "Boolean logos" just in case it has finite limits, the subobjects of any object form a Boolean algebra under inclusion, and pullback along any morphism induces a homomorphism of such Boolean algebras with left and right adjoints. [Much of this definition is redundant, but no matter]. Boolean logoses, functors between them which preserve all the defining structure, and arbitrary natural transformations between those comprise a two-category, which I'll call BoolLog.

Up to equivalence, the categories of all models of some theory in multi-sorted classical first-order logic with equality and the elementary embeddings between them are precisely those of the form BoolLog[B, Set]. That is, a category C is equivalent to one of the form Mod*(T) just in case there is some Boolean logos B such that C is equivalent to the full subcategory of Set^B consisting of those functors which preserve Boolean logos structure.

This isn't really saying much (the definition of a Boolean logos is a very straightforward categorical rendering of the definition of multi-sorted classical first-order logic with equality [although, like I said, it could be pared down a bit. And, of course, we can easily tweak the former definition around a little to correspond to variants on the latter (e.g., the single-sorted case, the intuitionistic case, etc.)]), but, perhaps such categorical rendering is all you were looking for (although, re-reading the reply you gave to my comment above, I suspect you were after a different sort of answer. Oh well.)

EDIT: I may as well add a paring down of the definition now. Another (equivalent) way to define a Boolean logos is as a category with finite limits, a right adjoint to pullback of subobjects along any morphism, and an initial object, such that certain maps constructed out of this structure are isomorphism (explained below). The category BoolLog has these as 0-cells, functors preserving finite limits, initial objects, and right adjoints to subobject-pullback as 1-cells, and arbitrary natural transformations as 2-cells; as before, the Hom-categories BoolLog[B, Set] are the categories of models of B and elementary embeddings between them. The requirement for preservation of initial objects destroys many of the completeness/cocompleteness properties for models which we might otherwise have expected from universal algebra; e.g., there won't necessarily be finite limits of models or "free" (i.e., initial) models.

There are two isomorphism conditions to complete this definition of a Boolean logos: 1) the unique maps from an initial object to its product with any other object should be isomorphisms [i.e., products distribute over 0-ary coproducts], and 2) from the previous structure, it follows that the subobjects of any object form a cartesian closed preorder with an initial object. In these preorders, the initial objects should be dualizing [which suffices to make these Boolean algebras].

I didn't add conditions to force Boolean logoses to represent complete theories, but that's easy enough: this happens just in case the only subobjects of the terminal object are the unique maps into it from itself and the initial object. And, of course, consistency amounts to asking for these two maps to be distinct; equivalently, the terminal category is the unique Boolean logos representing an inconsistent theory.