Введение
Концепция теории множеств
В математической логике, булевальнозначная модель является обобщением обычного тарского понятия структуры из теории моделей. В булевальнозначной модели, значения истинности высказываний не ограничиваются "истиной" и "ложностью", а вместо этого принимают значения в некоторой фиксированной полной булевой алгебре. Булевальнозначные модели были введены Даной Скотт, Робертом М. Солоуэем и Петром Вопенкой в 1960-х годах для лучшего понимания метода принуждения Пола Коэна. Они также связаны с семантикой алгебры Хейтинга в интуиционистской логике.
In mathematical logic, a Boolean valued model is a generalization of the ordinary Tarskian notion of structure from model theory. In a Boolean valued model, the truth values of propositions are not limited to "true" and "false", but instead take values in some fixed complete Boolean algebra. Boolean valued models were introduced by Dana Scott, Robert M. Solovay, and Petr Vopěnka in the 1960s in order to help understand Paul Cohen's method of forcing. They are also related to Heyting algebra semantics in intuitionistic logic.
Определение
Зафиксируем полную булеву алгебру B и язык первого порядка L; сигнатура L состоит из набора символов констант, символов функций и символов отношений. Булева модель для языка L состоит из области M, представляющей собой множество элементов (или имен), вместе с интерпретациями символов. В частности, модель должна сопоставить каждому символу константы L элемент из M, а каждому n-арному символу функции f из L и каждой n-кортежу элементов из M – элемент из M, соответствующий терму f(a0, ..., an-1). Интерпретация атомарных формул L более сложна. Для каждой пары элементов a и b из M модель должна сопоставить значение истинности выражению ; это значение истинности берется из булевой алгебры B. Аналогично, для каждого n-арного символа отношения R из L и каждого n-кортежа элементов из M модель должна сопоставить элемент B в качестве значения истинности.
Отношение к принуждению
Теоретики множеств используют метод, называемый принуждением, для получения результатов независимости и построения моделей теории множеств в других целях. Метод был первоначально разработан Полом Коэном, но с тех пор значительно расширен. В одной из форм принуждение "добавляет во вселенную" родовое подмножество посета, при этом посет конструируется таким образом, чтобы наложить интересные свойства на вновь добавленный объект. Проблема в том, что (для интересных посет) можно доказать, что такого родового подмножества просто не существует. Существует три основных способа решения этой проблемы:
синтаксическое принуждение: определяется отношение принуждения между элементами *p* посета и формулами φ языка принуждения. Это отношение определяется синтаксически и лишено семантики, то есть модель не строится. Вместо этого, исходят из предположения, что ZFC (или другая аксиоматизация теории множеств) доказывает независимое утверждение, и показывают, что ZFC также должно быть способно доказать противоречие. При этом принуждение происходит "над V", то есть нет необходимости начинать с счётной транзитивной модели. Подробнее об этом методе см. в Кунен (1980). счётные транзитивные модели: начинают с счётной транзитивной модели *M* теории множеств, содержащей посет и достаточной для достижения поставленной цели. Затем существуют фильтры на посете, которые являются родовыми относительно *M*, то есть пересекают все плотные открытые подмножества посета, которые также являются элементами *M*.
фиктивные родовые объекты: теоретики множеств часто просто предполагают, что посет имеет подмножество, родовое относительно всей *V*. Этот родовый объект, в нетривиальных случаях, не может быть элементом *V* и, следовательно, "фактически не существует". (Разумеется, вопрос о том, существуют ли множества "фактически", является предметом философских споров, но выходит за рамки данного обсуждения.) При некоторой практике этот метод оказывается полезным и надёжным, хотя и может быть философски неудовлетворительным.
syntactic forcing A forcing relation is defined between elements p of the poset and formulas φ of the forcing language. This relation is defined syntactically and has no semantics; that is, no model is ever produced. Rather, starting with the assumption that ZFC (or some other axiomatization of set theory) proves the independent statement, one shows that ZFC must also be able to prove a contradiction. However, the forcing is "over V"; that is, it is not necessary to start with a countable transitive model. See Kunen (1980) for an exposition of this method. countable transitive models One starts with a countable transitive model M of as much of set theory as is needed for the desired purpose, and that contains the poset. Then there do exist filters on the poset that are generic over M; that is, that meet all dense open subsets of the poset that happen also to be elements of M.
fictional generic objects Commonly, set theorists will simply pretend that the poset has a subset that is generic over all of V. This generic object, in nontrivial cases, cannot be an element of V, and therefore "does not really exist". (Of course, it is a point of philosophical contention whether any sets "really exist", but that is outside the scope of the current discussion.) With a little practice this method is useful and reliable, but it can be philosophically unsatisfying.