O.K, a massively naive question. I've never really studied any non-standard models of PA before. I was just wondering if there's ever been any attempt to use the kind of Boolean valued model theory familiar from set theory in the context of arithmetic. Obviously, the actual structure of the model would have to be very different, but I mean specifically the idea of using elements of a complete Boolean algebra as truth-values for sentences of PA. If this hasn't been done, has anyone got any ideas about if/how it could be done?



Boolean Valued Models of PA
For any complete Boolean algebra $\mathbb{B}$, we may form the class $V^{\mathbb{B}}$ of all $\mathbb{B}$ names, and define $\mathbb{B}$-valued truth $[\! [\varphi]\! ]\in\mathbb{B}$ in the usual set-theoretic manner. By restricting to names $\tau$ for which $[\! [\tau\in\check{\mathbb{N}}]\! ]=1$, we get a natural $\mathbb{B}$-valued model of PA. In particular, for any ultrafilter $U\subset\mathbb{B}$ we may form the Boolean ultrapower $j:V\to \check V/U$, defined by $j(x)=[\check x]\_U$, where $\tau=\_U\sigma$ just in case $[\![\tau=\sigma]\!]\in U$. Restricting this embedding to the natural number structure gives an elementary embedding of $\mathbb{N}$ into $\check{\mathbb{N}}/U$, which is the quotient of the $\mathbb{B}$-valued structure consisting of names for natural numbers. This is discussed in my paper [Well-founded Boolean ultrapowers as large cardinal embeddings](http://jdh.hamkins.org/boolean-ultrapowers/), which provides a general introduction to the Boolean ultrapower. 


To summarize: the basic idea is to use the forcing-theoretic name construction, but consider only the class of names that name a natural number. This is naturally a Boolean-valued model of PA, whose quotients by an ultrafilter will give actual nonstandard models of PA.


Basically, since we have a $\mathbb{B}$-valued model $V^{\mathbb{B}}$ of an entire set-theoretic universe, we get inside that $\mathbb{B}$-valued models of any particular kind of mathematical structure, simply by restricting the class of names for objects in that structure.


