O.K, a massively naive question. I've never really studied any nonstandard 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 truthvalues for sentences of PA. If this hasn't been done, has anyone got any ideas about if/how it could be done?
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 settheoretic 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 Wellfounded Boolean ultrapowers as large cardinal embeddings, which provides a general introduction to the Boolean ultrapower.
To summarize: the basic idea is to use the forcingtheoretic name construction, but consider only the class of names that name a natural number. This is naturally a Booleanvalued 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 settheoretic 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.

$\begingroup$ Thanks so much Joel. That makes perfect sense. I don't know why I didn't think of it. $\endgroup$ – King Kong Oct 2 '14 at 11:56

$\begingroup$ But if the embedding is elementary, what’s the point? $\endgroup$ – Emil Jeřábek Oct 2 '14 at 12:10

$\begingroup$ It is elementary, but not surjective, so these will be nonstandard $\mathbb{B}$valued models of true arithmetic. If you want models of some other theory, instead of true arithmetic, then use names for elements of another fixed structure, and you'll get a nonstandard $\mathbb{B}$valued version of that structure. $\endgroup$ – Joel David Hamkins Oct 2 '14 at 12:12

1$\begingroup$ That does not help. You want to use forcing to construct models of something that does not hold in the model you start with, elementary extension can be trivially constructed using compactness without the need for any forcing machinery. $\endgroup$ – Emil Jeřábek Oct 2 '14 at 12:15

$\begingroup$ The Boolean ultrapower is a definable elementary embedding $j:V\to\check V/U$, such that in $V$ there is a $\check V/U$generic object $G$ for the image of $\mathbb{B}$. So basically, it provides an elementary extension of $V$ for which you have an actual generic object and can then form the generic extension, which is the same as the full quotient $V^{\mathbb{B}}/U$. So the forced theory is what is true in $V^{\mathbb{B}}/U$, whose ground model is the Boolean ultrapower $\check V/U$. $\endgroup$ – Joel David Hamkins Oct 2 '14 at 12:17
It proves quite challenging to set up a notion of Booleanvalued 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 Booleanvalued models (or direct forcing constructions) have been used to prove independence results, such as Ajtai’s seminal result about PHP. A unified framework for Booleanvalued 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.

$\begingroup$ Ah, now I understand what you were driving at in your comments on my answer. This of course is what people would ordinarily mean by forcing over models of PA. In my answer, I was focused merely on the problem of constructing Booleanvalued models of PA, which is what I understood the question to be about. $\endgroup$ – Joel David Hamkins Oct 2 '14 at 13:32

1$\begingroup$ But in particular, isn't "trivialize" a bit strong in your first sentence? After all, we don't ordinarily understand the ultrapower construction to be trivial, just because it provides an elementary extension. Similarly, the Boolean ultrapowers should be thought of as a fundamental modeltheoretic tool, providing models with perhaps interesting cuts and so on. $\endgroup$ – Joel David Hamkins Oct 2 '14 at 13:34

1$\begingroup$ The ultrapower construction is trivial in many respects, and that’s undoubtedly one of the reasons it appears so rarely in modern model theory. It only survives in the context of set theory where one needs to deal with classsized models. You can get any cuts you want with plain compactness (or starting with a sufficiently saturated model, as people usually do). Using sophisticated tools to construct elementary extensions is simply a waste of effort. $\endgroup$ – Emil Jeřábek Oct 2 '14 at 13:48

1$\begingroup$ I see; that is an interesting perspective. Meanwhile, is there hope that the methods you are talking about will provide models of PA? $\endgroup$ – Joel David Hamkins Oct 2 '14 at 15:05

2$\begingroup$ I am not aware of any results that would give models of PA. The progress of the methods for bounded arithmetic is stalled at the theories $V^0[p]$ (related to boundeddepth Frege systems with mod$p$ counting gates; a lower bound for these systems is a major open problem). However, it is not entirely clear to me whether that’s because forcing for stronger arithmetical theories is inherently combinatorially difficult, or because the methods are intentionally geared towards independence of statements of low complexity that translate to propositional lower bounds. $\endgroup$ – Emil Jeřábek Oct 2 '14 at 16:13
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 mid1970s:
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.

1$\begingroup$ Ali, I recall that you once spoke on this for the CUNY Logic Workshop. Is that right? $\endgroup$ – Joel David Hamkins Oct 13 '14 at 12:47

1$\begingroup$ Joel, as far as I remember, I only gave one talk related to this topic, and that was in an ASLmeeting at Penn State in 1990. But I remember discussing Boolean ultrapowers with you in New York (and my paper on this topic), some time around 2005. $\endgroup$ – Ali Enayat Oct 13 '14 at 14:16

1$\begingroup$ I remember you talking about Boolean ultrapowers (in an equivalent formulation) and conservative endextensions in one of your talks in Room 6417, but it may have been in the context of a talk on another topic. No matter... $\endgroup$ – Joel David Hamkins Oct 13 '14 at 16:14

1$\begingroup$ Joel, I will take your word for it, especially because you remember the room! $\endgroup$ – Ali Enayat Oct 13 '14 at 16:47

2$\begingroup$ That is our room with the wraparound floortoceiling chalkboards. $\endgroup$ – Joel David Hamkins Oct 13 '14 at 16:49
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 nonstandard 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.