A geometric theory of Blueprints? (Algebras over the field with one element) In my attempt to tackle the various approaches of defining algebraic geometry over $\mathbb F_1$, I was just reading through Lorscheid's paper The geometry of blueprints. I certainly like the idea a lot and I get the feeling of it being the 'right' approach to $\mathbb F_1$.
A blueprint is a commutative monoid $B$ with zero, together with a pre-addition, which is -the way he defines it- an  additive, multiplicative equivalence relation on $\mathbb N(B)$ respecting the $0$, i.e. ($0_\mathbb N \equiv 0_B$) and reflecting equality on simple terms $a \equiv b \implies a = b$.
A morphism of blueprints is a homomorphism of monoids respecting $0$ and the pre-addition.
The idea is that blueprints should be $\mathbb F_1$-algebras, with $\mathbb F_1$ being given by $\left\{0,1\right\}$ with standard multiplication and trivial pre-addition. $\mathbb F_1$ is then the initial object in the category of blueprints.
Blueprints generalize semirings and commutative monoids in a nice way ($\text{SemiRing}$ and $\text{CommMonoids}$ are full reflective subcategories of the category of blueprints).
They carry just enough structure to talk about ideals. He then defines blueprinted spaces and locally blueprinted spaces in much the way you'd expect, and from that also 'blue schemes' (as locally blue spaces being locally isomorphic to $\text{Spec}(B)$ for a blueprint $B$).
Now, I'm sure the answer is simple, but are 'Blueprints' a geometric theory? In particular, what would be a nice way to write down the axioms?
Let me phrase it like this

Is there a geometric theory whose $\text{Set}$ based models are blueprints? Is it coherent? Can it be extended to a theory of $\textit{local}$ blueprints?

It is a standard fact that the classifying topos of the coherent theory of local $R-$algebras is the gros zariski topos over $Spec(R)$. Given that the answer to the above question is yes, is the following true?

A blue scheme (as defined by Lorscheid) can be regarded as an object of the classifying topos of the theory of local blueprints.

In the same style of thinking, the topos of sheaves on the spectrum of a given blueprint $B$ should classify the 'theory of prime filters on $B$' in the same way as the topos of sheaves on the spectrum of a commutative ring classifies its theory of prime filters.
I'm still a novice in topos theory, which is why I'm asking: Does any of this make sense?
 A: $\newcommand{\N}{\mathbb N}\newcommand{\paren}[1]{\left(#1\right)}\newcommand{\T}{\mathbb{T}}\newcommand{\m}{\mathfrak{m}}\newcommand{\E}{\mathbf{E}}$I can answer your first set of questions:
There is a geometric theory of blueprints. It's easiest* to work from the definition of a blueprint as a pair $B = (A,R)$ consisting of a semiring $R$ and a multiplicative subset $A \subseteq R$ which contains $0$ and $1$, and which generates all of $R$. 
The theory will have a sorts $A,R$, function symbols $+, \cdot$, constant symbols $0_A,1_A, 0_R, 1_R$, and a unary function symbol $\iota$, giving the inclusion of $A$ into $R$. In addition to axioms asserting that $R$ is a semiring and that $A$ embeds monomorphically as a multiplicative submonoid of $R$ such that $\iota(0_A) = 0_R$ and $\iota(1_A) = 1_R$, we have the infinitary axiom
$$ \vdash^{x : R} (x = 0) \lor \paren{\bigvee_{n \in \N, \; \varphi \in \text{Oper}_{n+1}}\exists a_0\dotsm a_n . \varphi(\iota(a_0),\dotsc,\iota(a_n)) = x }$$
where $\text{Oper}_n$ is the set of $n$-ary semiring operations built from $0_R,1_R,+,\cdot$. This axioms states that $A$ suffices to generate all of $R$
There can be no coherent axiomatization of the theory $\T$ of blueprints. To see this, suppose that $\T$ were coherent. Then we could obtain a new coherent theory $\T\,'$ by introducing the following additional coherent axioms which require a blueprint in $\text{Set}$ to be isomorphic to $(\{0,1\} \hookrightarrow \N)$.
$$
\vdash^{a: A} \iota(a) = 0 \lor \iota(a) = 1
$$ $$
x + y = 0 \vdash^{x,y : R} x = y = 0 $$
Since any consistent finitary first-order theory with an infinite model will admit arbitrarily large models in $\text{Set}$, this is impossible.
Regarding local blueprints: The definition of local blueprints as those having a unique maximal ideal of course cannot, in its current form, be stated in geometric logic. However, we can say in $\text{Set}$ that a congruence $\sim_\m$ on a blueprint $B = (A,R)$ is the unique maximal nontrivial congruence on $B$ iff for any pair of elements $x,y \in R$, if $x \sim_\m y$ fails, then the smallest congruence $\sim$ such that $x \sim y$ is trivial. This can be stated in a conservative geometric extension of our theory of blueprints if we adjoin a binary relation symbol $\sim_m$ on $R \times R$, together with axioms stating that $\sim_m$ is a congruence, in addition to the following axiom which states that unless $x \sim_\m y$ holds, every congruence containing $(x,y)$ contains every pair of elements in $R$.
$$\vdash^{x,y,z,w:R} {x \sim_\m y \lor} \paren{\bigvee_{n \in \N} \exists a_0\dotsm a_n : A . \E(z,\iota(a_0)) \land \E(\iota(a_0), \iota(a_1)) \land \dotsi \land \E(\iota(a_n), w)}
$$ where $\E(c,d)$ denotes the sub-expression $$
\bigvee_{n \in \N, \; \varphi \in \text{Oper}_{n+2}} \exists b_0 \dotsm b_n : A. \varphi(c,b_0,\dotsc,b_n) = \varphi(d,b_0, \dotsc, b_n)
$$
*But not essential. Since the list object is a geometric construction, we could also write down a two-sorted theory which axiomatizes the behavior of an equivalence relation on the set of lists. The downside of that approach is that it would involve lots of complicated-to-state infinitary axioms.
