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?
$\begingroup$
$\endgroup$
Add a comment
|
4 Answers
$\begingroup$
$\endgroup$
8
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.
answered Oct 2, 2014 at 11:53
-
$\begingroup$ Thanks so much Joel. That makes perfect sense. I don't know why I didn't think of it. $\endgroup$ Commented Oct 2, 2014 at 11:56
-
$\begingroup$ But if the embedding is elementary, what’s the point? $\endgroup$ Commented Oct 2, 2014 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$ Commented Oct 2, 2014 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$ Commented Oct 2, 2014 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$ Commented Oct 2, 2014 at 12:17
$\begingroup$
$\endgroup$
13
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.
answered Oct 2, 2014 at 12:34
-
$\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 Boolean-valued models of PA, which is what I understood the question to be about. $\endgroup$ Commented Oct 2, 2014 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 model-theoretic tool, providing models with perhaps interesting cuts and so on. $\endgroup$ Commented Oct 2, 2014 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 class-sized 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$ Commented Oct 2, 2014 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$ Commented Oct 2, 2014 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 bounded-depth 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$ Commented Oct 2, 2014 at 16:13
$\begingroup$
$\endgroup$
5
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.
answered Oct 13, 2014 at 12:24
-
1$\begingroup$ Ali, I recall that you once spoke on this for the CUNY Logic Workshop. Is that right? $\endgroup$ Commented Oct 13, 2014 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 ASL-meeting 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$ Commented Oct 13, 2014 at 14:16
-
1$\begingroup$ I remember you talking about Boolean ultrapowers (in an equivalent formulation) and conservative end-extensions 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$ Commented Oct 13, 2014 at 16:14
-
1$\begingroup$ Joel, I will take your word for it, especially because you remember the room! $\endgroup$ Commented Oct 13, 2014 at 16:47
-
2$\begingroup$ That is our room with the wrap-around floor-to-ceiling chalkboards. $\endgroup$ Commented Oct 13, 2014 at 16:49
$\begingroup$
$\endgroup$
0
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.
answered Oct 2, 2014 at 15:10