Boolean Valued Models of PA 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?
 A: This belated answer is prompted by:
(1) Joel Hamkins' answer, in which he brings attention to Boolean ultrapowers of models of arithmetic.
(2)  Emil Jeřábek's comment "Using sophisticated tools to construct elementary extensions is simply a waste of effort" (in the exchange with Hamkins following Jeřábek's answer).
First a definition: full arithmetic is the first order theory of the full expansion of the standard model of arithmetic, i.e, it is the first order theory of the model $ (\Bbb{N}, X)_{X \subseteq{\omega}}$, where $\Bbb{N}$ is the standard model of arithmetic $(\omega, +, \times)$.  Note that full arithmetic has an uncountable vocabulary.
Next, two results of Andreas Blass from the mid-1970s:
Theorem 1. Every model $\cal{A}=$ $(A, \cdot \cdot \cdot) $ of full arithmetic has a conservative elementary end extension $\cal{B}=$ $(B, \cdot \cdot \cdot) $, i.e., if X is a subset of B that is parametrically definable in $\cal{B}$, then $X \cap A$ is parametrically definable in $A$.
Theorem 2. Assuming CH (the continuum hypothesis) there is a model of full arithmetic that possesses a nonconserative elementray end extension.
And, finally, the point of this posting: back in 1990, I used the method of Boolean ultrapowers to improve theorem 2 above by eliminating the CH assumption.
My result appears as Theorem 3.4 of the paper below, which includes references for the aforementioned results of Blass, as well as other applications of the method of Boolean ultrapowers.
A. Enayat, Minimal elementary extensions of models of set theory and arithmetic. 
Arch. Math. Logic 30 (1990), no. 3, 181–192.
A: The paper "Partially definable forcing and bounded arithmetic" by
A. Atserias and M. Müller presents a very general framework of forcing for models of (week) arithmetic.
Its presentation is more close to set theoretic forcing and it gives constructions of Paris and Wilkie, Riis and Ajtai.

In addition, I found the abstract of the paper
''A Nonstandard Model of Arithmetic Constructed by means of Forcing Method''
by Zhang Jinwen surprising (The paper seems to be in Chinese, and I don't know if it is translated to English or not). 

Abstract: The first nonstandard model of arithmetic was given by Skolem. A. Robinson has introduced the concepts of standard, internal and external objects (sets, relations, functions, etc.) on the compactness theorem and concurrent relations, and has proved that if a set S is infinite, then S contains nonstandard internal objects. It is interesting to ask whether this is a common property of all non-standard modes of arithmetic. The author's answer to this question is in the negative.We have proved the theorem that there exists a nonstandard model of formal arithmetic in which there are infinitely many infinte internal subsets containing no nonstandard elements.This means that these infinite internal subsets are composed exclusively of finite natural numbers. In order to obtain this theorem we have made use of Cohen's forcing method.

A: 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, 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.
A: It proves quite challenging to set up a notion of Boolean-valued models for arithmetic that on the one hand does not trivialize (i.e., the result is not elementarily equivalent to the original model), and on the other hand, gives models of a sufficiently strong theory.
The area where it works with moderate success are fragments of bounded arithmetic, where Boolean-valued models (or direct forcing constructions) have been used to prove independence results, such as Ajtai’s seminal result about PHP. A unified framework for Boolean-valued models of bounded arithmetic and its applications in proof complexity can be found in Krajíček’s book Forcing with random variables and proof complexity.
