Here's the contents of file I get when I export from LyX using LaTeX
(plain). It is followed by the output from TeXWorks's console output
window after running bibtex.
This is really long. Stefano asked for it.
***************************************************************
%% LyX 2.0.5.1 created this file. For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
\documentclass[10pt,english]{article}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\usepackage{geometry}
\geometry{verbose,tmargin=3.4cm,bmargin=3.4cm,lmargin=4.4cm,rmargin=4.4cm}
\usepackage{amstext}
\usepackage{amssymb}
\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
\newcommand{\noun}[1]{\textsc{#1}}
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage{tikz}
\makeatother
\usepackage{babel}
\begin{document}
\title{Actualism, Serious Actualism, and Quantified Modal Logic }
\author{Author}
\date{August 27, 2014}
\maketitle
\begin{abstract}
Actualism is the view that whatever is, in any sense of the word,
is actual. Serious actualism is the view that a sentence consisting
of a predicate applied to a singular term is false if the term does
not denote. In this paper I develop SAT, a seriously actualistic quantified
modal logic based on T, that also supports an actualistic interpretation.
SAT contains an abstraction operator by means of which predicates
can be created out of complex formulas. This makes it possible to
prove a uniform substitution theorem: If a sentence $\phi$ is logically
true, then any sentence that results from substituting a (perhaps
complex) predicate abstract for each occurrence of a simple predicate
abstract in $\phi$ is also logically true. (This solves a problem
identified by Kripke at the very beginning of the modern semantic
study of modal logic.) Following an approach developed by Menzel I
also show that SAT supports a thoroughly actualistic definition of
truth \emph{simpliciter}. I also present a tableau proof system and
prove that it is sound and complete with respect to logical truth.
Extension of the tableau rules, and corresponding soundness and completeness
results, to systems based on other propositional modal logics (e.g.,
K, B, S4, and S5) is straightforward. Such extensions preserve uniform
substitution and other metatheorems. \medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\medskip{}
\end{abstract}
\date{\tableofcontents{}}
\section{Preliminaries}
How should we deal with subject-predicate sentences containing non-denoting
singular terms? Suppose \textquoteleft{}Dweet\textquoteright{} is
a name that doesn't denote anything, and consider the following sentences.
\begin{description}
\item [{(1)}] Dweet is a sexagenarian.
\item [{(2)}] Dweet enjoys messing about in boats.
\end{description}
It seems perfectly plausible to construe \textquoteleft{}is a
sexagenarian\textquoteright{}
and \textquoteleft{}enjoys messing about in boats\textquoteright{}
as predicates, and thus to take the sentences in question to be of
subject-predicate form. I\textquoteright{}ll call such
sentences\textemdash{}those
that result from applying a predicate to a singular
term\textemdash{}\emph{attributive
sentences}. I'll also use this term for sentences like (3) that apply
a relational predicate to two or more singular terms.
\begin{description}
\item [{(3)}] Obama is taller than Dweet.
\end{description}
How should truth values be assigned to attributive sentences like
(1)-(3) that contain at least one non-denoting singular term?
One answer to this question is that such sentences have no truth values.
Another is that they have truth values, some of them being true and
others false, just like ordinary attributive sentences. A third answer,
the one I advocate and want to explore here, is that all such attributive
sentences are false. If there is no such thing as Dweet, then all
claims to the effect that Dweet has such and such properties (or stands
in such and such relations) are incorrect, and all sentences that
express such claims are false. This view has been called \emph{serious
actualism}.%
\footnote{For example by Plantinga, \cite{plantinga:1985a}, p. 93, and
\cite{plantinga:1985b},
p. 316, and by Stephanou \cite{stephanou:2007}, 219. %
}
Intuitively, serious actualism provides a model for understanding
ordinary language that is at least as plausible as those provided
by the other two alternatives. And when properly developed it has
advantages, both technical and philosophical, over them. Or so I claim.
Briefly put, serious actualism is superior to the no-truth-value view
because it does not require that we abandon two-valued logic. It is
superior to the some-are-true-some-are-false alternative because it
is less likely to tempt us with metaphysical excess, and because it
forces us to draw a sharp line between the logic of fiction and the
logic of non-fictional discourse. More fundamentally, serious actualism
reflects some basic intuitions about objects and predication better
than the other two approaches.%
\footnote{Burge endorses this view in \cite{Burge1974}, 313. He doesn't use
the term ``serious actualism'', but he presents a first-order schema
that expresses it using primitive predicate and relational terms.
Of this schema he says, ``It expresses a deep and widely held intuition
that the truth of simple singular sentences (other than those implicitly
embedded in intensional contexts) is contingent on the contained singular
terms' having a denotation. The pre-theoretic notion seems to be that
true predications at the most basic level express comments on topics,
or attributions of properties or relations to objects: lacking a topic
or object, basic predications cannot be true.'' %
}
I also advocate \emph{actualism}, the view that everything that is,
in any coherent sense of `is', is actual. According to actualism
there are no merely possible things, things that don't exist but somehow
manage to subsist or have some alternative kind of being. Non-denoting
names like \textquoteleft{}Dweet\textquoteright{} and `Pegasus'
really are non-denoting. They don't denote, designate or refer in
any sense.
In what follows I develop a system of quantified modal logic that
is both seriously actualistic and actualistic. A major goal is to
extend the thesis of serious actualism to complex predicates without
giving up desirable logical properties, the most important of which
is uniform substitution. Substituting a complex predicate for each
occurrence of a simple predicate in a logical truth should yield a
logical truth.
Any seriously actualistic attempt to deal with sentences more complex
than simple attributive sentences faces two problems. One is easily
solved; the solution to other is more difficult. The first problem
is that in standard modern logic connectives and quantifiers are usually
treated only as devices for generating more complex sentences out
of simpler ones. But in natural language they play a second role as
well, allowing us to generate more complex predicates and relational
terms out of simpler ones. This point is easily illustrated, using
negation, with the following sentence.
\begin{description}
\item [{(4)}] Dweet is not a sexagenarian.
\end{description}
Is (4) an attributive sentence, with \textquoteleft{}is not a
sexagenarian\textquoteright{}
as its predicate, or is it simply the negation of the attributive
sentence (1)? If we choose the former answer, we seem to be multiplying
primitive predicates needlessly. But if we choose the latter, we are
forced to say that (4) is true, since it negates (1), which is false.
Yet this seems arbitrary, because \textquoteleft{}is not a
sexagenarian\textquoteright{}
appears to have as good a claim to being a predicate as \textquoteleft{}is
a sexagenarian\textquoteright{}. And if (4) is an attributive sentence,
then under the seriously actualistic approach to non-designating singular
terms it is false, not true.
This problem is easily solved by adopting a suitable device for
distinguishing
the scopes of negation and other logical operators. We want to distinguish
between
\begin{description}
\item [{(4a)}] Dweet is a non-sexagenarian.
\end{description}
and
\begin{description}
\item [{(4b)}] It is not the case that Dweet is a sexagenarian.
\end{description}
In the formal language developed in later sections this distinction
will be marked using a predicate abstraction operator ($\lambda$),
that allows us to render (4a) and (4b) as follows.
\begin{description}
\item [{(4a{*})}] $\langle\lambda x.\neg Sx\rangle(d)$
\item [{(4b{*})}] $\neg\langle\lambda x.Sx\rangle(d)$
\end{description}
In (4b{*}) the predicate $\langle\lambda x.Sx\rangle$ (is a sexagenarian)
is applied to the singular term $d$ (Dweet), and the resulting sentence
is negated. But in (4a{*}) negation is involved in forming the predicate
$\langle\lambda x.\neg Sx\rangle$ (is not a sexagenarian). Predicate
abstraction allows us to control the scope of negation and thereby
distinguish two senses of (4), using $S$ as the only primitive predicate.
Augmenting modal languages with predicate abstraction is not a new
idea, but its usefulness has not been fully exploited.%
\footnote{Modal languages with a predicate abstraction operator can be found
in Stalnaker and Thomason \cite{Stalnaker1968}, Thomason and Stalnaker
\cite{Thomason1968}, Fitting and Mendelsohn \cite{Fitting1998},
and Fitting \cite{Fitting2002a}, but none of the logics discussed
by these authors are seriously actualistic. Similarly, the non-modal
logic studied by Lambert and Bencivenga in \cite{Lambert1986} contains
a predicate abstraction operator, but it is not seriously actualistic. %
} The first-order modal system developed here contains a predicate
abstraction operator, and it embodies serious actualism in the manner
just described. I'll focus on the version of this system based on
the propositional modal logic T, which I call SAT (seriously actualistic
T), but the results obtained apply to languages based on several other
propositional modal logics.
The second, and more difficult problem facing the serious actualist
in developing a system worthy of being called a logic involves uniform
substitution. The result of substituting a complex predicate for each
occurrence of a simple predicate in a logically true sentence should
also be logically true. In section 5.1 I show that when complex predicates
are defined using predicate abstraction uniform substitution does
indeed preserve logical truth in SAT. But none of the work on serious
actualism of which I am aware deals with this matter fully and
satisfactorily.%
\footnote{Systems that are seriously actualistic with respect to
\emph{atomic}
sentences have been studied by Fine \cite{fine_k:1981a}, Jager
\cite{jager_t:1982a}
and \cite{Jager1988}, Menzel \cite{menzel:1991a}, and Stephanou
\cite{Stephanou2002} and \cite{stephanou:2005}. But because these
systems lack a predicate abstraction operator, none of them support
uniform substitution. In \cite{Stalnaker1977}, however, Stalnaker
gives a subtle and insightful discussion of logical form in a first-order
non-modal language supplemented with a predicate abstraction operator.
He also discusses a seriously actualistic modal extension of this
logic, emphasizing the importance of the scope of the abstraction
operator in determining the logical form of a sentence. And he suggests
(pp. 335-336), but does not prove, that in this modal extension uniform
substitution preserves logical truth. Stalnaker further explores this
same logic in \cite{Stalnaker1995}, which is reprinted with minor
changes in \cite{Stalnaker2003}. I discuss his work in section 6.2.%
}
It is hard to over-emphasize the importance of uniform substitution.
There is nearly universal agreement among logicians that a formal
system is not a logic unless it respects logical form in this way.
The reason that seriously actualistic modal systems have not been
more widely studied is probably that they appear not to support uniform
substitution. But this is only because attention has been focused
on languages that lack a means of properly handling predication. In
such languages uniform substitution does indeed fail to preserve logical
truth. This was noticed by Kripke at the very beginning of the modern
semantic study of modal logic:
\begin{quotation}
It is natural to assume that an \emph{atomic} predicate should be
\emph{false} in a world \emph{H} of all those individuals not existing
in that world; that is, that the extension of a predicate letter must
consist of actually existing individuals. ... We have chosen not to
do this because the rule of substitution would no longer hold; theorems
would hold for atomic formulae which would not hold when the atomic
formulae are replaced by arbitrary formulae. (This answers a question
of Putnam and Kalmar.)%
\footnote{\cite{kripke:1963b}, p. 86, emphasis in the original.%
}
\end{quotation}
Kripke's insight can be illustrated using sentences that express existential
generalization, such as
\begin{description}
\item [{(5)}] $Fa\rightarrow\exists xFx$
\end{description}
and
\begin{description}
\item [{(5{*})}] $\neg Fa\rightarrow\exists x\neg Fx$.
\end{description}
If we adopt the view that Kripke says ``is natural to assume'',
(5) is valid but (5{*}) is not. If\emph{ a} does not denote at a world
and the extension of \emph{F} is the entire domain of that world,
$\neg Fa$ is true but $\exists x\neg Fx$ is false. So if we make
the natural assumption that primitive predicates behave in accordance
with serious actualism, we must accept the unnatural result that complex
predicates do not. Uniform substitution fails.
In section 5.1, however, I show that when a complex predicate abstract
replaces each occurrence of a primitive predicate abstract in a sentence,
logical truth is preserved. So if $\phi(y)$ is any formula with free
occurrences of \emph{y} (but no free occurrence of any other variable)
every instance of
\begin{description}
\item [{(6)}] $\langle\lambda y.\phi(y)\rangle(a)\rightarrow\exists
x\langle\lambda y.\phi(y)\rangle(x)$
\end{description}
is valid.
Just as predicate abstraction facilitates a plausible account of serious
actualism, so an actuality connective ($\mathbf{\mathsf{A}}$) facilitates
the expression of actualism itself.%
\footnote{Modal languages augmented with an actuality connective have been
widely
studied. See, for example, Hodes \cite{Hodes1984c}, \cite{Hodes1984a},
and more recently Gilbert and Mares \cite{Gilbert2012}. %
} Letting $\mathsf{\mathcal{E}}(x)$ abbreviate $\exists y(y=x)$,
actualism can be formalized as
\begin{description}
\item [{(7)}] $\forall x\mathsf{A}\mathsf{\mathcal{E}}(x)$.
\end{description}
Although (7) is not valid, it is true. That is, it is true at the
actual world element of the intended model of SAT, which is defined
in section 7. Indeed (7) is knowable \emph{a priori}. For I know,
independently of experience, that I and all my surroundings are part
of the actual world. Hence I know that everything actually exists.%
\footnote{I've discussed formulas of propositional logic with a structure
similar
to that of (9) in \cite{Authora} and \cite{Author}.%
} There is a tableau for (7) in section 8.3.7 that illustrates this
point.
It is also worth noting that since SAT contains $\mathbf{\mathsf{A}}$
it is able to capture the content of sentences that cannot otherwise
be expressed in first-order modal languages. An example is
\begin{description}
\item [{(8)}] There might have been something that doesn't actually exist,
\end{description}
which can be rendered
\begin{description}
\item [{(9)}] $\lozenge\exists x\neg\mathsf{A}\mathsf{\mathcal{E}}(x)$.
\end{description}
Without an actuality connective, there is no way to express (8) in
a first-order modal language.%
\footnote{See Hodes \cite{Hodes1984b}, \cite{Hodes1984c},
\cite{Hodes1984a}.%
}
Several other features of SAT should be noted before delving into
the details. SAT is a version of free logic and as such has three
important features. First, as has already been stated, it makes all
attributive sentences with non-denoting singular terms false. Hence,
second, unrestricted universal instantiation is not valid. One cannot
infer the formal analogue of (2) from that of
\begin{description}
\item [{(10)}] Everyone enjoys messing about in boats.
\end{description}
Third, SAT allows models in which quantifiers range over the empty
domain. So no existentially quantified sentence is a logical truth,
and all inferences from a universal sentence to the corresponding
existential sentence are invalid.%
\footnote{In logicians\textquoteright{} jargon SAT is a negative universally
free logic. It is free because (as is now common) primitive predicates
may have a null extension and because universal instantiation for
individual quantifiers is not valid, universally free because it includes
interpretations in which individual quantifiers range over the empty
domain, and negative because atomic sentences containing non-denoting
singular terms are always false. For these terms, and a comprehensive
account of free logic, see Lambert \cite{Lambert2003}, especially
pp. 124-127, and 131.%
}
To summarize, and to provide some additional information as a guide
to the details that follow, SAT has the following noteworthy features.
\begin{itemize}
\item The object language contains the usual symbols of a first-order modal
language plus a predicate abstraction operator ($\lambda$) and an
actuality connective ($\mathsf{A}$).
\item Names are non-rigid. SAT is thus a contingent identity system. An
identity statement containing two names may be true at some worlds
and false at others.
\item A name need not denote at each world. Indeed a name need not denote
at any world.
\item If a name denotes at a world, it denotes an object that exists in
that world. This makes an actualistic interpretation possible. Indeed
the sentence $\forall x\mathsf{A}\mathsf{\mathcal{E}}(x)$, which
expresses the core tenet of actualism, is true in the intended model.
\item An atomic sentence is false at a world unless all the terms it
contains
denote objects in the domain of that world. Since identity is a primitive
predicate, this holds for identity sentences. And since names need
not denote, even a self-identity sentence can be false at a world.
Thus no self-identity sentence is a logical truth.
\item Far from being a flaw, the fact that self-identity sentences are not
logically true is an advantage. For it avoids the result that $\exists
y\square(y=a)$
is a truth of logic without artificially restricting necessitation
or existential generalization.
\item The extension of a predicate abstract at a world, like that of a
primitive
predicate, is restricted to objects that exist in that world. Thus
SAT embodies serious actualism. All sentences of the form $\forall
x\square(\langle\lambda y.\phi\rangle(x)\rightarrow\mathsf{\mathcal{E}}(x)$)
are logical truths.
\item There are models in which some or all worlds have empty domains. (In
the latter case the domain of the entire model is also empty).
\item The actual world element of a model plays no special role in the
definitions
of validity and logical consequence. Validity is thus general validity,
truth at every world in every model.
\end{itemize}
In sections 2-4 I present the syntax and semantics of SAT. Section
5 contains important semantic metatheorems, including Uniform Substitution
and Replacement (substitution of logically equivalent sub-formulas).
Section 6 compares SAT with the work of others, and section 7 presents
an actualistic account of truth. Section 8 contains semantic tableau
proof rules and some examples of their application. Section 9 is a
brief conclusion. In the Appendix (section 10) I prove the tableau
proof rules sound and complete with respect to validity as defined
for SAT. These proofs extend straightforwardly to several related
systems.
\section{Syntax}
The language under consideration, \emph{$\mathfrak{L}$}, is a first-order
modal language supplemented with a predicate abstraction operator
and an actuality connective.
\subsection{Symbols}
The non-logical symbols of \emph{$\mathfrak{L}$} are \emph{individual
constants} (names) and \emph{predicate constants} (predicates). The
former are the lower case letters \emph{a} through \emph{j}; the latter
are the upper case letters \emph{A} through \emph{Z}.%
\footnote{Subscripts can be used to insure an infinite supply of names and
predicates;
superscripts to indicate the arity of predicates. In practice I'll
have no need for subscripts, and I'll let context indicate arity.
The lower case letters `\emph{k}' through `\emph{t}' are reserved
for use in tableau proofs. See section 6.%
} The logical symbols are the \emph{variables}, which are the lower
case letters \emph{u} through \emph{z}%
\footnote{The remark made in the previous footnote about individual
constants
and subscripts applies also to variables.%
}, plus the following symbols
\[
\neg\,\,\,\,\wedge\,\,\,\,\vee\,\,\,\,\rightarrow\,\,\,\,\leftrightarrow\,\,\,\,\square\,\,\,\,\lozenge\,\,\,\,\mbox{\ensuremath{\forall}}\,\,\,\,\exists\,\,\,\,=\,\,\,\,\mathsf{A\,\,\,\,}\lambda\,\,\,\,.\,\,\,\,\langle\:\,\,\,\rangle\,\,\,\,(\,\,\,\,)
\]
The first ten of these are the usual truth-functional and modal connectives,
quantifiers, and the identity predicate. The next two are the actuality
connective and the abstraction operator. The remaining five are punctuation
marks. The term \emph{term} applies to both individual constants and
variables.
\subsection{Formulas and Sentences}
Formulas and sentences of \emph{$\mathfrak{L}$} are as usual. An\emph{
atomic formula} is either an \emph{n}-ary predicate followed by \emph{n}
terms, or the identity sign flanked by two terms (the whole being
enclosed in parentheses). All occurrences of variables in atomic formulas
are \emph{free occurrences}. Thus the following are atomic formulas
\[
Bx\,\,\,\, Gxy\,\,\,\,(z=c)\,\,\,\, Xzyz\,\,\,\, Gyb\,\,\,\,(d=h)\,\,\,\,
Xaab\,\,\,\,(b=b),
\]
and all the occurrences of variables in them are free. The notions
of\emph{ formula}, \emph{free occurrence of a variable in a formula},
and \emph{predicate abstract} are defined simultaneously, as follows.
\begin{description}
\item [{1.}] Every atomic formula is a formula, and every occurrence of
a variable in an atomic formula is a free occurrence.
\item [{2.}] If $\phi$ is a formula, so are $\neg\phi,$ $\square\phi,$
$\lozenge\phi,$ and $\mathsf{A}\phi.$ The free occurrences of variables
in these formulas are the same as those in $\phi.$
\item [{3.}] If $\phi$ and $\psi$ are formulas, so are $(\phi\wedge\psi),$
$(\phi\vee\psi),$ $(\phi\rightarrow\psi),$ and $(\phi\leftrightarrow\psi).$
The free occurrences of variables in these formulas are the same as
those in $\phi$ together with those in $\psi.$
\item [{4.}] If $\phi$ is a formula, $\alpha$ is a variable, and $\alpha$
has at least one free occurrence in $\phi$, then $\forall\alpha\phi$
and $\exists\alpha\phi$ are formulas. The free occurrences of variables
in these formulas are the same as those in $\phi,$ except for occurrences
of $\alpha.$%
\footnote{Clauses 4 and 5 do not allow vacuous quantification or predicate
abstraction.
There is no point in allowing either, and vacuous quantification yields
anomalies when empty domains are allowed. For example, although $\forall
xFx\rightarrow Fa$
is false if the domain of quantification is empty, $\forall y(\forall
xFx\rightarrow Fa)$
is true. %
}
\item [{5.}] If $\phi$ is a formula, $\alpha$ is a variable, and $\alpha$
has at least one free occurrence in $\phi$, then
$\langle\lambda\alpha.\phi\rangle$
is a \emph{predicate abstract}. The free occurrences of variables
in $\langle\lambda\alpha.\phi\rangle$ are the same as those in $\phi,$
except for occurrences of $\alpha$.
\item [{6.}] If $\langle\lambda\alpha.\phi\rangle$ is a predicate abstract
and $\tau$ is a term, $\langle\lambda\alpha.\phi\rangle(\tau)$ is
a formula. The free occurrences of variables in
$\langle\lambda\alpha.\phi\rangle(\tau)$
are the same as those in $\langle\lambda\alpha.\phi\rangle$ together
with those in $\tau$.%
\footnote{A variable occurs free in a term $\tau$ only if $\tau$ \emph{is}
a variable. Clause 6 is stated so as to facilitate expansion of the
class of terms to include function symbols and description operators. %
}
\end{description}
Any occurrence of a variable in a formula that is not free is \emph{bound}.
A formula in which all occurrences of variables are bound is a
\emph{sentence}.
It will be convenient, in what follows, to have a way of abbreviating
formulas involving iterated predicate abstraction. Consider a formula
of the form
\[
\langle\lambda\alpha_{1}.\langle\lambda\alpha_{2}.\langle\lambda\alpha_{3}.\phi\rangle(\tau_{3})\rangle(\tau_{2})\rangle(\tau_{1}),
\]
where $\alpha_{1},\alpha_{2},$ $\alpha_{3}$ are variables,
$\tau_{1},\tau_{2},$
$\tau_{3}$ are terms, and $\phi$ is a formula. Such formulas will
be abbreviated as
\[
\langle\lambda\alpha_{1},\alpha_{2},\alpha_{3}.\phi\rangle(\tau_{1},\tau_{2},\tau_{3})
\]
Similar abbreviations will be used for formulas containing different
numbers of iterated predicate abstracts.
\section{Semantics}
The logic I present in this paper is a seriously actualistic quantified
modal logic whose underlying propositional modal logic is the system
T. Hence its name, SAT. Its semantic framework will be familiar to
those who know Kripke-style modal semantics, and especially familiar
to those who know Fitting and Mendelsohn's \cite{Fitting1998} presentation
of it. Indeed only small changes in Fitting and Mendelsohn's definitions
of basic semantic notions are sufficient to yield SAT.%
\footnote{The Fitting and Mendelsohn \cite{Fitting1998} system to which SAT
is most similar is the one they develop in chapter 11. %
} But small differences in semantic details can make a big difference
in the resulting logic, and this is the case with SAT.
Although in what follows I confine attention to SAT, similar proof
techniques are readily available, and similar metatheorems hold, when
the underlying modal propositional logic is changed to K, B, S4, or
S5. Especially noteworthy among these metatheorems are uniform substitution
and substitutivity of equivalents (section 5) and soundness and completeness
of the tableau rules (section 10). I call the systems in question
SAK, SAB, SAS4, and SAS5. In what follows I'll periodically remind
the reader that what is being proved applies also to them.
The fundamental semantic notions are those of \emph{model},\emph{
interpretation},\emph{ valuation},\emph{ satisfaction}, \emph{truth},
\emph{validity}, and \emph{consequence}.
\subsection{Models}
A \emph{model} is a quintuple $\mathit{\mathrm{\mathcal{M=\langle
W\mathrm{,}\mathrm{@,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
where $\mathcal{W}$ is a non-empty set,
$@\in\mathcal{\mathcal{\mathcal{W}}}$,
$\mathcal{R}$ is a reflexive binary relation on $\mathcal{W}$, $\mathcal{D}$
is a function from members of $\mathcal{W}$ to (possibly empty) sets
(all of which are disjoint from $\mathcal{W}$), and $\mathcal{I}$
assigns extensions to non-logical symbol of the language at members
of $\mathcal{W}$.
$\mathcal{D_{M}}=\bigcup\{\mathcal{D}(w_{i})|w_{i}\in\mathcal{W}$\},
the union of the sets of individuals assigned to members of $\mathcal{W}$
by $\mathcal{D}$, is called \emph{the domain of the model}
$\mathcal{M}$\emph{.
}The intuitive idea, of course, is that $\mathcal{W}$ is a set of
worlds, @ is the actual world, $\mathcal{R}$ is the relative possibility
relation among worlds, $\mathcal{D}$ assigns to each world the (possibly
empty) set of individuals that exist in it, $\mathcal{I}$ is an
interpretation
of the non-logical symbols of the language, and $\mathcal{D_{M}}$
is the set of all actual and possible individuals. Notice that this
definition allows the domain of a model, $\mathcal{D_{M}}$, to be
empty.
\subsection{Interpretations}
An interpretation $\mathcal{I}$ is a function that assigns individuals
to individual constants and sets of ordered \emph{n}-tuples of individuals
to \emph{n}-ary predicates, both assignments being relative to a member
of $\mathcal{W}$. $\mathcal{I}$ is not required to assign anything
to an individual constant at a world, but if it does, the individual
so assigned must exist at that world. Similarly, $\mathcal{I}$ requires
the extension of an \emph{n}-ary predicate at a world to contain only
\emph{n}-tuples of individuals that exist at that world. This holds
for all predicates, including the identity predicate. (So if the individual
constant \emph{d} fails to denote at a world, even ($d=d$) is false
at that world.) It is these two features of \emph{$\mathcal{I}$ }that
make the object language actualistic and seriously actualistic,
respectively,
and thereby distinguish it from most other quantified modal logics.
More precisely, an \emph{interpretation} $\mathcal{I}$ of a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
is the union of a (perhaps partial) function on individual constants
and members of $\mathcal{W}$ and a total function on predicate constants
and members of $\mathcal{W}$ such that:
\begin{description}
\item [{1.}] For an individual constant $\iota$, and a world
$w\in\mathcal{W},$
if $\mathcal{I\mathrm{(}}\iota,w)$ is defined,
$\mathcal{I\mathrm{(}}\iota,w)\in\mathcal{D}(w)$.%
\footnote{Thus an interpretation needn't assign anything to any individual
constant
at any world. In models in which $\mathcal{D}(w)$ is empty, this
will always be the case. %
}
\item [{2.}] For each \emph{n}-ary predicate $\theta$ and each
$w\in\mathcal{W}$,
$\mathcal{I\mathrm{(}}\theta,w)$ is a set of ordered \emph{n}-tuples
of elements of $\mathcal{D\mathrm{(}}w)$. Specifically, if $\theta$
is `$=$', $\mathcal{I\mathrm{(}}\theta,w)$ is the identity relation
on $\mathcal{D\mathrm{(}}w)$.%
\footnote{If $\mathcal{D\mathrm{(}}w)$ is empty, all predicates, including
`$=$', are assigned the null set at $w.$%
}
\end{description}
These two clauses embody actualism and serious actualism, respectively.%
\footnote{The serious actualism embodied in clause 2 is exactly the same as
that of Menzel and Stephanou. (See clause (M2) on p. 361 of Menzel
\cite{menzel:1991a} and the definition of a model in Stephanou
\cite{Stephanou2002},
p. 197 and \cite{stephanou:2005}, p. 383.) But the actualism of clause
1 is more liberal than that of either. In his preferred system, G,
Menzel limits the denotations of individual constants to objects in
the domain of the real-world element of a model. (See clause
(M$1{}^{\prime}$)
on p. 361 \cite{menzel:1991a}.) Stephanou does the same on the previously
referenced pages. The actualism of SAT, on the other hand, allows
individual constants to denote different objects at different worlds,
requiring only that an object denoted at a world be a member of the
domain of that world. Thus it allows, but does not require, individual
constants to function like definite descriptions, referring to nothing
in the actual world but to ``something'' in some other possible
world. Although the previous sentence may sound incompatible with
actualism, I argue in section 7 that the idea behind it can be given
an entirely actualistic expression. %
}
\subsection{Valuations of Variables; Designations of Terms}
Three more semantic functions must be defined before I can define
satisfaction.
First, a \emph{valuation $\mathcal{V}$} relative to a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
is a (total) function from the set of variables of the language into
$\mathcal{D_{M}}$. (Thus if $\mathcal{D_{M}}$ is empty, \emph{$\mathcal{V}$
}is the null set\emph{.})
Next, where $\mathit{\mathcal{V}}$ and \emph{$\mathcal{U}$} are
valuations relative to a model $\mathit{\mathrm{\mathcal{M=\langle
W\mathrm{,}\mathrm{@,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
$w\in W,$ $\alpha$ is a variable, and $\mathcal{D\mathrm{(}}w)$
is not empty, $\mathcal{U}$ is an $\alpha$\emph{-variant-at-}$w$\emph{
}of $\mathit{\mathcal{V}}$ if $\mathit{\mathcal{V}}$ and
\emph{$\mathcal{U}$}
differ at most in what they assign to $\alpha,$ and\emph{
$\mathcal{U}(\alpha)\in\mathcal{D\textrm{(\ensuremath{w})}}$}.
(If \emph{$\mathcal{D\mathrm{(}}w)$} is empty, the term is undefined
and hence no valuation is an $\alpha$\emph{-}variant-at-$w$ of
$\mathit{\mathcal{V}}.$)
Finally, I define \emph{the designation of a term }at a world of a
model relative to a valuation\emph{.} Recall that a term may be either
a variable or an individual constant. Since it is models (via their
constituent interpretations) that assign designations to individual
constants, but valuations that assign designations to variables, it
will be convenient to have a single notation that expresses the designation
of a term. For this purpose I adopt the notation
$(\mathcal{V}\star\mathcal{I})(\tau,w)$
of Fitting and Mendelsohn. Where $\mathit{\mathcal{V}}$ is a valuation
relative to a model $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
$w\in\mathcal{W},$ and $\tau$ is a term
\begin{description}
\item [{1.}] If $\tau$ is a variable,
$(\mathcal{V}\star\mathcal{I})(\tau,w)=\mathcal{V}(\tau)$.
\item [{2.}] If $\tau$ is an individual constant, and
$\mathcal{I\mathrm{(}}\tau,w)$
is defined,
$(\mathcal{V}\star\mathcal{I})(\tau,w)=\mathcal{I\mathrm{(}}\tau,w)$.
Otherwise $(\mathcal{V}\star\mathcal{I})(\tau,w)$ is undefined.
\end{description}
Notice that under these definitions variables designate rigidly, but
individual constants are allowed to designate non-rigidly.
\subsection{Satisfaction and Satisfiability}
The definition of \emph{satisfaction} is now straightforward. First,
abbreviate valuation\emph{ $\mathcal{V}$} \emph{satisfies} formula
$\phi$ at world $w$ of model $\mathcal{M}$ as
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$,
and valuation\emph{ $\mathcal{V}$} \emph{does not satisfy} formula
$\phi$ at world $w$ of model $\mathcal{M}$ as
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
Satisfaction of a formula $\phi$ relative to a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
a valuation $\mathit{\mathcal{V}}$, and a world
$\mathit{w}\in\mathcal{\mathcal{\mathcal{W}}},$
is defined as follows (where $\theta$ is an \emph{n}-ary predicate,
$\alpha$ is a variable, $\tau$ and $\tau_{1},...,\tau_{n}$ are
terms, and $\phi$, $\chi$, and $\psi$ are formulas).
\begin{description}
\item [{1.}] If $\phi$ is the atomic formula $\theta\tau_{1}...\tau_{n}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\langle(\mathcal{V}\star\mathcal{I})(\tau_{1},w),...,(\mathcal{V}\star\mathcal{I})(\tau_{n},w)\rangle\in\mathcal{I\mathrm{(}}\theta,w)$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$%
\footnote{Clause 1 includes the case where $\theta$ is `$=$' and $\phi$
is $(\tau_{1}=\tau_{2})$. %
}
\item [{2.}] If $\phi$ is $\neg\psi$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$
; otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{3.}] If $\phi$ is $(\psi\wedge\chi)$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
and
$\mathcal{M}_{\mathcal{V}}\mathrm{(\chi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{4-6.}] The clauses for `$\vee$' , `$\rightarrow$', and
`$\leftrightarrow$'
are similar (with obvious modifications) to clause 3.
\item [{7.}] If $\phi$ is $\square\psi,$
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w^{*}})}=\mathrm{\textrm{1}}}}$
for all $\mathit{w^{*}}\in\mathcal{W}$ such that
$w\mathcal{R}\mathit{w^{*}}$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{8.}] If $\phi$ is $\lozenge\psi,$
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w^{*}})}=\mathrm{\textrm{1}}}}$
for at least one $\mathit{w^{*}}\in\mathcal{W}$ such that
$w\mathcal{R}\mathit{w^{*}}$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{9.}] If $\phi$ is $\mathsf{A}\psi$ ,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if $\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{@
)}=\mathrm{\textrm{1}}}}$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{10.}] If $\phi$ is $\forall\alpha\psi$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
for all valuations $\mathcal{U}$ that are $\alpha$-variants-at-$w$
of $\mathcal{V}$; otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
\item [{11.}] If $\phi$ is $\exists\alpha\psi$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
for at least one valuation $\mathcal{U}$ that is an $\alpha$-variant-at-$w$
of $\mathcal{V}$; otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
\item [{12a.}] If $\phi$ is $\langle\lambda\alpha.\psi\rangle(\tau)$,
$(\mathcal{V}\star\mathcal{I})(\tau,w)$ is defined, and
$(\mathcal{V}\star\mathcal{I})(\tau,w)\in\mathcal{D\textrm{(\emph{w})}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$
if
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$,
where $\mathcal{U}$ is the $\alpha$-variant-at-$w$ of $\mathcal{V}$
such that $\mathcal{U}(\alpha)=(\mathcal{V}\star\mathcal{I})(\tau,w)$;
otherwise
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}.$
\item [{12b.}] If $\phi$ is $\langle\lambda\alpha.\psi\rangle(\tau)$
and either $(\mathcal{V}\star\mathcal{I})(\tau,w)$ is undefined or
$(\mathcal{V}\star\mathcal{I})(\tau,w)\notin\mathcal{D\textrm{(\emph{w})}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
\end{description}
A set of formulas $\Sigma$ \emph{is satisfiable} if and only if there
is a model $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}},$
a valuation $\mathcal{V}$ relative to $\mathcal{M},$ and a world
$w\in\mathcal{W},$ such that for each formula $\sigma_{i}\in\Sigma$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\sigma_{i},\mathcal{\mathrm{\mathit{w})}=}}1$.
A formula $\phi$ is \emph{satisfiable} if and only if $\{\phi\}$
is satisfiable.
\subsection{Truth at a World in a Model; Truth in a Model}
As in the standard Tarskian approach to semantics, a sentence of SAT
is satisfied by a valuation at a world in a model just in case it
is satisfied by all such valuations. Truth and falsity for sentences
can thus be defined in the usual way. A sentence $\phi$ is \emph{true}
\emph{at world} $w$ of model $\mathcal{M}$ iff all valuations
\emph{$\mathcal{V}$
}relative to $\mathcal{M}$\emph{ }satisfy\emph{ }$\phi$ at $w$.
Similarly, $\phi$ is \emph{false} \emph{at world }$w$ of $\mathcal{M}$
iff no valuation \emph{$\mathcal{V}$ }relative to $\mathcal{M}$
satisfies $\phi$ at $w$. A sentence $\phi$ is \emph{true} \emph{in
model} $\mathcal{M}$ iff $\phi$ is true at world\emph{ }$\mathrm{@}$
of $\mathcal{M}$.
Notice that truth and falsity are defined only for sentences. This
is deliberate. Extending these definitions so that they apply to all
formulas would not be a harmless change. It would be tantamount to
introducing \emph{possibilist} universal quantifiers (quantifiers
that range over the domain of a model) and allowing them to stand
at the beginnings of sentences. Such quantifiers flout the fundamental
principle of actualism. And defining truth in this way can lead to
serious confusion, as was shown by Kripke \cite{kripke:1963b} in
his refutation of an alleged proof of the converse Barcan formula
given by Prior.%
\footnote{Fine has shown in his ``Postscript'' to \cite{Prior1977}, pp.
142-145
(reprinted in \cite{Fine2005}, pp. 154-156), that when a modal logic
with world-relative quantifiers, like SAT, is supplemented with Vlach
connectives possibilist quantifiers can be defined. (See \cite{Vlach1973}.
One Vlach connective is like the actuality connective, but more fine-tuned.
When applied to a formula within the scope of a modal connective,
it shifts evaluation back to the world in which the modal connective
was evaluated, not back to the actual world. The second Vlach connective
keeps track of worlds in which shifts caused by the first Vlach connective
are initiated.) Although possibilist quantifiers are rejected by actualists,
introducing them as primitive or defining them using the Vlach connectives
makes them explicit. It is preferable to allowing them to creep into
the language disguised as free variables. %
}
\subsection{Validity, Consequence, and Equivalence}
Definitions of validity, logical consequence, and logical equivalence,
again only for sentences, can now be given in the standard way. (These
definitions apply to SAK, SAB, SAS4, and SAS5, as well as to SAT.)
A sentence $\phi$ is \emph{valid} (abbreviated $\mathrm{\vDash\phi}$)
iff it is true at every world of every model.\noun{ }A sentence $\phi$
is a \emph{logical consequence} of a set of sentences $\Gamma$ (abbreviated
$\mathrm{\Gamma\vDash\phi}$) iff for every world in every model,
if each member of $\Gamma$ is true at that world so is $\phi$. Two
sentences $\phi$ and $\phi'$ are \emph{logically equivalent} iff
$\vDash(\phi\leftrightarrow\phi')$.
The notion of validity just defined (truth at each world of each model)
is called \emph{general validity}. It should not be confused with
the weaker notion of \emph{real world validity}, which requires only
truth at the actual-world element, @, of each model. Elsewhere I have
argued that general validity better captures our intuitive notion
of logical truth.%
\footnote{See \cite{Authora}, \cite{Author}. These two kinds of validity
were
first distinguished by Davies and Humberstone \cite{Davies1980} and
have received much discussion. For an object language that does not
contain an actuality connective (or any other logical operator that
makes special reference to a designated world) they coincide. %
}
The reasons for the validity or invalidity of sample sentences given
in subsequent sections should not be difficult to understand if one
keeps in mind three major features of SAT. First, individual constants
are non-rigid. They are free to designate different objects, or no
object at all, in different worlds. Second, both primitive predicates
and predicate abstracts are false at a world of an object that does
not exist at that world (and false of an $n$-tuple of objects unless
all $n$ objects exist at the world). Third, quantification is
world-relative.
The introduction of tableau proofs in a later section may help provide
greater insight into the workings of the semantics.
\section{Notable Features of the Semantics}
\subsection{Attributive Sentences}
We are now in a position to see how SAT handles the examples with
which we began in section 1. Consider a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
and a particular world $w\in\mathcal{W}$ such that $\mathcal{D\mathrm{(}}w)$
is not empty. For predicate constants \emph{S} and \emph{N}, and individual
constant \emph{d}, suppose that $\mathcal{I\mathrm{(}}S,w)$ and
$\mathcal{I\mathrm{(}}N,w)$
are non-empty subsets of $\mathcal{D\mathrm{(}}w)$,
$\mathcal{I\mathrm{(}}N,w)$
is the complement of $\mathcal{I\mathrm{(}}S,w)$ with respect to
$\mathcal{D\mathrm{(}}w)$, and
$\mathcal{I\mathrm{(}}d,w)\notin\mathcal{D\mathrm{(}}w).$
Then $\langle\lambda x.\neg Sx\rangle(d)$ and $\langle\lambda
x.Nx\rangle(d)$\noun{
}are both false at $w$ while $\neg\langle\lambda x.Sx\rangle(d)$
and $\neg\langle\lambda x.\neg Nx\rangle(d)$ are both true. If we
think of \emph{S}, \emph{N}, and \emph{d} as `is a sexagenarian',
`is a non-sexagenarian', and `Dweet', respectively, and \emph{w}
as the world of interest, we have formal representations of sentences
(4a) and (4b) of the Introduction. Since Dweet doesn't exist at \emph{w},
all attributive sentences involving `Dweet' are false, and the denials
of all such sentences are true.
Without predicate abstraction we would need both \emph{S} and \emph{N}
as primitive predicates in order to symbolize sentences (4a) and (4b).
For $Nd$ is false at \emph{w} while\noun{ }$\neg Sd$ is true.\noun{
}Predicate abstraction lets the serious actualist say what he wants
to say, whether a predicate or its complement is taken as primitive.%
\footnote{It may be tempting to think that the sort of difference noted in
this
section, in which the truth value of a sentence depends on whether
a negation sign is placed inside or outside a predicate abstract,
is due entirely to the fact that the sentences involved contain individual
constants. But this is not true. Consider the sentences $\exists
x\lozenge\langle\lambda y.\neg Sy\rangle(x)$
and $\exists x\lozenge\neg\langle\lambda y.Sy\rangle(x)$, and further
specify the model under consideration so that for every world
$\mathit{w^{*}}\in\mathit{\mathrm{\mathcal{W}}}$
such that $w\mathcal{R}\mathit{w^{*}}$,
$D\textrm{(\emph{\ensuremath{w^{*}}})}$
is disjoint from $D\textrm{(\emph{w})}$. The first sentence is false
at $w$ and the second true. %
}
\subsection{Identity}
Since individual constants may denote different objects at different
worlds (and need not denote anything at some or even any worlds),
SAT allows identity sentences to be true at some worlds and false
at others.%
\footnote{Individual constants can nevertheless be made to approximate rigid
designators using suitable assumptions. See section 6.2 for details. %
} It is thus a contingent identity logic. Adding this feature to serious
actualism entails that self-identity sentences are false at worlds
in which the individual constant involved does not denote. And as
the following paragraphs show, this in turn allows us to avoid having
as theorems of logic statements to the effect that $\iota$ necessarily
exists, for every individual constant $\iota$.
Exposition will be facilitated by defining an existence predicate,
$\mathsf{\mathcal{E}}$, that is true of an object at a world if and
only if the object exists at that world. For a term $\tau$, define
$\mathsf{\mathcal{E}}(\tau)$ as $\exists\alpha(\alpha=\tau)$, where
the variable $\alpha$ is distinct from $\tau$.%
\footnote{In the sentence schema given in this and subsequent sections
$\alpha,\alpha_{1},\alpha_{2},...,$
are variables, $\psi(\alpha),\psi(\alpha_{1}),\psi(\alpha_{2}),...,$
are formulas containing one or more free occurrences of the indicated
variable but no free occurrence of any other variable,
$\iota,\iota_{1},\iota_{2},...,$
are individual constants, and
$\psi(\iota),\psi(\iota_{1}),\psi(\iota_{2}),...,$
the results of substituting $\iota,\iota_{1},\iota_{2},...,$ for
each free occurrence of the indicated variable in
$\psi(\alpha),\psi(\alpha_{1}),\psi(\alpha_{2}),....$ %
}
Every sentence of the form
\begin{description}
\item [{(Id)}] $\forall\alpha(\alpha=\alpha)$
\end{description}
is valid, but claims of self identity that make use of individual
constants are not. Thus neither $d=d$ nor $\langle\lambda
x.(x=x)\rangle(d))$
is valid. Indeed both are false at world \emph{w} of the model $\mathcal{M}$
of section 4.1. And while all sentences of the forms
\begin{description}
\item [{($\mathrm{\square}$Id1)}]
$\forall\alpha(\alpha=\alpha\rightarrow\square(\mathcal{E}(\alpha)\rightarrow(\alpha=\alpha)))$,
\end{description}
\medskip{}
\begin{description}
\item [{($\mathrm{\square}$Id2)}]
$\forall\alpha_{1}\forall\alpha_{2}(\alpha_{1}=\alpha_{2}\rightarrow\square(\mathcal{E}(\alpha_{1})\rightarrow(\alpha_{1}=\alpha_{2})))$,
\end{description}
and
\begin{description}
\item [{(ND)}]
$\forall\alpha_{1}\forall\alpha_{2}(\alpha_{1}\neq\alpha_{2}\rightarrow\square(\alpha_{1}\neq\alpha_{2}))$
\end{description}
are valid, no sentence of the form
$\forall\alpha(\alpha=\alpha\rightarrow\square(\alpha=\alpha))$,
$\forall\alpha_{1}\forall\alpha_{2}(\alpha_{1}=\alpha_{2}\rightarrow\square(\alpha_{1}=\alpha_{2}))$,
or $\forall\alpha\square(\alpha=\alpha)$ is.%
\footnote{The label (ND), for necessity of distinctness, is borrowed from
Stalnaker
\cite{Stalnaker1995}. Necessity of distinctness is valid in SAT even
though none of the versions of necessity of identity listed here are. %
}
It is also noteworthy that existence claims and claims of self identity
are logically equivalent. That is, all instances of
\begin{quotation}
$\mathcal{E}(\iota)\leftrightarrow(\iota=\iota)$
\end{quotation}
are valid. And since the rule of necessitation preserves validity,
if $d=d$ were valid, then $\mathcal{E}(d)$ and $\mathcal{\square
E}(d)$\textemdash{}abbreviations
of $\exists x(x=d)$ and $\square\exists x(x=d)$\textemdash{}would
also be valid. Similarly for every individual constant in the language.
But surely we do not want to have all, or any, sentences of the form
\begin{description}
\item [{(NE)}] $\square\mathcal{E}(\iota)$
\end{description}
as theorems of logic. The consistent serious actualist avoids this
problem by unflinchingly applying her basic principle to self identities.
No sentence of the form
\begin{description}
\item [{(SI)}] $\iota=\iota$
\end{description}
is a logical truth.%
\footnote{This approach to identity, including the logical equivalence of
$\mathcal{E}(\iota)$
and $(\iota=\iota)$, is endorsed by Burge \cite{Burge1974}.%
}
Failure to take this principled step is not only inconsistent with
serious actualism, it leads to other difficulties. In Menzel's
\cite{menzel:1991a}
painstaking reconstruction of Prior's seriously actualistic modal
logic, all sentences of the form (SI) are valid, but no sentence of
the form (NE) is. Menzel achieves this result only by denying that
the rule of necessitation applies to (SI) or to valid sentences that
depend on it.%
\footnote{See \cite{menzel:1991a}, especially pp. 359-364.%
} But this seems \emph{ad hoc}.
So in SAT statements of self-identity and tautologies are not logically
equivalent. While in classical logic $d=d$ and $Sd\vee\neg Sd$ are
both logical truths, in SAT only the latter is. Similarly $\forall
x(Sx\vee\neg Sx)\rightarrow(Sd\vee\neg Sd)$
is valid, but $\forall x(x=x)\rightarrow(d=d)$ is not.%
\footnote{Kripke notes a closely related distinction in \cite{kripke:1963b},
p. 90.%
} The proper comparison is between $\langle\lambda y.(y=y)\rangle(d)$
and $\langle\lambda y.(Sy\vee\neg Sy)\rangle(d)$, which are logically
equivalent though not valid.
With respect to substitutivity of identicals, all sentences of the
forms
\begin{description}
\item [{(Sub1)}]
$(\iota_{1}=\iota_{2})\rightarrow(\langle\lambda\alpha.\phi(\alpha)\rangle(\iota_{1})\rightarrow\langle\lambda\alpha.\phi(\alpha)\rangle(\iota_{2}))$
\end{description}
and
\begin{description}
\item [{(Sub2)}]
$\forall\alpha_{1}\forall\alpha_{2}(\alpha_{1}=\alpha_{2}\rightarrow(\langle\lambda\alpha_{3}.\phi(\alpha_{3})\rangle(\alpha_{1})\rightarrow\langle\lambda\alpha_{3}.\phi(\alpha_{3})\rangle(\alpha_{2})))$
\end{description}
are valid, but not all sentences of the form
$((\iota_{1}=\iota_{2})\wedge\phi(\iota_{2}))\rightarrow\phi(\iota_{1})$
are. There are thus instances of the corresponding argument form in
which the conclusion is not a consequence of the premises.%
\footnote{An example of such an argument is
\begin{description}
\item [{(Gibb)}] $(g=l),\square(\exists
x(x=l)\rightarrow(l=l)\nvDash\square(\exists x(x=l)\rightarrow(g=l)$.
\end{description}
I call this argument (Gibb) because it plays a pivotal role in Gibbard's
argument (\cite{Gibbard1975}, pp. 200 ff) for contingent identity.
Gibbard's reasons for favoring a contingent identity logic are very
different from mine. I won't consider his work here except to note
that a crucial step in his argument is illuminated by the use of predicate
abstraction.
It is important for Gibbard's purposes that (Gibb) not be a valid
argument. He explains its invalidity as follows:
\begin{quote}
{[}The conclusion{]} follows from {[}the premises{]} by Leibniz' Law,
then, only if the context
\begin{quote}
$\square(\exists x(x=l)\rightarrow(\ldots=l)$
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~(7)
\end{quote}
attributes a property. We can block the inference to {[}the conclusion{]},
then, simply by denying that the context (7) attributes a property.
\end{quote}
Gibbard does not make use of predicate abstraction, but by its use
we can see more clearly what he means by ``attributing a property''.
The property he denies (7) attributes is expressible in my notation
as
\begin{quote}
$\langle\lambda y.\square(\exists x(x=l)\rightarrow(y=l)\rangle$
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~(7{*}).
\end{quote}
And in view of (Sub1) the following variant of (Gibb) \medskip{}
$(g=l),\langle\lambda y.\square(\exists
x(x=l)\rightarrow(y=l)\rangle(l)\vDash\langle\lambda y.\square(\exists
x(x=l)\rightarrow(y=l)\rangle(g)$
\medskip{}
is a valid argument. So from my perspective Gibbard's criticism of
(Gibb) amounts to denying that (7{*}) ``attributes a property''. %
}
\subsection{Quantifiers}
Quantification is world-relative in SAT, and primitive predicates
and predicate abstracts are true at a world only of objects that exist
at that world. Because of these two features some of the classical
principles involving quantifiers hold only in restricted forms.
Existential generalization in the form
\begin{description}
\item [{(EG)}]
$\langle\lambda\alpha_{2}.\psi(\alpha_{2})\rangle(\iota)\rightarrow\exists\alpha_{1}\langle\lambda\alpha_{2}.\psi(\alpha_{2})\rangle(\alpha_{1})$
\end{description}
is valid. Thus the sentences $\langle\lambda
x.Nx\rangle(d)\rightarrow\exists y\langle\lambda yNx\rangle y)$\noun{
}and $\langle\lambda x.\neg Sx\rangle(d)\rightarrow\exists y\langle\lambda
x.\neg Sx\rangle(y)$\noun{
}are valid, but not every sentence of the form
$\psi(\iota)\rightarrow\exists\alpha\psi(\alpha)$
is. For example $\neg Sd\rightarrow\exists x\neg Sx$ is not. Similarly,
not all instances of
$(\psi(\iota)\wedge\mathcal{E}(\iota))\rightarrow\exists\alpha\psi(\alpha)$
are valid. Although this schema is valid in standard non-modal free
logics, the presence of $\mathsf{\mathcal{E}}(\iota)$ in the antecedent
is not sufficient to guarantee validity when modal connectives are
available. The sentence $(\square Sd\wedge\mathcal{E}(d))\rightarrow\exists
x\square Sx$
is easily seen to be invalid.
When applied to predicate abstracts quantifiers do not exhibit their
usual dual properties. Thus in spite of the validity of (EG), not
all sentences of the form
\begin{quotation}
$\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\iota)$
\end{quotation}
are valid. Indeed
\begin{quotation}
$\forall x\langle\lambda y.Sy\rangle(x)\rightarrow\langle\lambda
y.Sy\rangle(d)$
\end{quotation}
is not. Even if the antecedent is true, \emph{d} must designate in
order for the consequent to be true.
Universal instantiation in the form
\begin{description}
\item [{(UI)}]
$\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow(\mathcal{E}(\iota)\rightarrow\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\iota))$,
\end{description}
however, is valid. And just as in the case of (EG) the use of predicate
abstraction in (UI) is essential, since not every sentence of the
form
$\forall\alpha_{1}\phi(\alpha_{1})\rightarrow(\mathcal{E}(\iota)\rightarrow\phi(\iota))$
is valid. The reader should have no difficulty finding a counterexample
to the sentence
\begin{description}
\item [{(\emph{faux}~UI)}] $\forall x\square
Sx\rightarrow(\mathcal{E}(d)\rightarrow\square Sd$).
\end{description}
There is a tableau for (\emph{faux} UI) in section 8.3.
\subsection{The Barcan and Converse Barcan Formulas}
SAT provides sensible treatments of the Barcan and Converse Barcan
Formulas. Consider first the following form of the Converse Barcan
Formula.
\begin{description}
\item [{(CBF)}]
$\exists\alpha_{1}\lozenge\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\lozenge\exists\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
\end{description}
(CBF) is valid, as seems entirely plausible. Evaluated at any world
\emph{w}, (CBF) says (roughly) that if there is an object in \emph{w}
that has a property in some possible world $\mathit{w'}$, then there
is a possible world in which some object has this property. Given
the antecedent, and given that according to serious actualism an object
can have a property at a world only if it exists in that world,
$\mathit{w'}$
as described is sufficient to make the consequent true. If an object
from \emph{w} has a property in $\mathit{w'}$, that object must exist
in $\mathit{w'}$.%
\footnote{Indeed similar reasoning shows that
$\exists\alpha_{1}\square\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\square\exists\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
is valid. %
}
Standard counterexamples to this form of the Converse Barcan Formula
assume that true predications can be made of objects at worlds in
which those objects do not exist.%
\footnote{In \cite{kripke:1963b} Kripke gives a counterexample to the
$\square\forall$-form
of the converse Barcan formula. It assumes that \emph{false} predications
using monadic predicates can be made of objects at worlds in which
those objects do not exist. And the semantics of \cite{kripke:1963b}
also allows the kind of counterexample given above to (CBF), an instance
of the $\exists\lozenge$-form of the converse Barcan formula, in
which \emph{true} predications using monadic predicates are made of
objects at worlds in which those objects do not exist. Yet in this
same paper Kripke expresses misgivings about this latter allowance,
as the passage quoted in section 1 above shows. %
} Serious actualism rejects this assumption. In so doing it provides
a plausible explanation of why these counterexamples so often seem
wrong to the uninitiated. They are wrong.
Of course the Converse Barcan Formula can also be expressed using
necessity and universal quantification. (CBF) is logically equivalent
to
\begin{quotation}
$\square\forall\alpha_{1}\neg\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\forall\alpha_{1}\square\neg\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$,
\end{quotation}
which is also valid. But in this form the fact that negations precede
predicate abstracts is crucially important. Not all sentences of the
form
\begin{description}
\item [{(\emph{faux}~CBF)}]
$\square\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\forall\alpha_{1}\square\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
\end{description}
are valid. Standard counterexamples apply. There are tableaus for
instances of (CBF) and (\emph{faux} CBF) in section 8.3.
It is worth noting that in \cite{Stalnaker1995} Stalnaker gives a
version of the Converse Barcan Formula that is entailed by, but does
not entail, (\emph{faux} CBF). Translated into my notation it is
\begin{description}
\item [{(Stal~CBF)}]
$\square\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\forall\alpha_{1}\langle\lambda\alpha_{2}.\square\phi(\alpha_{2})\rangle(\alpha_{1})$.
\end{description}
(Stal CBF) is not valid in SAT or in Stalnaker's system. For more
about the latter see section 6.2.
Turning now to the Barcan formula, it is not difficult to see that
both of the following formulations have invalid instances.
\begin{quotation}
$\lozenge\exists\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\exists\alpha_{1}\lozenge\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
$\forall\alpha_{1}\square\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\square\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
\end{quotation}
Standard counterexamples again apply.
\subsection{Extensionality of Predicate Abstraction}
Predicate abstraction in SAT is in a certain sense extensional, as
the following valid sentences show.
\begin{quotation}
$\forall z(\langle\lambda x.\langle\lambda
y.Fy\rangle(x)\rangle(z)\leftrightarrow\langle\lambda y.Fy\rangle(z))$
$\langle\lambda x.\langle\lambda
y.Fy\rangle(x)\rangle(d)\leftrightarrow\langle\lambda y.Fy\rangle(d)$
$\langle\lambda z,w.\langle\lambda
x,y.Rxy\rangle(z,w)\rangle(d,o)\leftrightarrow\langle\lambda
x,y.Rxy\rangle(d,o)$
$\forall u\forall v(\langle\lambda z,w.\langle\lambda
x,y.Rxy\rangle(z,w)\rangle(u,v)\leftrightarrow\langle\lambda
x,y.Rxy\rangle(u,v))$
\end{quotation}
If predicate abstracts are taken to represent properties, then having
a property and having the property of having that property are not
distinguished in the semantics. Similarly for relations.
\section{Some Important Semantic Metatheorems}
Since antiquity logicians have realized the importance of logical
form. If a sentence is logically true, then every sentence of the
same form is also logically true. In predicate logic this principle
manifests itself in the principle of uniform substitution for predicates.
Substituting the same complex predicate for each occurrence of a simple
predicate in a logically true sentence should yield another logical
truth. Yet seriously actualistic logics have commonly been thought
to violate this fundamental principle. In section 5.1 I show that
when predication is understood properly, using predicate abstraction,
uniform substitution of predicates does indeed preserve logical truth.
This holds for SAT and its kindred systems, and it is one of their
main advantages over other attempts to formalize seriously actualistic
modal logics.
Another important feature of SAT is that it supports a theorem (sometimes
called a replacement theorem) that sanctions substituting logically
equivalent sub-formulas for each other within a given formula. If,
in a formula, an occurrence of a sub-formula is replaced by a logically
equivalent formula, the result is logically equivalent to the original.
Of course such a theorem depends on an appropriate definition of logical
equivalence for \emph{formulas}. (The definition of logical equivalence
given in section 3.6 applies only to sentences.) In section 5.2 I
define logical equivalence for formulas and prove a replacement theorem.
Section 5.3 contains two theorems about validity and logical consequence
of sentences. Section 5.4 contains a deduction theorem.%
\footnote{All the results given in sections 5.1-5.4 for SAT hold as well for
SAK, SAB, SAS4, and SAS5.%
}
\subsection{Uniform Substitution for Predicate Abstracts}
If a sentence $\phi$ is logically true, then any sentence that results
from substituting a new predicate (simple or complex) for each occurrence
of a simple predicate in $\phi$ should be logically true as well.
Yet it appears that uniform substitution does not preserve logical
truth in seriously actualistic systems. For example, where \emph{F}
and $G$ are primitive predicates, although
\begin{quotation}
$\exists x\lozenge Fx\rightarrow\lozenge\exists xFx$
\end{quotation}
is valid in SAT,
\begin{quotation}
$\exists x\lozenge\neg Gx\rightarrow\lozenge\exists x\neg Gx$
\end{quotation}
is not.%
\footnote{In systems without predicate abstraction both of these sentences
count
as instances of the converse Barcan formula. By an argument similar
to the one given for (CBF) in section 4.4, the first sentence is valid
in SAK and hence in SAT, SAB, SAS4, and SAS5. But the second sentence
is invalid even in SAS5 and hence in the other systems. %
} Yet the second sentence has the same general form as the first, since
it results from substituting $\neg Gx$ for \emph{Fx}. I believe failure
of uniform substitution is the reason seriously actualistic systems
of quantified modal logic have not been widely studied.
Indeed Kripke cited this failure as a major problem very early in
the development of model-theoretic modal semantics. In section 1 I
quoted the salient passage from \cite{kripke:1963b}, one of his most
important and most frequently cited early papers. Yet if properly
understood, uniform substitution does preserve validity in seriously
actualistic systems.%
\footnote{As I mentioned in an earlier footnote Stalnaker
\cite{Stalnaker1977}
noticed this problem in a slightly different context. He gives an
interesting example on pp. 335-336, but there is no uniform substitution
theorem in \cite{Stalnaker1977} or his later \cite{Stalnaker1995}.
I discuss \cite{Stalnaker1995} in section 6.2.%
}
Proper understanding means taking predicate abstraction seriously
as the preferred means of expressing predication, and thus understanding
uniform substitution as substitution of a predicate abstract for each
occurrence of a primitive predicate abstract throughout a sentence.%
\footnote{By a primitive predicate abstract I mean one like $\langle\lambda
y.Fy\rangle$,
in which the formula following the dot is atomic.%
} For example, if we substitute $\langle\lambda y.\neg Gy\rangle$
for $\langle\lambda y.Fy\rangle$ throughout the valid sentence
\begin{description}
\item [{(11)}] $\exists x\square\langle\lambda
y.Fy\rangle(x)\rightarrow\square\exists x\langle\lambda y.Fy\rangle(x)$,
\end{description}
we obtain
\begin{description}
\item [{(12)}] $\exists x\square\langle\lambda y.\neg
Gy\rangle(x)\rightarrow\square\exists x\langle\lambda y.\neg Gy\rangle(x)$,
\end{description}
which is also valid. Theorem 1 shows that the foregoing is not an
isolated example.
\begin{description}
\item [{Theorem}] 1. Uniform Substitution for Predicate Abstracts (USPA)
\end{description}
Consider a sentence $\Phi$, an atomic formula
$\theta\alpha_{1}...\alpha_{n}$,
where $\alpha_{1},...,\alpha_{n}$ are distinct variables, and a formula
$\psi$. Suppose that each of the variables $\alpha_{1},...,\alpha_{n}$
has at least one free occurrence in $\psi$, and no other variable
occurs free in $\psi$. Suppose also that $\theta$ occurs in $\Phi$
only as part of the predicate abstract
$\langle\lambda\alpha_{1},...,\alpha_{n}.\theta\alpha_{1}...\alpha_{n}\rangle$,
and that $\Psi$ is the result of simultaneously substituting
$\langle\lambda\alpha_{1},...,\alpha_{n}.\psi\rangle$
for each occurrence of
$\langle\lambda\alpha_{1},...,\alpha_{n}.\theta\alpha_{1}...\alpha_{n}\rangle$
in $\Phi$. Under these conditions, if $\Phi$ is valid, then so is
$\Psi.$
Proof: Consider the case where $n=1$. To facilitate the proof I define
the extension of a unary predicate and the extension of a predicate
abstract at a world in a model. If $\theta$ is a unary predicate,
the \emph{extension of predicate }$\theta$ \emph{at world }$w$ \emph{in
model} $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
(abbreviated
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)$)
is $\mathcal{I\mathrm{(}}\theta,w)$. By the definition of an interpretation
(section 3.2)
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)\subseteq\mathcal{D\mathrm{(}}w)$.
If $\psi$ is a formula, $\alpha$ is a variable, $\alpha$ has at
least one free occurrence in $\psi$, and no variable other than $\alpha$
occurs free in $\psi$, the \emph{extension of predicate abstract
}$\langle\lambda\alpha.\psi\rangle$ \emph{at world }$w$ \emph{in
model} $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
(abbreviated
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha.\psi\rangle)$)
is \{$\mathcal{V}(\alpha)\mathcal{\mid
M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi\rangle(\alpha),\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$\},
where \emph{$\mathcal{V}$} ranges over all valuations relative to
$\mathit{\mathrm{\mathcal{M}}}$. By clause 12 in the definition of
satisfaction (section 3.4) it follows that
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha.\psi\rangle)\subseteq\mathcal{D\mathrm{(}}w)$.
Since $\theta$ is a unary predicate, $\theta\alpha$ is a formula.
So
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha.\theta\rangle)$
is \{$\mathcal{V}(\alpha)\mathcal{\mid
M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\theta\alpha\rangle(\alpha),\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$\},
where \emph{$\mathcal{V}$} ranges over all valuations relative to
$\mathit{\mathrm{\mathcal{M}}}$. It follows from the definition of
satisfaction (section 3.4) and the definition of
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)$
(above) that
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha.\theta\alpha\rangle)=Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)=\mathcal{I\mathrm{(}}\theta,w)$.
Now suppose $\Psi$ is invalid. Hence there is a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
a world $w\in\mathcal{W}$, and a valuation \emph{$\mathcal{V}$},
such that\emph{
}$\mathcal{M}_{\mathcal{V}}\mathrm{(\Psi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
Consider the model $\mathit{\mathrm{\mathcal{M\mbox{*}=\langle
W\mathrm{,}\mathrm{@,}R\mathrm{,}D\mathrm{,}I\mbox{*}\rangle}}}$,
which is exactly like $\mathit{\mathrm{\mathcal{M}}}$ except that,
for all $w*\in W$,
$\mathcal{I\mbox{*}}(\theta,w*)=Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w*}}}}}}}}(\langle\lambda\alpha.\psi\rangle)$.
Since
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w*}}}}}}}}(\langle\lambda\alpha.\psi\rangle)\subseteq\mathcal{D\mathrm{(}}w*)$,
$\mathit{\mathrm{\mathcal{I\mbox{*}}}}$ is well defined. A straightforward
induction on the complexity of $\Phi$ shows that
$\mathcal{M\mbox{*}}_{\mathcal{V}}\mathrm{(\Phi,\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{0}}}}$.
Hence $\Phi$ is invalid (in the same sense). The proof easily generalizes
to cases where $n>1$.%
\footnote{Where $n=2$, again define
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)$
as $\mathcal{I\mathrm{(}}\theta,w)$. Hence
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\theta)\subseteq\mathcal{D\mathrm{(}}w)\times\mathcal{D\mathrm{(}}w)$).
Define
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha{}_{1},\alpha{}_{2}.\psi\rangle)$
as \{$\mathcal{\langle
V}(\alpha{}_{1}),\mathcal{V}(\alpha{}_{2})\rangle\mid
M_{\mathcal{V}}\mathrm{(\langle\lambda\alpha{}_{1},\alpha{}_{2}.\psi\rangle(\alpha{}_{1},\alpha{}_{2}),\mathcal{\mathrm{\mathit{w})}=\mathrm{\textrm{1}}}}$\},
where \emph{$\mathcal{V}$} ranges over all valuations relative to
$\mathit{\mathrm{\mathcal{M}}}$. It follows that
$Ext_{\mathit{\mathit{\mathrm{\mathcal{M_{\text{\ensuremath{w}}}}}}}}(\langle\lambda\alpha{}_{1},\alpha{}_{2}.\psi\rangle)\subseteq\mathcal{D\mathrm{(}}w)\times\mathcal{D\mathrm{(}}w)$.
%
} $\blacksquare$
In addition to sanctioning the move from (13) to (14), USPA also allows
us to infer the validity of (16) and (17) from that of (15).
\begin{description}
\item [{(13)}] $\exists x\forall y\langle\lambda
u,v.Ruv\rangle(x,y)\rightarrow\forall y\exists x\langle\lambda
u,v.Ruv\rangle(x,y)$
\item [{(14)}] $\exists x\forall y\langle\lambda u,v.\neg\lozenge\exists
w(Fuw\wedge Gwv)\rangle(x,y)\rightarrow\forall y\exists x\langle\lambda
u,v.\neg\lozenge\exists w(Fuw\wedge Gwv)\rangle(x,y)$
\item [{(15)}] $\exists x\forall y\langle\lambda u,v.(\exists
w\langle\lambda z.\exists x\square Hxuz\rangle(w)\rightarrow\forall
w\langle\lambda z.\forall x\lozenge
Kxvz\rangle(w))\rangle(x,y)\rightarrow\forall y\exists x\langle\lambda
u,v.(\exists w\langle\lambda z.\exists x\square
Hxuz\rangle(w)\rightarrow\forall w\langle\lambda z.\forall x\lozenge
Kxvz\rangle(w))\rangle\rangle(x,y)$
\end{description}
The reader will be able to generate other examples of inferences sanctioned
by USPA.
\subsection{Replacement (Substitution of Equivalents)}
Well-behaved logics typically support a definition of logical equivalence
for formulas and a replacement theorem.%
\footnote{The definition of logical equivalence given in section 3.6 applies
only to sentences.%
} Such theorems generally guarantee that given a formula $\phi$, replacing
any subformula $\psi$ of $\phi$ by a formula $\psi'$ equivalent
to $\psi$, yields a formula $\phi'$ equivalent to the original $\phi$.%
\footnote{Since SAT bans vacuous quantifiers, the result of replacing an
occurrence
of $\psi$ by $\psi'$ in $\phi$ may not be a formula. (Let $\psi$,
$\psi'$, and $\phi$ be $Fx\vee\neg Fx$,\emph{ }$Fa\vee\neg Fa$,
and\emph{ }$\forall x(Fx\vee\neg Fx)$.) Hence the limitation of Theorem
2 below to those cases where $\phi'$ is a formula. %
} In non-modal first-order logic it is sufficient for this purpose
to declare formulas $\chi$ and $\chi'$ logically equivalent if
$\forall\alpha_{1}...\forall\alpha_{n}(\chi\leftrightarrow\chi')$
is valid, where $\alpha_{1},...,\alpha_{n}$ include all the variables
that have free occurrences in $\chi$ or $\chi'$. But such a definition
will not support substitution of equivalents for modal logics that
allow different worlds in a model to have different domains of individuals.
For these logics we need a stronger notion of logical equivalence.
For a formula $\phi$, let the $\forall\square$\emph{-closure of}
$\phi$ be any sentence formed by prefixing $\phi$ with a sequence
of interspersed universal quantifiers and necessity connectives. This
sequence may be of any finite length and the universal quantifiers
and necessity connectives may appear in any order. None of the quantifiers
may be vacuous, however, since vacuous quantifiers are banned by the
definition of a formula. A $\forall\square$-closure of a sentence
will consist of that sentence prefixed with zero or more necessity
connectives.
For a formula $\phi$ I write $\Vvdash\phi$ to indicate that every
$\forall\square$-closure of $\phi$ is valid, and I say that two
formulas $\psi$ and $\psi'$ are \emph{logically equivalent} if and
only if $\Vvdash(\psi\leftrightarrow\psi').$%
\footnote{For sentences, this definition of logical equivalence reduces to
the
one given in section 3.6. See also Theorem 4 below. %
}
Armed with this definition the statement and proof of the replacement
theorem are both straightforward.
\begin{description}
\item [{Theorem~2.}] Replacement (Substitution of Equivalent Sub-formulas)
\end{description}
Let $\psi$, $\psi'$, $\phi$, and $\phi'$ be formulas. If
$\Vvdash(\psi\leftrightarrow\psi')$,
and $\phi'$ is like $\phi$ except that $\phi'$ contains an occurrence
of $\psi'$ at a place where $\phi$ contains an occurrence of $\psi$,
then $\Vvdash(\phi\leftrightarrow\phi')$.
Proof: Straightforward, adapting the proof of Replacement in Mates
\cite{Mates1972a}, pp. 135-136. First prove the following lemma:
If $\Vvdash(\psi\leftrightarrow\psi'),$ then
$\Vvdash(\neg\psi\leftrightarrow\neg\psi'),$
$\Vvdash((\psi\wedge\chi)\leftrightarrow(\psi'\wedge\chi)),$
$\Vvdash(\square\psi\leftrightarrow\square\psi'),$
$\Vvdash(\mathsf{A}\psi\leftrightarrow\mathsf{A}\psi'),$
$\Vvdash(\forall\alpha\psi\leftrightarrow\forall\alpha\psi'),$
and
$\Vvdash(\langle\lambda\alpha.\psi\rangle(\tau)\leftrightarrow\langle\lambda\alpha.\psi'\rangle(\tau)),$
where $\psi,$ $\psi',$ and $\chi$ are formulas, $\alpha$ is a
variable, and $\tau$ is a term.%
\footnote{It is sufficient to consider just these cases since all the SAT
logical
operators can be defined using $\neg,\wedge,\square,\mathsf{A},\forall,$
and $\lambda.$ %
} Theorem 2 then follows by induction on the complexity of $\phi.$
$\blacksquare$
\subsection{Sentences: Closure, Validity, Consequence, Equivalence}
Two further results concerning sentences are easily established.
\begin{description}
\item [{Theorem~3.}] Closure and Validity
\end{description}
For any sentence $\phi,$ $\Vvdash\phi$ if and only if $\vDash\phi.$
Proof: The \textquoteleft{}if' part is immediate by the rule of
necessitation
(section 4.4). For the \textquoteleft{}only if' part, suppose $\nvDash\phi.$
Then $\phi$ is false at some world $w$ of some model $\mathcal{M}$.
Construct a model $\mathcal{M}'$ that is exactly like $\mathcal{M}$
except for containing an additional world $w'$ such that
$w'\mathcal{R}\mathit{w}$.
$\square\phi$ is false at $w',$ and hence $\nvDash\square\phi.$
So it is false that $\Vvdash\phi.$ $\blacksquare$
\begin{description}
\item [{Theorem~4.}] Logical Consequence and Logical Equivalence
\end{description}
For any sentences $\phi$ and $\phi',$ the following three conditions
are equivalent:
\begin{quotation}
1. $\Vvdash(\phi\leftrightarrow\phi')$
2. $\vDash(\phi\leftrightarrow\phi')$
3. $\mathrm{\phi\vDash\phi'}$ and $\mathrm{\phi'\vDash\phi}.$
\end{quotation}
Proof: The equivalence of 1 and 2 is immediate by Theorem 3. The equivalence
of 2 and 3 holds in view of the standard definition of consequence
in section 3.7. $\blacksquare$
It is noteworthy that, as in standard first-order non-modal logic,
two sentences are logically equivalent if and only if each is a consequence
of the other as 2 and 3 of Theorem 4 show.
\subsection{Deduction Theorem}
A deduction theorem exactly analogous to that of standard first-order
non-modal logic also holds.
\begin{description}
\item [{Theorem~5.}] Deduction Theorem
\end{description}
For any sentences $\phi$ and $\phi',$ and any set of sentences $\Gamma,$
$\Gamma\cup\{\phi\}\vDash\phi'$ if and only if
$\Gamma\vDash\phi\rightarrow\phi'.$
Proof: Obvious in view of the standard definition of consequence in
section 3.6. $\blacksquare$
\section{Comparisons with Other Systems}
\subsection{Actualism and Serious Actualism: Plantinga, Jager, Stephanou}
Actualism and serious actualism have long been advocated by Plantinga.
He defines actualism as the claim that there neither are nor could
have been things that do not exist.%
\footnote{See \cite{plantinga:1985a} pp. 91-93, \cite{plantinga:1985b} p.
314. Plantinga apparently doesn't use the term `actualism' in
\cite{plantinga:1974},
but he states it's denial on p. 149 and argues against it--effectively,
in my opinion--on pp. 149-153. %
} Rendered in my notation this is
\begin{description}
\item [{(Act1)}] $\neg(\exists x\neg\mathcal{E}(x)\vee\lozenge\exists
x\neg\mathcal{E}(x))$,\noun{ }
\end{description}
which is valid and equivalent to
\begin{description}
\item [{(Act2)}] $\square\forall x\mathcal{E}(x)$.
\end{description}
But these sentences do not distinguish actualism from possibilism.
Both would still be valid if quantifiers were given a possibilist
interpretation, that is if they were made to range over the domain
of a model, rather than just over the domains of worlds in a model.
Possibilists will have no qualms accepting them. Actualism is better
expressed by
\begin{quotation}
There is nothing that isn't actual,
\end{quotation}
equivalently
\begin{quotation}
Everything is actual,
\end{quotation}
which is expressible as
\begin{description}
\item [{(Act3)}] $\forall x\mathsf{A}\mathcal{E}(x)$.
\end{description}
(Act3) is not valid in SAT, since it is false at any world that contains
an object not in the domain of the actual world, but it is true in
the intended model,
$\mathit{\mathrm{\mathcal{\mathrm{\mathcal{M_{I}^{A}}}}}}$,
which is defined in section 7. Possibilists should want to reject
(Act3), since the central tenet of possibilism is that there is more
to reality than that which is actual. Yet if quantifiers are given
a possibilist interpretation (Act3) is valid. So (Act3) marks a distinction
between actualism and posibilism that (Act1) and (Act2) do not.%
\footnote{There are versions of possibilism that would accept (Act3), but
discussing
them would take us too far afield.%
}
In his argument for actualism in \cite{plantinga:1974} Plantinga
distinguishes between what he calls predicative and impredicative
singular propositions. The former affirm, and the latter deny, a property
of an object.%
\footnote{\cite{plantinga:1974}, pp. 136, 149.%
} Plantinga's rebuttal of what he calls the Classical Argument for
possible but non-existent objects makes use of this distinction.%
\footnote{\cite{plantinga:1974}, p. 133.%
} Specifically, (using his numbering) he distinguishes the impredicative
\begin{description}
\item [{(13{*})}] Socrates does not have the property of existing
\end{description}
from the predicative
\begin{description}
\item [{(13{*}{*})}] Socrates has the property of nonexistence.%
\footnote{\cite{plantinga:1974}, p. 151.%
}
\end{description}
Plantinga says, rightly, that (13{*}) is true in just those worlds
in which
\begin{description}
\item [{(23{*})}] Socrates exists
\end{description}
is false, and that (13{*}{*}) is false in every world.
Predicate abstraction is ideally suited to mark these distinctions.
In SAT Plantinga's (13{*}) and (13{*}{*}) are naturally expressed
as
\begin{description}
\item [{({*})}] $\neg\langle\lambda y.\mathcal{E}(y)\rangle(s)$
\end{description}
and
\begin{description}
\item [{({*}{*})}] $\langle\lambda y.\neg\mathcal{E}(y)\rangle(s)$,
\end{description}
respectively, and their truth values are determined exactly as Plantinga
says. ({*}) is true at a world in a model just in case \emph{s} fails
to denote at that world, and the denial of ({*}{*}) is true at every
world in every model. So in SAT
\begin{description}
\item [{($\neg${*}{*})}] $\neg\langle\lambda y.\mathcal{\neg
E}(y)\rangle(s)$
\end{description}
and indeed
\begin{description}
\item [{($\neg\lozenge${*}{*})}] $\neg\lozenge\langle\lambda
y.\neg\mathcal{E}(y)\rangle(s)$
\end{description}
are valid. Not only is it false that Socrates is nonexistent, it is
impossible that he be so. And the use of predicate abstraction makes
it clear that this latter claim, embodied in ($\neg\lozenge${*}{*}),
is a far cry from
\begin{quotation}
$\neg\lozenge\neg\langle\lambda y.\mathcal{E}(y)\rangle(s)$,
\end{quotation}
which is of course false in the intended model
$\mathit{\mathrm{\mathcal{\mathrm{\mathcal{M_{I}^{A}}}}}}$.%
\footnote{The sentences $\neg\langle\lambda
y.\lozenge\neg\mathcal{E}(y)\rangle(s)$,
$\langle\lambda y.\neg\lozenge\neg\mathcal{E}(y)\rangle(s)$, and
$\neg\lozenge\neg\mathcal{E}(s)$, all orthographically similar to
($\neg\lozenge${*}{*}), are also false in
$\mathit{\mathrm{\mathcal{\mathrm{\mathcal{M_{I}^{A}}}}}}$.%
}$^{,}$%
\footnote{In a recent paper \cite{Percival2011} Percival discusses many
issues
concerning actualism and the use of predicate abstraction. Space prevents
me from going into details, but SAT is innocent of a charge he makes
against another actualistic logic with an abstraction operator. (He
defines this logic in \cite{Percival2011} 413-414, including footnote
45). The charge is that although this logic supports the claim that
``$\ldots$ some existing object is such as to exist contingently'',
it also holds that ``$\ldots$ it is metaphysically possible for
there to be objects that do not exist''. I find the reasoning Percival
gives in support of this charge unclear, but it is clear the charge
does not apply to SAT. In SAT $\exists
x(\mathcal{E}(x)\wedge\neg\square\mathcal{E}(x))$
is true in the intended model, but $\lozenge\exists x\neg\mathcal{E}(x)$
is logically false, since its denial is equivalent to (Act2). %
}
Plantinga also advocates serious actualism, which he expresses as
``... no object \emph{x} has any property in any world in which \emph{x}
doesn't exist'', and ``... no object could have a property without
existing''.%
\footnote{\cite{plantinga:1985a}, p. 93, and \cite{plantinga:1985b}, p. 316,
respectively.%
} Understood this way serious actualism quantifies over properties
and so cannot be expressed in a first-order language. But it can be
approximated schematically as
\begin{description}
\item [{(SA)}]
$\forall\alpha_{1}\square(\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\mathcal{E}(\alpha_{1})))$,
\end{description}
all instances of which are valid in SAT.
Plantinga nowhere formalizes his preferred modal logic; for this he
refers his readers to the work of Jager. In \cite{jager_t:1982a},
Jager presents his system \emph{A}, in which an atomic formula is
satisfied at a world by an \emph{n}-tuple of objects only if each
of those objects exists at that world. \emph{A} is thus seriously
actualistic with respect to atomic formulas. But it lacks predicate
abstraction and thus is not fully seriously actualistic in the way
SAT is. \emph{A} contains the usual connectives and quantifiers, but
it lacks individual constants and an actuality connective. For each
model the variables of $A$ take their values from the domain of that
model, and they denote the same object at each world therein. But
the range of quantifiers at a world is limited to the domain of that
world. Thus in its treatment of variables and quantifiers $A$ is
exactly like SAT. \emph{A} differs from SAT in that negation and necessity
are given \emph{de} \emph{re} interpretations, which I'll represent
with $\neg_{r}$ and $\square_{r}$, and which are easily defined
in SAT. For example, $\neg_{r}Fx$ and $\square_{r}Fx$ can be expressed
as
\begin{quotation}
$\langle\lambda y.(\mathcal{E}(y)\wedge\neg Fy)\rangle(x)$
\end{quotation}
and
\begin{quotation}
$\langle\lambda y.(\mathcal{E}(y)\wedge
Fy\wedge\square(\mathcal{E}(y)\rightarrow Fy)\rangle(x)$,
\end{quotation}
respectively.%
\footnote{For the formula $Rxy$, $\neg_{r}Rxy$ can be expressed in SAT as
$\langle\lambda z,w.(\mathcal{E}(z)\wedge\mathcal{E}(w)\wedge\neg
Rzw)\rangle(x,y)$
and $\square_{r}Rxy$ as $\langle\lambda
z,w.(\mathcal{E}(z)\wedge\mathcal{E}(w)\wedge
Rzw\wedge\square((\mathcal{E}(z)\wedge\mathcal{E}(w))\rightarrow
Rzw))\rangle(x,y)$.
Similarly for formulas, atomic or complex, with free occurrences of
three or more variables. %
}
In \cite{Jager1988} Jager extends system \emph{A} to the system he
calls \emph{D}, in order to facilitate distinguishing \emph{de} \emph{re}
and \emph{de dicto} modalities and negations. He does this by supplementing
\emph{A} in a way that makes it possible to exempt particular occurrences
of variables within the scope of $\neg_{r}$ or $\square_{r}$ from
the requirement, described in the previous paragraph, that they denote
an object at the world of evaluation in order for the formula in which
they appear to be satisfied at that world. Specifically, he adds an
operator he calls a \emph{dictifier} ($\nabla$) and, for each variable
\emph{$\alpha$,} infinitely many \emph{position variants}, $\alpha^{1}$,
$\alpha^{2}$, $\alpha^{3}$, ..., of $\alpha$. (In the semantics
of \emph{D} each position variant of a variable is assigned the same
value as the variable itself.) Thus if $\nabla x^{1}Rx^{1}y^{1}$
appears within the scope of $\neg_{r}$ or $\square_{r}$, $x^{1}$
(but not $y^{1}$) is exempt from the requirement in question.
Using these resources, and adding individual constants such as \emph{s}
and \emph{p} to the language of \emph{D} to facilitate representing
English sentences (as Jager himself does), the sentences
\begin{quotation}
Socrates has the property of necessarily-teaching-Plato
\end{quotation}
and
\begin{quotation}
Plato has the property of necessarily-being-taught-by-Socrates
\end{quotation}
can be expressed as
\begin{quotation}
$\square_{r}\nabla pTsp$
\end{quotation}
and
\begin{quotation}
$\square_{r}\nabla sTsp$,
\end{quotation}
respectively. In SAT these sentences can be expressed, at least as
perspicuously, as
\begin{quotation}
$\langle\lambda x.\square(\mathcal{E}(x)\rightarrow Txp)\rangle(s)$
\end{quotation}
and
\begin{quotation}
$\langle\lambda x.\square(\mathcal{E}(x)\rightarrow Tsx)\rangle(p)$,
\end{quotation}
respectively.
More generally, it is easy to show that every Jager model and variable
assignment can be exactly replicated by a SAT model and valuation.%
\footnote{The only complication is that SAT must be augmented by infinitely
many position variants of each of its variables, and, for each
SAT-model-plus-valuation,
each position variant of a variable must be assigned the same object
as the variable itself. %
} Given this fact, and using the SAT constructions for expressing Jager's
\emph{de re} negation and \emph{de re} necessity given three paragraphs
back, it is easily proved that a formula of \emph{D} is satisfied
by a variable assignment at a world of a Jager model if and only if
it is satisfied at the same world of the corresponding SAT model by
the corresponding valuation.
Finally, it should be noted that Stephanou has given a long and subtle
defense of serious actualism in \cite{stephanou:2007}. Although,
like Plantinga, he understands serious actualism as quantifying over
properties and relations as well as individuals, he recognizes that
it is partially expressed by first-order formulas of the form
\begin{description}
\item [{(SA1)}]
$\forall\alpha\square(\phi(\alpha)\rightarrow\mathcal{E}(\alpha))$,
\end{description}
where $\phi(\alpha)$ is an atomic formula in which $\alpha$, and
perhaps other variables, have free occurrences. He calls the schema
(SA1) \emph{predicate actualism}, and he is keenly aware that it is
plausible only when $\phi(\alpha)$ is construed as an atomic formula.
For he notes that from (SA1) and
\begin{quotation}
$\forall\alpha\square(\neg\phi(\alpha)\rightarrow\mathcal{E}(\alpha))$
\end{quotation}
it follows that
\begin{quotation}
$\forall\alpha\square\mathcal{E}(\alpha)$,
\end{quotation}
a result he wants to avoid.
In \cite{stephanou:2007} Stephanou does not present a system of formal
semantics, although he considered such systems in \cite{Stephanou2002}
and \cite{stephanou:2005}. And although (SA1) is a valid schema in
the systems he presents in the latter two papers, uniform substitution
of complex formulas for atomic formulas does not preserve validity
in any of them. For none of these systems contains predicate abstraction
or any means of obtaining its effect. So while Stephanou's semantic
systems treat primitive predicates in accordance with serious actualism,
they lack a mechanism for passing that treatment on to more complex
formulas.
\subsection{Names and Abstraction: Garson, Chihara, Stalnaker}
Of all the systems discussed by Garson in his encyclopedic survey
of modal logics SAT is most similar to Q3.%
\footnote{\cite{Garson2001} pp. 278-280.%
} Both are free logics in which quantifiers are world relative, variables
are rigid, and individual constants are non-rigid. They differ in
that SAT contains predicate abstraction and embodies serious actualism,
features that Q3 lacks.
Because it contains predicate abstraction SAT supports a straightforward
free-logic version of universal instantation: (UI) given in section
4.3. The version of universal instantation Garson gives for Q3 (due
to Hintikka) is considerably more complex. And although the individual
constants of SAT and Q3 are non-rigid, in both systems they can be
made to approximate rigid designators. For the individual constant
\emph{d} all that is required is the stipulation $\exists x\square(d=x)$,
or $\exists x(\square(d=x)\wedge\square\square(d=x))$, or $\exists
x(\square(d=x)\wedge\square\square(d=x)\wedge\square\square\square(d=x))$,
and so on.%
\footnote{For SAK $(d=d)$ would be added. The sentences in this list that
are
existential generalizations of conjunctions are similar to, but in
general stronger than, the sentences used by Hintikka in formulating
a rule of universal instantiation for Q3. The latter sentences are
conjunctions of existential generalizations. See Garson \cite{Garson2001},
pp. 279-280 for details.%
} We can thus stipulate that \emph{d} denotes one and the same object
in all possible worlds (including the actual world), or that it does
this in all possible worlds and in all possibly possible worlds, and
so on. (In SAS4 and SAS5 this entire set of sentences can be replaced
by the single sentence $\exists x\square(d=x)$.)
Chihara's systems M$_{1}$ and M{*} are similar to SAT in that they
are seriously actualistic free logics with world-relative quantifiers.
They differ from it in that their individual constants are model-wide
rigid designators. They also differ in lacking predicate abstraction
and identity. SAT is closer to M$_{1}$, since M{*} is simply M$_{1}$
plus Chihara's (seemingly false) Principle of Compossibility.%
\footnote{For M$_{1}$, M{*}, and the Principle of Compossibility see Chihara
\cite{chihara:1998a}, pp. 220-224.%
}
In \cite{Stalnaker1995} (which is reprinted with minor changes in
\cite{Stalnaker2003}) Stalnaker develops a quantified modal logic
with predicate abstraction that is similar to, but interestingly different
from, SAT. A striking feature of this system, which I'll call Stal-T,%
\footnote{Stalnaker says (\cite{Stalnaker1995}, note 21) that his results
hold
if the underlying propositional modal logic is K, T, B, S4, S5, K4,
or K5. I use `Stal-T' to refer to the T-based version of his system
to facilitate comparison with SAT, the T-based version of mine. But
the similarities and differences noted in the text also hold when
the underlying modal logic is any of those listed.%
} is that its universal quantifier applies directly to predicate abstracts
(and to unary predicates) rather than to formulas. His says this approach
\begin{quotation}
$\ldots$ gives a clearer representation of the logic of quantification
because it separates two conceptually distinct operations that are
performed by variable-binding operators. First is the implicit formation
of complex predicates from complex sentences by introducing
blanks\textemdash{}free
variables\textemdash{}in the sentences. The second is generalization:
the formation of general claims from predicates\textemdash{}the claims
that everything in the domain, or at least one thing in the domain,
satisfies the predicate that is implicitly represented by the the
open sentence. In our language, the abstraction operator makes the
first of these operations explicit, turning an open sentence into
an expression that has the syntactic role as well as the semantic
function of a predicate. Then the quantifier has only the job of expressing
generality.%
\footnote{\cite{Stalnaker1995}, p. 14.%
}
\end{quotation}
Stalnaker's predicate abstraction operator (represented by a cap over
a variable) plays the same role in his system as the lambda operator
plays in SAT. So where \emph{S} is a unary predicate, $\hat{x}Sx$
and $\hat{x}Sxd$ in Stal-T correspond, respectively, to $\langle\lambda
x.Sx\rangle$
and $\langle\lambda x.Sx\rangle(d)$ in SAT. Similarly, $\forall\hat{x}Sx$
corresponds to $\forall xSx$.
In addition to predicate abstraction and the universal quantifier
Stal-T, like SAT, contains the usual truth-functional and modal connectives.
Indeed SAT and Stal-T are nearly identical logics. Yet even though
Stalnaker is clearly interested in the proper representation of logical
form, he does not discuss uniform substitution for predicate abstracts
(compare section 5.1 above). Neither does he discuss substitution
of equivalent sub-formulas (compare section 5.2 above). His main focus
is on showing how to combine extensional first-order free logic and
propositional modal logic without having to retract anything from
either and adding only ``... two principles that concern the interaction
of modality with predication, and modality with identity''.%
\footnote{\cite{Stalnaker1995}, p. 23. %
} He gives an axiomatization of Stal-T, which he claims is sound and
complete with respect to the semantics, but he does not prove this.
SAT and Stal-T are alike in that the extensions of predicates and
predicate abstracts at a world are restricted to objects in the domain
of that world. Both are thus seriously actualistic with respect to
all predicates, unlike the systems of Jager and Stephanou (discussed
in section 6.1) that are seriously actualistic only with respect to
primitive predicates. They are also alike in that the domain of a
world in a model may be empty, an individual constant need not denote
at a world and may denote different objects at different worlds, and
the denotation (if any) of an individual constant at a world must
be in the domain of that world. They differ in that Stal-T, but not
SAT, counts vacuous predicate abstracts as well formed, and applies
the terms `valid' and `invalid' to formulas containing free occurrences
of variables. If the semantics of Stal-T is modified to be like that
of SAT in these two ways, corresponding sentences of the two languages
will take the same truth value at each world of each model.
The sentences of Stal-T are unambiguous, but inserting $\langle$
and $\rangle$ as additional brackets to mark off predicate abstracts
will improve readability and facilitate comparison with SAT. So, for
example, where \emph{S} is a primitive unary predicate I'll write
$\exists\langle\hat{x}Sx\rangle$ for $\exists\hat{x}Sx$,
$\neg\forall\langle\hat{x}\neg Sx\rangle$
for $\neg\forall\hat{x}\neg Sx$,
$\forall\langle\hat{x}\square\langle\hat{y}Sy\rangle x\rangle$
for $\forall\hat{x}\square\hat{y}Syx$. The transformations that preserve
equivalence are as follows.
Starting with a sentence of SAT replace subformulas of the form
$\forall\alpha\phi$
with $\forall\langle\hat{\alpha}\phi\rangle$, $\exists\alpha\phi$
with $\exists\langle\hat{\alpha}\phi\rangle$, and
$\langle\lambda\alpha.\phi\rangle(\beta)$
with $\langle\hat{\alpha}\phi\rangle\beta$. To go in the other direction,
first replace any subformulas of the form $\forall\psi$ and $\exists\psi$,
where $\psi$ is a primitive unary predicate, with $\forall x\psi x$
and $\exists x\psi x$.%
\footnote{In Stal-T quantifiers apply directly to primitive unary predicates
so, for example, $\forall S$ and $\exists S$ are well formed. %
} Then replace subformulas in accordance with the pairings given in
the first sentence of this paragraph, but in the reverse order. This
will yield a sentence of SAT. Under these transformations the resulting
sentence will be equivalent to the original, given the modifications
of Stal-T syntax and semantics noted two paragraphs back.
Stalnaker points out that both the Barcan formula and its converse
have invalid instances when expressed in his language as
\begin{quotation}
$\forall\hat{x}\square\phi\rightarrow\square\forall\hat{x}\phi$
\end{quotation}
and
\begin{quotation}
$\square\forall\hat{x}\phi\rightarrow\forall\hat{x}\square\phi$.
\end{quotation}
But he does not mention that some non-trivial instances of the following
form of the converse Barcan formula,
\begin{quotation}
$\exists\hat{x}\lozenge\phi\rightarrow\lozenge\exists\hat{x}\phi$,
\end{quotation}
are valid in Stal-T. Using the convention on brackets introduced above
and taking $\phi$ as $\langle\hat{y}Sy\rangle x$ or (where \emph{T}
is a binary predicate) $\langle\hat{y}Tyd\rangle x$ yields
\begin{quotation}
$\exists\langle\hat{x}\lozenge\langle\hat{y}Sy\rangle
x\rangle\rightarrow\lozenge\exists\langle\hat{x}\langle\hat{y}Sy\rangle
x\rangle$
\end{quotation}
and
\begin{quotation}
$\exists\langle\hat{x}\lozenge\langle\hat{y}Tyd\rangle
x\rangle\rightarrow\lozenge\exists\langle\hat{x}\langle\hat{y}Tyd\rangle
x\rangle$,
\end{quotation}
both of which are valid in Stal-T. Transformed into SAT they become
\begin{quotation}
$\exists x\lozenge\langle\lambda y.Sy\rangle(x)\rightarrow\lozenge\exists
x\langle\lambda y.Sy\rangle(x)$
\end{quotation}
and
\begin{quotation}
$\exists x\lozenge\langle\lambda y.Tyd\rangle(x)\rightarrow\lozenge\exists
x\langle\lambda y.Tyd\rangle(x)$,
\end{quotation}
which are instances of the valid schema (CBF) given in section 4.4
above. Indeed, where $\phi(\alpha_{2})$ is a formula containing free
occurrences of $\alpha_{2}$ (but no free occurrences of any other
variable) all sentences of the form
\begin{description}
\item [{(CBF{*})}]
$\exists\langle\hat{\alpha_{1}}\lozenge\langle\hat{\alpha_{2}}\phi(\alpha_{2})\rangle\alpha_{1}\rangle\rightarrow\lozenge\exists\langle\hat{\alpha_{1}}\langle\hat{\alpha_{2}}\phi(\alpha_{2})\rangle\alpha_{1}\rangle$,
\end{description}
are valid in Stal-T. But not all sentences of the form
\begin{description}
\item [{(\emph{faux}~CBF{*})}]
$\square\forall\langle\hat{\alpha_{1}}\langle\hat{\alpha_{2}}\phi(\alpha_{2})\rangle\alpha_{1}\rangle\rightarrow\forall\langle\hat{\alpha_{1}}\square\langle\hat{\alpha_{2}}\phi(\alpha_{2})\rangle\alpha_{1}\rangle$
\end{description}
are. Of course (CBF{*}) and (\emph{faux} CBF{*}) are just the translations
into Stal-T of (CBF) and (\emph{faux} CBF) of section 4.4. So Stal-T
distinguishes between the two versions of the converse Barcan formula
just as SAT does.
\section{Truth \emph{simpliciter} and Actualism}
Thus far I have been concerned almost exclusively with matters of
logic: logical truth, logical consequence, logical equivalence. These
notions were defined, using models, in a way that embodies serious
actualism. Indeed we have seen that serious actualism is reflected
in certain logically true sentences of the language. (Recall (SA)
from section 6.1.) But as yet I have said almost nothing about about
truth \emph{simpliciter} or about actualism, the view that whatever
is is actual.
Given the semantics developed thus far, based on models, it's natural
to designate a particular model as the intended model and then identify
truth \emph{simpliciter} with truth at the actual world element of
this model. A modal realist would specify the intended model,\emph{
}$\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$ (\emph{$\mathcal{I}$}
for intended), as $\mathit{\mathit{\mathrm{\mathcal{\langle
W_{\text{\ensuremath{\mathcal{I}} }}\mathrm{,}\mathrm{@
_{\mathcal{I}},}R\mathrm{_{\mathcal{I}},}D_{\mathcal{I}}\mathrm{,}I_{\mathcal{I}}}\mathcal{\rangle}}}}$,
where $\mathcal{W_{\text{\ensuremath{\mathcal{I}} }}}$ really is
the set of all possible worlds,$@_{\mathcal{I}}$ is the actual world,
$R\mathrm{_{\mathcal{I}}}$ is the relation of relative possibility
among the worlds,
$\mathit{D_{\mathcal{I}}}(\mathit{\mathrm{\mathcal{\mathrm{@
_{\mathcal{I}}}}}})$
is the set of all actual individuals, $D_{\mathcal{M_{I}}}$ is the
set of all actual and possible individuals, etc. Truth \emph{simpliciter}
becomes truth at $\mathit{\mathrm{\mathcal{\mathrm{@_{\mathcal{I}}}}}}$
of $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$. But this approach
is not available to the actualist, who eschews all talk of possible
worlds, possible objects, and alleged relations among such alleged
entities. So construed $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$
does not exist.
There is, however, a way for an actualist who accepts modal terms
(like those italicized in this paragraph) as primitive to make this
kind of approach work. Using only selected pure sets as surrogates
for actual and possible objects, and given some convention about what
counts as modeling, set theory can be used to create, out of pure
sets alone, a model isomorphic to
$\mathit{\mathrm{\mathcal{M_{\text{I}}}}}$.
More precisely, the model in question \emph{would be} isomorphic to
$\mathit{\mathrm{\mathcal{M_{\text{I}}}}}$ if
$\mathit{\mathrm{\mathcal{M_{\text{I}}}}}$
existed. Under this approach $\mathit{\mathrm{\mathcal{\mathrm{@_{I}}}}}$
becomes a set-theoretic construct that accurately models the world,
how things are. The other members of $\mathcal{W_{\text{I}}}$ are
similar set-theoretic constructs, each of which \emph{might have been}
a model of the world.
$\mathit{\mathrm{\mathcal{D_{\text{I}}}}}(\mathit{\mathrm{\mathcal{\mathrm{@
_{I}}}}})$
is the set of surrogates of all actual things, and for each
$w_{i}\in\mathcal{W_{\text{I}}}$,
$\mathit{\mathrm{\mathcal{D_{\text{I}}}}}(w_{i})$ is the set of things
that \emph{would be} surrogates of the actual things if $w_{i}$ \emph{were
}a model of how things are. In this way an actualist who is willing
to accept modal terms as primitive can construct a model that \emph{would
be} isomorphic to $\mathit{\mathrm{\mathcal{M_{\text{I}}}}}$ if the
latter existed.%
\footnote{If in constructing such a model we attempt to represent ``all of
reality'', including both the physical world and the entire set-theoretic
universe, cardinality problems will of course arise. But I can see
no barrier to constructing models of this kind that, while not completely
comprehensive, are large enough to be interesting.%
}
This approach has been developed in detail by Christopher Menzel
\cite{Menzel1990a}.
He uses pure sets (entities whose existence is relatively widely accepted)
to construct models of how things are and how they might have been.
As sketched in the previous paragraph, under this approach some pure
sets represent (actual and possible) individuals, others represent
the extensions (at worlds) of properties and relations, and still
others represent the (actual and other possible) worlds themselves.%
\footnote{Menzel's construction makes use of properties and relations, in
addition
to pure sets. In \cite{Ray1996} Ray argues that pure sets alone suffice.
I believe Ray is correct, but I won't address the issue here.%
} Menzel's theory is complex, and I won't try to present it in detail,
but it will be useful to quote his general description of the project.
In the following passage he uses
$\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$
in the same way I used $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$
in the previous paragraph, namely as a term that would denote the
modal realist's intended model if only it existed.%
\footnote{Menzel \cite{Menzel1990a}, p. 372. Menzel's
$\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$
and my $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$differ in
some details, but the differences are unimportant for present purposes.%
}
\begin{quotation}
Suspend your skepticism for the moment and take the possibilist's
vision of modal reality at face value; imagine, that is to say, that
there really is a standard model
$\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$
replete with possible worlds and their (in general) merely possible
inhabitants. At the same time ... allow that modality is primitive,
not analyzable in terms of primitive worlds. Every modal statement
thus yields at most an \emph{equivalent} statement about worlds and
their denizens, but no such statement is to be considered an \emph{analysis}
of the modal statement. Consider a model $\mathit{\mathrm{\mathcal{M}_{4}}}$
... isomorphic to $\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$,
but constructed only out of unproblematic (relatively speaking!) necessary
beings; pure sets, say. In virtue of the isomorphism, of course,
$\mathit{\mathrm{\mathcal{M}_{4}}}$
would do just as well as $\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$
for defining truth for modal languages; structurally,
$\mathit{\mathrm{\mathcal{M}_{4}}}$
represents modal reality no less than
$\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$.
Now, while retaining your belief in the primitiveness of modality,
reinvoke you skepticism about worlds. The standard model drops away,
but $\mathit{\mathrm{\mathcal{M}_{4}}}$ endures with only pure sets
in place of worlds and possibilia, as accurate a representation of
modality as before.
\end{quotation}
Menzel proceeds to specify in substantial detail the conditions
$\mathit{\mathrm{\mathcal{M}_{4}}}$
must satisfy in order to provide a satisfactory account of truth
\emph{simpliciter}
for a first-order modal language. This account makes use of modal
terms, but it invokes no entities about the existence of which skepticism
is justified. In particular it does not invoke
$\mathit{\mathrm{\mathcal{M^{\diamondsuit}}}}$
or anything like $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$.
Under this account truth \emph{simpliciter} turns out to be just truth
at the actual-world element of $\mathit{\mathrm{\mathcal{M}_{4}}}$.
Following Menzel \cite{Menzel1990a} and Ray \cite{Ray1996} an actualistic
variant of $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$ can be
specified making use only of pure sets, (relatively) unproblematic
objects. So construed $\mathcal{M_{\text{\ensuremath{\mathcal{I}} }}}$
does\emph{ }exist.
When so construed I'll call it
$\mathit{\mathrm{\mathcal{M_{I}^{A}}}=\mathit{\mathrm{\mathcal{\langle
W_{\text{\ensuremath{\mathcal{I}} }}^{A}\mathrm{,}\mathrm{@
_{\mathcal{I}}^{\mathcal{A}},}R_{\mathcal{I}}^{\mathcal{A}}\mathrm{,}D_{\mathcal{I}}^{\mathcal{A}}\mathrm{,}I_{\mathcal{I}}^{\mathcal{A}}}\mathcal{\rangle}}}}$\emph{
}(\emph{$\mathcal{I}$} for intended, \emph{$\mathcal{A}$} for actualistic).
$\mathit{\mathrm{\mathcal{\mathrm{\mathcal{M_{I}^{A}}}}}}$ is the
\emph{intended model}, in which $\mathcal{W_{\text{\ensuremath{\mathcal{I}}
}}^{A}}$
is the set of all world surrogates, $\mathit{\mathrm{\mathcal{\mathrm{@
_{\mathcal{I}}^{\mathcal{A}}}}}}$
is the actual world surrogate,
$\mathit{D_{\mathcal{I}}^{\mathcal{A}}}(@_{\mathcal{I}}^{\mathcal{A}})$
is the set of all actual individual surrogates, etc. Truth
\emph{simpliciter}
is now just truth at $@_{\mathcal{I}}^{\mathcal{A}}$, the actual-world
element of $\mathit{\mathrm{\mathcal{\mathrm{\mathcal{M_{I}^{A}}}}}}$.
Necessary truth is truth at all $w_{\text{\ensuremath{\mathcal{I}}
}}^{A}\in\mathcal{W_{\text{\ensuremath{\mathcal{I}} }}^{A}}$
such that
$@_{\mathcal{I}}^{\mathcal{A}}R_{\mathcal{I}}^{\mathcal{A}}w_{\text{\ensuremath{\mathcal{I}}
}}^{A}$.
Given this terminology the sentence (Act3) of section 6.1, which expresses
actualism, is true but not necessary.
\begin{description}
\item [{(Act3)}] $\forall x\mathsf{A}\mathcal{E}(x)$
\end{description}
(Act3) is true because it says that everything is actual, an
obvious\textemdash{}indeed
an \emph{a priori}\textemdash{}truth. But on the plausible assumption
that there might have been things that don't actually exist, (Act3)
is not true at every $w_{\text{\ensuremath{\mathcal{I}}
}}^{A}\in\mathcal{W_{\text{\ensuremath{\mathcal{I}} }}^{A}}$
such that
$@_{\mathcal{I}}^{\mathcal{A}}R_{\mathcal{I}}^{\mathcal{A}}w_{\text{\ensuremath{\mathcal{I}}
}}^{A}$,
and hence not necessary. So (Act3) is an example of a contingent \emph{a
priori} truth. I have discussed this and related matters elsewhere.
In \cite{Authora} I argued that sentences with the form
$(\mathsf{A}p\rightarrow p)$
(where \emph{p} is not itself a necessary truth) are contingent yet
true \emph{a priori}. In \cite{Author} I argue that such sentences
are also synthetic.%
\footnote{See especially \cite{Authora}, p. x, and \cite{Author}, section
y.z.%
}
Although (Act3) is true but not necessary, we have seen that all sentences
of the form (SA) of section 6.1, which express serious actualism,
are not only true and necessary, they are logical truths.
\begin{description}
\item [{(SA)}]
$\forall\alpha_{1}\square(\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\mathcal{E}(\alpha_{1})))$
\end{description}
The status of (Act3) is tied up with the fact that I have defined
validity as general validity, truth at every world in every model.
Were validity defined as real world validity, truth at the actual-world
element of every model, things would be different. (Act3) and other
sentences with a similar structure would be classified as valid, but
the rule of necessitation (Nec) would no longer preserve validity.
Elsewhere I have argued at length that general validity has a better
claim to the title of logical truth than does real world validity.%
\footnote{See \cite{Authora}, and \cite{Author}. %
}
\section{Tableaus}
In this section I develop a system of tableau proofs for SAT and its
kindred systems.%
\footnote{Namely, SAK, SAB, SAS4, and SAS5.%
} In the Appendix I prove that these systems are sound and (weakly)
complete with respect to the corresponding notions of logical consequence.
These tableau systems follow closely those of Fitting and Mendelsohn
\cite{Fitting1998}.
\subsection{The Basics}
\subsubsection{\emph{$\mathfrak{L^{\bigstar}}$}, the Language of Tableaus}
\emph{$\mathfrak{L^{\bigstar}}$} is a slight extension of the language
\emph{$\mathfrak{L}$} presented in section 2. It differs from
\emph{$\mathfrak{L}$
}only in containing additional individual symbols called grounded
terms. Grounded terms will be explained shortly, but first I need
to describe the prefixes that appear in tableau nodes.
Each tableau node consists a formula of \emph{$\mathfrak{L^{\bigstar}}$
}preceded by a prefix, this prefix being a sequence of (numerals for)
positive integers and the symbol \textbf{@ }separated by periods.
The first symbol in a sequence is always 1 or \textbf{@}. Thus the
following are sequences: 1, \textbf{@}.1.1.3, 1.4.5.2, 1.1.2. If $\sigma$
is a prefix and \emph{n} is a positive integer, then $\sigma.n$ is
$\sigma$ followed by a period followed by \emph{n.} Thus if $\sigma$
is 1.3.4 or \textbf{@}$.$1.1, and \emph{n} is 2, then $\sigma.n$
is 1.3.4.2 or \textbf{@}.1.1.2, respectively. Intuitively, tableau
prefixes play the role of the worlds of a model, and if nodes containing
the prefixes $\sigma$ and $\sigma.n$ appear on a tableau branch
it means that $\sigma\mathit{\mathrm{\mathcal{R}}}\sigma.n$.
The \emph{grounded terms} of \emph{$\mathfrak{L^{\bigstar}}$} are
individual symbols that have the prefixes of tableau nodes as subscripts.
Grounded terms are of two different kinds, \emph{grounded names} and
\emph{parameters}. Grounded names are the same symbols as the individual
constants of \emph{$\mathfrak{L}$} (the lower case letters \emph{a}
through \emph{j} ), each with a tableau prefix as subscript. Parameters
are the lower case letters \emph{k} through \emph{t} (not used in
\emph{$\mathfrak{L}$}) with this same kind of subscript. Examples
of grounded names are $a_{1.1.2},$ $b_{***@.2.1},$ $c_{1},$ and
$d_{***@.2.1.@}.$ Similarly, $k_{1.1.2},$ $p_{***@.2.1},$ $q_{1},$
and $r_{***@.2.1.@}$ are parameters.%
\footnote{The individual constants and variables of \emph{$\mathfrak{L},$
}as
defined in section\emph{ }2.1, may be indexed with numerical subscripts
as a way of ensuring that their supply is unlimited. Strictly speaking
the new grounded terms of \emph{$\mathfrak{L^{\bigstar}}$ }should
have this feature as well.\emph{ }In practice one seldom needs more
than a few such symbols of either language and thus seldom needs these
purely indexical subscripts. When such a need arises, indexical and
tableau-node-prefix subscripts can be distinguished by placing the
latter in parentheses after the former. Thus $b_{257(***@.2.1)}$
counts as a grounded name,\emph{ }and $p{}_{3(1.1.1)}$ as a parameter.
In general, a grounded term can be represented as $\tau_{\kappa(\sigma)},$
where $\tau$ is one of the lower case letters \emph{a} through \emph{t},
$\kappa$ is an indexical subscript, and $\sigma$ is a tableau prefix. %
}
\emph{$\mathfrak{L^{\bigstar}}$} is like \emph{$\mathfrak{L}$} except
that the new grounded terms function like rigidly designating names.
Syntactically, they behave exactly like the individual constants of
\emph{$\mathfrak{L}$. }That is, they may appear in atomic formulas
and as the terms that follow predicate abstracts. (Thus if
$\langle\lambda\alpha.\phi\rangle$
is a predicate abstract and $\tau_{\sigma}$ is a grounded term,
$\langle\lambda\alpha.\phi\rangle(\tau_{\sigma})$
is a formula of \emph{$\mathfrak{L^{\bigstar}}$}. The free variable
occurrences in $\langle\lambda\alpha.\phi\rangle(\tau_{\sigma})$
are the same as those in $\langle\lambda\alpha.\phi\rangle$.) But
grounded terms never play the variable-binding role in quantification
or predicate abstraction.
Semantically, the grounded terms of \emph{$\mathfrak{L^{\bigstar}}$}
behave like the variables of \emph{$\mathfrak{L}$} in that they are
assigned their \emph{designata} by a valuation \emph{$\mathcal{V}$}
rather than by an interpretation $\mathcal{I}$ of a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$.
So given a grounded term $\tau_{\sigma}$, a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
and a valuation\emph{ $\mathcal{V}$} relative to
$\mathit{\mathrm{\mathcal{M}}}$,
\emph{$\mathcal{V}(\tau_{\sigma})\in\mathcal{D_{M}}$. }Thus unlike
an individual constant, whose denotation (if any) at a world is always
drawn from the domain of that world, a grounded term is assigned a
single, model-wide denotation from the domain of the model.%
\footnote{Subscripting an individual constant $\tau$ with a prefix is
similar
to applying Kaplan's \cite{Kaplan1979a} operator \emph{dthat} to
$\tau$. %
}
With these stipulations in place, the definition of \emph{satisfaction
}of a formula of \emph{$\mathfrak{L^{\bigstar}}$} by a valuation\emph{
$\mathcal{V}$} at a world\emph{ }$w$ of a model
$\mathit{\mathrm{\mathcal{M}}},$
is exactly like that given for \emph{$\mathfrak{L}$} in section 3.4.
Similarly for the definitions of the\emph{ satisfiability }of a formula
of\emph{ $\mathfrak{L^{\bigstar}}$} and \emph{satisfiability }of
a set of formulas of\emph{ $\mathfrak{L^{\bigstar}}$.} But sections
3.5 and 3.6 define terms (truth at a world in a model, truth
\emph{simpliciter},
validity, consequence, and equivalence) that apply only to sentences
of \emph{$\mathfrak{L}$}. None of these terms apply to formulas of
\emph{$\mathfrak{L^{\bigstar}}$} that are not sentences of
\emph{$\mathfrak{L}$}.
\subsubsection{The General Structure of Tableaus}
The purpose of tableaus is to generate proofs of logical consequence
and validity for arguments and sentences, respectively, of
\emph{$\mathfrak{L}$}.
Hence the formulas that appear as parts of the initial nodes of a
tableau are always sentences of \emph{$\mathfrak{L}.$}
A tableau test for an argument of \emph{$\mathfrak{L}$} with premises
$\gamma{}_{1},$ $\gamma_{2},$ ... , $\gamma{}_{n}$ and conclusion
$\phi$ begins with the following \emph{n }+1 nodes:
\medskip{}
$\begin{array}[t]{lllllllllllllllllllllllllllllll}
& & & & & & & & & & & & & 1\,\,\gamma_{1}\\
& & & & & & & & & & & & & 1\,\,\gamma_{2}\\
& & & & & & & & & & & & & \,\,\vdots\\
& & & & & & & & & & & & & 1\,\,\gamma_{n}\\
& & & & & & & & & & & & & 1\,\,\neg\phi
\end{array}$\medskip{}
A tableau test for a single sentence $\phi$ of \emph{$\mathfrak{L}$}
begins with the single node
\medskip{}
$\begin{array}{cccccccccccccc}
& & & & & & & & & & & & & 1\,\,\neg\phi\end{array}$\medskip{}
The result of applying a tableau rule to a node or nodes of a tableau
will be the addition of one or more nodes, each a prefixed formula
of \emph{$\mathfrak{L^{\bigstar}},$} to the tableau. None of these
formulas will contain free occurrences of variables.
Some tableau rules produce branching. The construction of a branch
terminates when no more rules can be applied to any node on the branch,
or when some prefixed formula and the negation of this formula with
the same prefix ($\sigma\,\,\phi$ and $\sigma\,\,\neg\phi$) appear
as nodes on the branch. In the latter case the branch is said to be
\emph{closed}. A branch that is not closed is \emph{open}. A tableau
is \emph{closed} if all of its branches are closed.
A closed tableau beginning with $1\,\,\gamma_{1},$ $1\,\,\gamma_{2},$
... , $1\,\,\gamma{}_{n},$ and $1\,\,\neg\phi$ (where the
$\gamma_{i}\,(1\leq i\leq n)$
and $\neg\phi$ are, as specified above, all sentences of
\emph{$\mathfrak{L}$})\emph{
}is a \emph{derivation of} $\phi$ \emph{from} \{$\gamma_{1},$ $\gamma_{2},$
... , $\gamma_{n}$\}. If $\Gamma$ is a set of sentences of\emph{
$\mathfrak{L}$}, each $\gamma_{i}\,(1\leq i\leq n)\in\Gamma,$ and
there is a derivation of $\phi$ from \{$\gamma_{1},$ $\gamma_{2},$
... , $\gamma_{n}$\}, $\phi$ is said to be \emph{derivable from
}$\Gamma$ (abbreviated $\mathrm{\Gamma\vdash\phi}$). Similarly,
a closed tableau beginning with $1\,\,\neg\phi$ (where, again, $\phi$
is a sentence of \emph{$\mathfrak{L}$})\emph{ }is a \emph{proof }of
$\phi$. If there is such a proof $\phi$ is said to be a \emph{theorem}
(abbreviated $\mathrm{\vdash\phi}$).
In the Appendix I prove that a tableau is closed if and only if the
sentences of \emph{$\mathfrak{L}$} with which it begins are inconsistent
(i.e., there is no interpretation under which all of these sentences
are true). Thus validity coincides with theoremhood and, for finite
sets of premises, logical consequence coincides with derivability.
The foregoing holds for each of the five systems under consideration.
These proofs are based on the fact that an open tableau branch mimics
a model \emph{cum }valuation of \emph{$\mathfrak{L^{\bigstar}}$.}
The intuitive idea is that node prefixes designate worlds (\textbf{@}
designates the actual world), $\sigma\,\,\phi$ asserts that formula
$\phi$ is satisfied by the valuation at world $\sigma$, and the
appearance of $\sigma.n$ as a node prefix indicates that
$\sigma\mathcal{R}\sigma.n$.
\subsection{Tableau Rules}
\subsubsection{Truth-Functional Connectives}
Rules for conjunction, negated conjunction, and double negation are
standard and can be represented as follows:
\medskip{}
\begin{tabular}{lllllcccccl}
$\sigma\,\,\phi\wedge\psi$ & & & & & $\sigma\,\,\neg(\phi\wedge\psi)$ & & &
& & $\sigma\,\,\neg\neg\phi$\tabularnewline
\cline{1-1} \cline{6-6} \cline{11-11}
$\sigma\,\,\phi$ & & & & & $\sigma\,\,\neg\phi\mid\sigma\,\,\neg\psi$ & & &
& & $\sigma\,\,\phi$\tabularnewline
$\sigma\,\,\psi$ & & & & & & & & & & \tabularnewline
\end{tabular}
\medskip{}
The conjunction and double negation rules add the indicated nodes
to each branch in which the top node appears. The double negation
node produces branching in the usual way. Rules for the other
truth-functional
connectives are also standard and can be derived from those given
here.
\subsubsection{Modal and Actuality Connectives}
The SAT rules for necessity and negated necessity are the standard
ones for T. The negated necessity rule is:
\medskip{}
\begin{tabular}{lll}
$\sigma\,\,\neg\square\phi$ & $\sigma.n$ is new to the branch &
\tabularnewline
\cline{1-1}
$\sigma.n\,\,\neg\phi$ & & \tabularnewline
\end{tabular}
\medskip{}
For each branch containing $\sigma\,\,\neg\square\phi$ this rule
is applied just once, and integer $n$ is chosen so that prefix $\sigma.n$
is new to the branch. The necessity rule for SAT takes two forms.
\medskip{}
\begin{tabular}{cc}
1. & $\sigma\,\,\square\phi$\tabularnewline
\cline{2-2}
& $\sigma\,\,\phi$\tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{ccc}
2. & $\sigma\,\,\square\phi$ & if the prefix $\sigma.n$ appears somewhere
on the branch\tabularnewline
\cline{2-2}
& $\sigma.n\,\,\phi$ & \tabularnewline
\end{tabular}
\medskip{}
Form 2 generally adds multiple nodes to a branch. And as new prefixes
come to appear on a branch form 2 is reapplied, using these prefixes,
to nodes to which it has already been applied using other prefixes.
Tableau rules for the other logics under consideration are also standard.
SAK uses only form 2 of the necessity rule. For SAB, SAS4, and SAS5
three additional forms are needed.
\medskip{}
\begin{tabular}{lll}
3. & $\sigma.n\,\,\square\phi$ & if the prefix $\sigma.n$ appears somewhere
on the branch\tabularnewline
\cline{2-2}
& $\sigma\,\,\phi$ & \tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{ccc}
4. & $\sigma\,\,\square\phi$ & if the prefix $\sigma.n$ appears somewhere
on the branch\tabularnewline
\cline{2-2}
& $\sigma.n\,\,\square\phi$ & \tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
5. & $\sigma.n\,\,\square\phi$ & if the prefix $\sigma.n$ appears somewhere
on the branch\tabularnewline
\cline{2-2}
& $\sigma\,\,\square\phi$ & \tabularnewline
\end{tabular}
\medskip{}
\noindent SAB retains forms 1 and 2 and adds form 3. SAS4 uses forms
1 and 4. SAS5 uses forms 1, 4, and 5. Since $\lozenge$ and $\square$
are interdefinable, rules for $\lozenge$ and $\neg\lozenge$ can
be derived from the ones given here.%
\footnote{For more on tableau rules for K, T, B, S4, and S5 see
\cite{Fitting1998},
p. 51-55. %
}
Rules for the actuality connective reflect the idea that a sentence
is actually true at a world just in case is true at the actual world.
\medskip{}
\begin{tabular}{ccccccllllllllll}
& & & & & & $\sigma\,\,\mathsf{A}\phi$ & & & & & & & & &
$\sigma\,\,\neg\mathsf{A}\phi$\tabularnewline
\cline{7-7} \cline{16-16}
& & & & & & \textbf{@}$\,\,\phi$ & & & & & & & & & \textbf{@
}$\,\,\neg\phi$\tabularnewline
\end{tabular}
\medskip{}
\subsubsection{Quantifiers}
Where $\alpha$ is a variable, let $\psi(\alpha)$ be a formula of
\emph{$\mathfrak{L^{\bigstar}}$ }containing at least one free occurrence
of $\alpha$ (but no free occurrence of any other variable). Let
$\tau_{\sigma}$
and $\pi_{\sigma}$ be a grounded term and a parameter, respectively,
each subscripted with the tableau prefix $\sigma$.%
\footnote{Thus $\tau_{\sigma}$ is either a parameter or a grounded name. %
} $\psi(\tau_{\sigma})$ stands for the result of replacing all free
occurrences of $\alpha$ in $\psi(\alpha)$ with $\tau_{\sigma}$.
Similarly for $\psi(\pi_{\sigma})$ and $\pi_{\sigma}$. The universal
quantifier and negated universal quantifier rules are as follows,
where $\tau_{\sigma}$ is any grounded term that already appears on
the branch, and $\pi_{\sigma}$ is a parameter that is new to the
branch.
\medskip{}
\begin{tabular}{cccccc}
$\sigma\,\,\forall\alpha\psi(\alpha)$ & $\tau_{\sigma}$ appears somewhere &
& & $\sigma\,\,\neg\forall\alpha\psi(\alpha)$ & $\pi_{\sigma}$ is
new\tabularnewline
\cline{1-1} \cline{5-5}
$\sigma\,\,\psi(\tau_{\sigma})$ & on the branch & & &
$\sigma\,\,\neg\psi(\pi_{\sigma})$ & to the branch\tabularnewline
\end{tabular}
\medskip{}
For each branch containing the node $\sigma\,\,\forall\alpha\psi(\alpha)$,
and each grounded term $\tau_{\sigma}$ that appears as part of a
node on that branch, the universal quantifier rule adds
$\sigma\,\,\psi(\tau_{\sigma})$
to the branch. (If no grounded term appears with the tableau prefix
$\sigma$ as subscript in any node on a branch containing
$\sigma\,\,\forall\alpha\psi(\alpha)$,
the universal quantifier rule is not applied to
$\sigma\,\,\forall\alpha\psi(\alpha)$
on that branch. This reflects the fact that the domain of a world
may be empty.) For each branch containing the node
$\sigma\,\,\neg\forall\alpha\psi(\alpha)$,
the negated universal quantifier rule is applied just once, and the
parameter $\pi_{\sigma}$ must be chosen so that it is new to the
branch.
The universal quantifier rule (and the dual negated existential quantifier
rule) reflect the fact that SAT is an actualistic free logic. Actualism
requires quantification to be world relative, and a free logic permits
instantiation at a world only with terms that denote objects in the
domain of that world. The negated universal quantifier rule (and the
dual existential rule) also reflect actualism in requiring that the
term being instantiated denote an object in the domain of the world
in question.
\subsubsection{Predicate Abstraction}
According to serious actualism an attributive sentence is true at
a world only if the object denoted by the term to which the abstract
applies exists at that world. In order to fully reflect this requirement
the (unnegated) predicate abstraction rule takes three forms. Form
1 ``grounds'' or ``rigidifies'' an individual constant governed
by a predicate abstract, thus transforming it into a grounded name.\emph{
}Forms 2 and 3 apply to terms that are already grounded. But since
the subscript of a grounded term may not be the same as the prefix
of the node in which the sentence containing it appears, two rules
are needed.
Suppose $\sigma$ and $\sigma_{1}$ are distinct prefixes, $\iota$
is an individual constant, and $\tau_{\sigma}$ and $\tau_{\sigma_{1}}$
are grounded terms. Forms 1 and 2 instantiate the predicate abstract
with $\iota_{\sigma}$ and $\tau_{\sigma}$, respectively. Form 3
instantiates it with $\tau_{\sigma_{1}}$, and it introduces a second
node. This second node reflects the fact that, since
$\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$
is true at world $\sigma$, $\tau_{\sigma_{1}}$ denotes an object
that exists in $\sigma$ as well as in $\sigma_{1}$.%
\footnote{Form 3 can be simplified so as to introduce only the second
conclusion
stated here. The first conclusion can be derived using form 2 and
the substitutivity of identity rule (section 8.2.5). %
}
\medskip{}
\begin{tabular}{lll}
1. & $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$ & $\iota$
is an individual constant of \emph{$\mathfrak{L}$ }\tabularnewline
\cline{2-2}
& $\sigma\,\,\psi(\iota_{\sigma})$ & ($\iota_{\sigma}$ is thus a grounded
name of $\mathfrak{L^{\bigstar}}$)\tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
2. & $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$ &
$\tau_{\sigma}$ is a grounded term \tabularnewline
\cline{2-2}
& $\sigma\,\,\psi(\tau_{\sigma})$ & \tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
3. &
$\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$ &
$\tau_{\sigma_{1}}$ is a grounded term, and $\sigma\neq\sigma_{1}$
\tabularnewline
\cline{2-2}
& $\sigma\,\,\psi(\tau_{\sigma_{1}})$ & \tabularnewline
& $\sigma\,\,(\pi_{\sigma}=\tau_{\sigma_{1}})$ & $\pi_{\sigma}$ is a
parameter that is new to the branch\tabularnewline
\end{tabular}
\medskip{}
\noindent It should be noted that form 1 of the predicate abstraction
rule and form 1 of the atomic formula rule are the only rules that
introduce grounded names into tableaus.
The rule for negated predicate abstraction also has three forms. Each
form applies to a tableau node that, except for the negation sign,
is the same as the node in the correspondingly numbered form of the
positive predicate abstraction rule.%
\footnote{Form 3 need not be taken as primitive. It's conclusion can be
obtained
using the substitutivity of identity rule (section 8.2.5) and form
2 of the negated predicate abstraction rule. %
}
\medskip{}
\begin{tabular}{lll}
1. & $\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$ &
$\iota$ is an individual constant, and the grounded name $\iota_{\sigma}$
\tabularnewline
\cline{2-2}
& $\sigma\,\,\neg\psi(\iota_{\sigma})$ & appears somewhere on the
branch\tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
2. &
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$ &
$\tau_{\sigma}$ is a grounded term \tabularnewline
\cline{2-2}
& $\sigma\,\,\neg\psi(\tau_{\sigma})$ & \tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
3. &
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$
& $\tau_{\sigma_{1}}$ is a grounded term, and
$\sigma\neq\sigma_{1}$\tabularnewline
& $\sigma_{2}\,\,(\upsilon{}_{\sigma}=\tau_{\sigma_{1}})$ & $\sigma_{2}$ is
any prefix; $\upsilon_{\sigma}$ is any term grounded
with $\sigma$\tabularnewline
\cline{2-2}
& $\sigma\,\,\neg\psi(\tau_{\sigma_{1}})$ & \tabularnewline
\end{tabular}
\medskip{}
\noindent In form 1 the presence of the grounded name $\iota_{\sigma}$
somewhere on the branch assures us that the individual constant $\iota$
designates, at world $\sigma,$ a member of the domain of $\sigma.$
($\iota$ need not appear with subscript $\sigma$ in the premise
of the rule.) If $\iota_{\sigma}$ did not appear on the branch, we
couldn't be sure that $\iota$ designates anything in the domain of
$\sigma$. But then we couldn't be sure that $\neg\psi(\iota)$ is
true in $\sigma$. For suppose $\theta$ is a primitive predicate,
$\iota$ does not designates at $\sigma$, and $\psi(\iota)$ is
$\neg\,\theta(\iota)$.
Then $\theta(\iota)$ is false at $\sigma$ and so is $\neg\psi(\iota)$.
The rationale for form 2 should be obvious. Form 3 is similar to from
1 in that the predicate abstract applies to a term that is not grounded
in $\sigma$. Thus assurance is needed that $\tau_{\sigma_{1}}$ really
does denote an object in the domain of world $\sigma$. The appearance
of $\sigma_{2}\,\,(\upsilon{}_{\sigma}=\tau_{\sigma_{1}})$ somewhere
on the branch provides this. If $\tau_{\sigma_{1}}$ did not denote
an object in the domain of world $\sigma$, $\neg\psi(\tau_{\sigma_{1}})$
might be false at $\sigma$, as in the case of form 1.
\subsubsection{Identity }
The self-identity rule reflects the fact that in SAT a sentence of
the general form $\beta=\beta$ is true at a world only if $\beta$
designates an object that exists at that world. Since the appearance
of a grounded term $\tau_{\sigma}$ in any node on a branch indicates
that the object it denotes exists at world $\sigma$, that object
must be self-identical at $\sigma.$ Thus where $\tau_{\sigma}$ is
any grounded term, the self-identity rule takes the following form:%
\footnote{The blank space above the horizontal line indicates that this rule
has no premise. %
}
\medskip{}
\begin{tabular}{ccc}
& & $\tau_{\sigma}$ appears somewhere on the branch \tabularnewline
\cline{1-1}
$\sigma\,\,(\tau_{\sigma}=\tau_{\sigma})$ & & \tabularnewline
\end{tabular}
\medskip{}
As usual, the substitutivity of identity rule sanctions substituting
co-referential rigid designators for each other, but in SAT it requires
some new notation and takes a rather complicated form. Suppose $\sigma_{1}$,
$\sigma_{2}$, $\sigma_{3}$, and $\sigma_{4}$ are prefixes of branch
nodes (not necessarily distinct), $\tau_{\sigma_{3}}$ and
$\upsilon_{\sigma_{4}}$
are grounded terms, and $\phi$ and $\psi$ are formulas of
\emph{$\mathfrak{L^{\bigstar}}$
}that contain no free occurrences of any variable. Suppose also that
$\phi$ and $\psi$ are alike except that $\psi$ contains occurrences
of $\upsilon_{\sigma_{4}}$ at one or more places where $\phi$ contains
occurrences of $\tau_{\sigma_{3}}$. If
$\tau_{\sigma_{3}}=\upsilon{}_{\sigma_{4}}$
holds at any world, \emph{$\mathcal{V}$} assigns the same member
of $\mathcal{D_{M}}$ to $\tau_{\sigma_{3}}$ and $\upsilon_{\sigma_{4}}.$
So if $\tau_{\sigma_{3}}=\upsilon_{\sigma_{4}}$ holds at $\sigma_{1}$
and $\phi$ holds at $\sigma_{2}$, $\psi$ also holds at $\sigma_{2}$.
(And the object denoted by $\tau_{\sigma_{3}}$ and $\upsilon_{\sigma_{4}}$
exists in the domains of worlds $\sigma_{1}$, $\sigma_{3}$, and
$\sigma_{4}$, and possibly in the domain of world $\sigma_{2}$.)
The substitutivity rule is thus:
\medskip{}
\begin{tabular}{l}
$\sigma_{1}\,\,\tau_{\sigma_{3}}=\upsilon_{\sigma_{4}}$\tabularnewline
$\sigma_{2}\,\,\phi$\tabularnewline
\hline
$\sigma_{2}\,\,\psi$\tabularnewline
\end{tabular}
\medskip{}
This rule is the only one that has two premises. Thus it can be applied
only when both of these premises appear on the same branch.
\subsubsection{Atomic Formulas of \emph{$\mathfrak{L^{\bigstar}}$}}
An atomic formula is satisfied by an \emph{n}-tuple of objects at
a world only if all those objects exist at that world. So each individual
term that appears in such a formula, whether grounded or ungrounded,
must designate an object that exists at that world. This fact must
be reflected in the tableau rules, and so, unlike other tableau systems,
SAT has a rule for atomic formulas. The rule has three forms, and
some additional notation will facilitate understanding. Where $\theta$
is an \emph{n}-ary predicate and $\tau$ and $\upsilon$ are terms,
$\theta(...\tau...)$ will stand for an atomic formula in which $\tau$
has one or more occurrences, and $\theta(...\upsilon...)$ for the
result of replacing each occurrence of $\tau$ in $\theta(...\tau...)$
with $\upsilon$.\emph{}%
\footnote{Although atomic formulas other than identities do not contain
parentheses
(see section 2.2), the use of parentheses in the metalinguistic
representation
of atomic formulas enhances readability. %
}
The first two forms of the rule are:
\medskip{}
\begin{tabular}{lll}
1. & $\sigma\,\,\theta(...\iota...)$ & $\iota$ is an individual constant of
\emph{$\mathfrak{L}$ }\tabularnewline
\cline{2-2}
& $\sigma\,\,\theta(...\iota_{\sigma}...)$ & ($\iota_{\sigma}$ is thus a
grounded name of $\mathfrak{L^{\bigstar}}$)\tabularnewline
\end{tabular}
\medskip{}
\begin{tabular}{lll}
2. & $\sigma\,\,\theta(...\tau_{\sigma_{1}}...)$ & $\tau_{\sigma_{1}}$ is a
grounded term, and $\sigma\neq\sigma_{1}$ \tabularnewline
\cline{2-2}
& $\sigma\,\,(\pi_{\sigma}=\tau_{\sigma_{1}})$ & $\pi_{\sigma}$ is a
parameter that is new to the branch\tabularnewline
\end{tabular}
\medskip{}
These two forms of the rule reflect the fact that an atomic sentence
is true at a world only if each of the terms it contains denotes an
object that exists at that world. As noted in section 8.2.4, form
1 of the predicate abstraction rule and form 1 of the atomic formula
rule are the only rules that introduce grounded names into tableaus.%
\footnote{It's important to notice that forms 1 and 2 apply to the case
where
$\theta$ is the identity predicate. If $\iota$ is an individual
constant, $\theta(...\iota...)$ is $(\iota=...)$ or $(...=\iota)$.
Similarly, if $\tau_{\sigma_{1}}$ is a grounded term,
$\theta(...\tau_{\sigma_{1}}...)$
is $(\tau_{\sigma_{1}}=...)$ or $(...=\tau_{\sigma_{1}})$.%
}
The third form of the atomic formula rule is unlike any other tableau
rule in that it allows a subscript to be removed from a grounded name.%
\footnote{This form does not apply to parameters, since the result of
removing
the tableau-prefix subscript from a parameter is not a symbol of either
\emph{$\mathfrak{L}$} or \emph{$\mathfrak{L^{\bigstar}}$.} %
} It is also unlike the first two forms in that it may be applied to
some but not all occurrences of an individual symbol in an atomic
formula. Let $\iota$ be an individual constant\emph{ }and $\iota_{\sigma}$
that same individual constant subscripted with $\sigma$. $\iota_{\sigma}$
is thus a grounded name. If $\iota_{\sigma}$ appears in an atomic
formula as part of a tableau node with prefix $\sigma$, one or more
occurrences of $\iota_{\sigma}$ may be replaced with $\iota$. To
call attention to the fact that form 3 of the rule allows replacement
of some but not all occurrences of a term in an atomic formula, I'll
use a new notation. Let $\theta(\iota_{\sigma})$ and $\theta(\iota)$
stand for atomic formulas that are alike except that $\theta(\iota)$
contains occurrences of $\iota$ at one or more places where
$\theta(\iota_{\sigma})$
contains occurrences of $\iota_{\sigma}$.
The third form of the atomic formula rule is:
\medskip{}
\begin{tabular}{lll}
3. & $\sigma\,\,\theta(\iota_{\sigma})$ & $\iota_{\sigma}$ is a grounded
name of \emph{$\mathfrak{L^{\bigstar}}$}\tabularnewline
\cline{2-2}
& $\sigma\,\,\theta(\iota)$ & ($\iota$ is thus an individual constant of
\emph{$\mathfrak{L}$)}\tabularnewline
\end{tabular}
\medskip{}
Like the first two forms, form 3 also reflects the fact that an atomic
sentence is true at a world only if each of the terms it contains
denotes an object that exists at that world.%
\footnote{As in the case of forms 1 and 2, it's important to notice that
form
3 applies where $\theta$ is the identity predicate, $\iota_{\sigma}$
is a grounded name, and $\theta(\iota_{\sigma})$ is thus
$(\iota_{\sigma}=...)$
or $(...=\iota_{\sigma})$. %
}
\subsection{Examples of Tableaus}
In the following examples tableau rules are referred to by abbreviated
names. For example, $\neg\rightarrow$ denotes the negated conditional
rule, $\neg\lambda2$ the second form of the negated abstraction rule,
Subs= the substitution of identity rule.
\subsubsection{The Converse Barcan Formula (CBF)}
The converse Barcan formula is SAT valid, as the following tableau
for a simple instance of (CBF) shows.
\medskip{}
\begin{tabular}{lllllcccccl}
& & & & $1\,\,\,\,\,\,\,\neg(\exists x\lozenge\langle\lambda
y.Fy\rangle(x)\rightarrow\lozenge\exists x\langle\lambda y.Fy\rangle(x))$
~~~~1. & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\exists x\lozenge\langle\lambda
y.Fy\rangle(x)$~~~~~~~2.
(From 1 by $\neg\rightarrow$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\lozenge\exists x\langle\lambda
y.Fy\rangle(x)$~~~~~3.
(From 1 by $\neg\rightarrow$.) & & & & & &
\multicolumn{1}{l}{}\tabularnewline
& & & & $1\,\,\,\,\,\,\,\lozenge\langle\lambda
y.Fy\rangle(p_{1})$~~~~~~~~~4.
(From 2 by $\exists$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\langle\lambda y.Fy\rangle(p_{1})$~~~~~~~~~~~~5.
(From 4 by $\lozenge$.) & & & & & & \tabularnewline
& & & & $1.1\,\, Fp_{1}$~~~~~~~~~~~~~~~~~~~~~~6. (From
5 by $\lambda3$.) & & & & & & \tabularnewline
& & & & $1.1\,\,(q_{1.1}=p_{1})$~~~~~~~~~~~~~~7. (From 5 by
$\lambda3$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg\exists x\langle\lambda y.Fy\rangle(x)$~~~~~~~8.
(From 3 by $\neg\lozenge2$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg\langle\lambda y.Fy\rangle(q_{1.1})$~~~~~~~~9.
(From 8 by $\neg\exists$, using $q_{1.1}$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg Fq_{1.1}$~~~~~~~~~~~~~~~~~~~10. (From
9 by $\neg\lambda2$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg Fp_{1}$~~~~~~~~~~~~~~~~~~~~11. (From
7 and 10 by Subs=.) & & & & & & \tabularnewline
& & & & ~~~~~~~~$\times$ & & & & & & \tabularnewline
\end{tabular}
\medskip{}
The use of variables other than \emph{x} and \emph{y} would not affect
this proof. And since none of the rules for atomic formulas have been
applied, replacing \emph{Fy} with any complex formula $\phi(y)$ would
not avoid closure.
\subsubsection{An Imposter (\emph{faux} CBF)}
In section 4.4 I dubbed formulas of the form
\begin{quotation}
$\square\forall\alpha_{1}\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})\rightarrow\forall\alpha_{1}\square\langle\lambda\alpha_{2}.\phi(\alpha_{2})\rangle(\alpha_{1})$
\end{quotation}
(\emph{faux} CBF). Not all formulas of this form are SAT valid, as
the following tableau shows.
\medskip{}
\begin{tabular}{lllllcccccl}
& & & & $1\,\,\,\,\,\,\,\neg(\square\forall x\langle\lambda
y.Fy\rangle(x)\rightarrow\forall x\square\langle\lambda
y.Fy\rangle(x))$~~~~1. & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\square\forall x\langle\lambda
y.Fy\rangle(x)$~~~~~~~2.
(From 1 by $\neg\rightarrow$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\forall x\square\langle\lambda
y.Fy\rangle(x)$~~~~~3.
(From 1 by $\neg\rightarrow$.) & & & & & &
\multicolumn{1}{l}{}\tabularnewline
& & & & $1\,\,\,\,\,\,\,\forall x\langle\lambda y.Fy\rangle(x)$~~~~~~~~~4.
(From 2 by $\square1$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\square\langle\lambda
y.Fy\rangle(p_{1})$~~~~~~~5.
(From 3 by $\neg\forall$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\langle\lambda y.Fy\rangle(p_{1})$~~~~~~~~~~~6.
(From 4 by $\forall$, using $p_{1}$) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\, Fp_{1}$~~~~~~~~~~~~~~~~~7. (From
6 by $\lambda1$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg\langle\lambda y.Fy\rangle(p_{1})$~~~~~8. (From
5 by $\neg\square$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\forall x\langle\lambda y.Fy\rangle(x)$~~~~~9. (From
2 by $\square2$.) & & & & & & \tabularnewline
& & & & ~~~~~~~~~~~~~$\circ$ & & & & & & \tabularnewline
\end{tabular}
\medskip{}
\subsubsection{Predicate Abstraction applied to Atomic Formulas is
Inessential}
A main theme of this paper is the importance of predicate abstraction
for a coherent account of logical form in quantified modal logic.
The tableaus in this section and the next illustrate this by showing
that while
\begin{quotation}
$\langle\lambda x.Fx\rangle(a)\leftrightarrow Fa$
\end{quotation}
is SAT valid,
\begin{quotation}
$\langle\lambda x.\neg Gx\rangle(a)\leftrightarrow\neg Ga$
\end{quotation}
is not. Here's the first tableau.
\medskip{}
\begin{tabular}{llllc}
& & & $1\,\,\neg(\langle\lambda x.Fx\rangle(a)\leftrightarrow Fa)$~~1. &
\tabularnewline
\end{tabular}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$\diagup$$\diagdown$
~~~~~~~~~~~~~~~~~~~~~~~~~~~~$\diagup$~~~~~~~~~$\diagdown$
~~~~~~~~~~~~~~~~~~~~~~~$\diagup$~~~~~~~~~~~~~~~~~~$\diagdown$
\begin{tabular}{lllll}
& & & & $1\,\,\langle\lambda y.Fy\rangle(a)$~~2.\tabularnewline
& & & & $1\,\,\neg Fa$~~3.\tabularnewline
& & & & $1\,\, Fa_{1}$~~~6.\tabularnewline
& & & & $1\,\, Fa$~~~~7.\tabularnewline
& & & & ~~~~~$\times$\tabularnewline
\end{tabular}%
\begin{tabular}{l}
$1\,\,\neg\langle\lambda x.Fx\rangle(a))$ ~~4.\tabularnewline
$1\,\, Fa$~~~~~~5.\tabularnewline
$1\,\, Fa_{1}$~~~~~8.\tabularnewline
$1\,\,\neg Fa_{1}$ ~~9.\tabularnewline
~~~~~$\times$\tabularnewline
\end{tabular}
\medskip{}
In the left branch $\lambda1$ applied to line 2 yields line 6, and
Atomic 3 applied to line 6 yields line 7. In the right branch Atomic
1 applied to line 5 yields line 8, which is the first node in the
right branch that contains $a_{1}$. The appearance of $a_{1}$ makes
it possible to apply $\neg\lambda1$ to line 4, which yields line
9 and closure. If $a_{1}$ did not appear on the right branch, $\neg\lambda1$
could not be applied to line 4. And if the only appearances of $a$
on the right branch were as parts of non-atomic sentences, Atomic
1 could not be applied and $a_{1}$ would not come to appear on the
branch. So the right branch closes only because $a$ appears on it
as part of an \emph{atomic} sentence. The next section contains a
tableau (for a sentence with a similar form) that fails to close for
exactly this reason.
\subsubsection{Predicate Abstraction applied to Non-atomic Formulas
\emph{is} Essential}
If $Fx$ and $Fa$ in $\langle\lambda x.Fx\rangle(a)\leftrightarrow Fa$
are replaced by non-atomic formulas $\phi(x)$ and $\phi(a)$, the
tableau for the resulting formula may not close. For example, consider
the tableau for $\langle\lambda x.\neg Gx\rangle(a)\leftrightarrow\neg Ga$.
\medskip{}
\begin{tabular}{llllc}
& & & $1\,\,\neg(\langle\lambda x.\neg Gx\rangle(a)\leftrightarrow\neg
Ga)$)~~1. & \tabularnewline
\end{tabular}
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$\diagup$$\diagdown$
~~~~~~~~~~~~~~~~~~~~~~~~~~~~$\diagup$~~~~~~~~~$\diagdown$
~~~~~~~~~~~~~~~~~~~~~~~$\diagup$~~~~~~~~~~~~~~~~~~$\diagdown$
\begin{tabular}{lllll}
& & & & $1\,\,\langle\lambda y.\neg Gy\rangle(a)$~~2.\tabularnewline
& & & & $1\,\,\neg\neg Ga$~~3.\tabularnewline
& & & & $1\,\, Ga$~~~~~~6. \tabularnewline
& & & & $1\,\, Ga_{1}$~~~~~7. \tabularnewline
& & & & $1\,\,\neg Ga_{1}$~~~8. \tabularnewline
& & & & ~~~~~$\times$\tabularnewline
\end{tabular}%
\begin{tabular}{l}
$1\,\,\neg\langle\lambda x.\neg Gx\rangle(a)$ ~~4.\tabularnewline
$1\,\,\neg Ga$~~5.\tabularnewline
~~~~~~~$\circ$\tabularnewline
\tabularnewline
\tabularnewline
\end{tabular}
\medskip{}
The left branch is the same as that of the tableau in the previous
section except for the use of double negation. But on the right branch
no rule can be applied to line 4 or line 5. Since the sentence on
line 5 is not atomic the grounded name $a_{1}$ cannot be introduced,
and in its absence $\neg\lambda1$ cannot be applied to line 4. The
right branch is thus open.
\subsubsection{Other Imposters}
Consider the formulas $\exists x\lozenge Fx\rightarrow\lozenge\exists xFx$
and $\exists x\lozenge\neg Fx\rightarrow\lozenge\exists x\neg Fx$.
In most systems of quantified modal logic both are considered instances
of the converse Barcan formula, and either both are valid or both
invalid. But in SAT neither is an instance (CBF) because neither contains
predicate abstracts. Yet in view of sections 8.3.1, 8.3.3 and 8.3.4
it should not be surprising that the tableau for $\exists x\lozenge
Fx\rightarrow\lozenge\exists xFx$
closes but the one for $\exists x\lozenge\neg Fx\rightarrow\lozenge\exists
x\neg Fx$
does not. (I leave it to the reader to verify that the former tableau
is nearly identical to the one given in section 8.3.1 but requires
only nine steps.) The tableau for $\exists x\lozenge\neg
Fx\rightarrow\lozenge\exists x\neg Fx$
follows.
\medskip{}
\begin{tabular}{lllllcccccl}
& & & & $1\,\,\,\,\,\,\,\neg(\exists x\lozenge\neg
Fx\rightarrow\lozenge\exists x\neg Fx)$
~~~~1. & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\exists x\lozenge\neg Fx$~~~~~~~2. (From 1
by $\neg\rightarrow$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\lozenge\exists x\neg Fx$~~~~~3. (From 1
by $\neg\rightarrow$.) & & & & & & \multicolumn{1}{l}{}\tabularnewline
& & & & $1\,\,\,\,\,\,\,\lozenge\neg Fp_{1}$~~~~~~~~~4. (From 2
by $\exists$.) & & & & & & \tabularnewline
& & & & $1.1\,\,\neg Fp_{1}$~~~~~~~~~~~~5. (From 4 by $\lozenge$.) & & & &
& & \tabularnewline
& & & & $1.1\,\,\neg\exists x\neg Fx$~~~~~~~~6. (From 3 by
$\neg\lozenge2$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\exists x\neg Fx$~~~~~~~~7. (From 3 by
$\neg\lozenge1$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\,\neg\neg Fp_{1}$~~~~~~~~~~8. (From 7 by
$\neg\exists$.) & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\,\, Fp_{1}$~~~~~~~~~~~~~~9. (From 8 by$\neg\neg$.) & &
& & & & \tabularnewline
& & & & ~~~~~~~~~~~$\circ$ & & & & & & \tabularnewline
\end{tabular}
\medskip{}
It is instructive to compare line 5 of the tableau in section 8.3.1
with line 5 of the above tableau. Each is inferred from line 4 of
its respective tableau by the $\lozenge$ rule. In the tableau of
section 8.3.1 the $\lambda3$ rule is applied to line 5, which leads
ultimately to closure. But in the tableau of this section no rule
can be applied to line 5, and it does not close.%
\footnote{This tableau suggests a two-world SAS5 model that falsifies
$\exists x\lozenge\neg Fx\rightarrow\lozenge\exists x\neg Fx$.
The domain of one world contains a single object, and the predicate
\emph{F} holds of that object at that world. The domain of the other
world is empty. Alternatively the second world can contain a distinct
object, with \emph{F} also holding of that object at that world.%
}
\subsubsection{A Tableau for an instance of (\emph{faux} UI)}
In the discussion of the logical properties of quantifiers in section
4.3 I mentioned sentences of a form I called (\emph{faux} UI), and
I gave an instance of it that I claimed is not SAT valid. Here's the
sentence:
\begin{quotation}
$\forall x\square Sx\rightarrow(\mathcal{E}(d)\rightarrow\square Sd$)
\end{quotation}
Its invalidity is shown by the following tableau.
\medskip{}
\begin{tabular}{llllllllllcccccl}
& & & & $1\,\,\,\,\,\neg(\forall x\square Sx\rightarrow(\exists
y(y=d)\rightarrow\square Sd))$~~~~1. & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\forall x\square Sx$~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~2.
(From 1 by $\neg\rightarrow$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\neg(\exists y(y=d)\rightarrow\square
Sd)$~~~~~~~~~~~~~3.
(From 1 by $\neg\rightarrow$.) & & & & & & & & & & &
\multicolumn{1}{l}{}\tabularnewline
& & & & $1\,\,\,\,\,\exists y(y=d)$~~~~~~~~~~~~~~~~~~~~~~~~~~~~4.
(From 3 by $\neg\rightarrow$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\neg\square Sd$~~~~~~~~~~~~~5. (From 3 by
$\neg\rightarrow$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,(p_{1}=d)$~~~~~~~~~~6. (From 4 by $\exists$.) & & & & &
& & & & & & \tabularnewline
& & & & $1\,\,\,\,\,(p_{1}=d_{1})$~~~~~~~~~7. (From 6 by Atomic
1.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\square Sp_{1}$~~~~~~~~~~~~~~8. (From 2
by $\forall$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\,\square Sd_{1}$~~~~~~~~~~~~~~9. (From 2
by $\forall$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\, Sp_{1}$~~~~~~~~~~~~~~~~10. (From 8 by
$\square1$.) & & & & & & & & & & & \tabularnewline
& & & & $1\,\,\,\,\, Sd_{1}$~~~~~~~~~~~~~~~~11. (From 9 by
$\square1$.) & & & & & & & & & & & \tabularnewline
& & & & $1.1\,\,\neg Sd$~~~~~~~~~~~~~~12. (From 5 by $\neg\square$.) & & &
& & & & & & & & \tabularnewline
& & & & $1.1\,\, Sp_{1}$~~~~~~~~~~~~~~~13. (From 8 by $\square2$.) & & & &
& & & & & & & \tabularnewline
& & & & $1.1\,\, Sd{}_{1}$~~~~~~~~~~~~~~~14. (From 9 by $\square2$.) & & &
& & & & & & & & \tabularnewline
& & & & $1.1\,\,(q_{1.1}=d_{1})$~~~~~~15. (From 13 by Atomic 2.) & & & & &
& & & & & & \tabularnewline
& & & & $1.1\,\,(r_{1.1}=d_{1})$~~~~~~16. (From 14 by Atomic 2.) & & & & &
& & & & & & \tabularnewline
& & & & ~~~~~~~~~~~$\circ$ & & & & & & & & & & & \tabularnewline
\end{tabular}
\medskip{}
This tableau is not complete. The rules for self-identity, substitution
of identity, and universal quantifier can be applied in several additional
ways. But the tableau will not close. Indeed its single branch suggests
a simple countermodel to \emph{faux} (UI). In this model,
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
$\mathit{\mathrm{\mathcal{W}}}$ contains two worlds, $w_{1}$ and
$w_{1.1}$, such that $w_{1}\mathcal{R}w_{1}$, $w_{1.1}\mathcal{R}w_{1.1}$,
and $w_{1}\mathcal{R}w_{1.1}$. $\mathit{\mathrm{\mathcal{\mathrm{@}}}}$
may be either $w_{1}$ or $w_{1.1}$. The domains of these worlds
will be the same one-membered set. Anticipating the strategy employed
in the Completeness Lemma (section 9.2) let
$\mathcal{D}(w_{1})=\mathcal{D}(w_{1.1})=\{\{p_{1},d_{1},q_{1.1},r_{1.1}$\}\}.
(Where $\sigma_{1}$, $\sigma_{2}$, and $\sigma_{3}$ are tableau
prefixes and $\tau_{\sigma_{2}}$ and $\upsilon_{\sigma_{3}}$ are
grounded terms, $\{\{p_{1},d_{1},q_{1.1},r_{1.1}\}\}$ is the set
of equivalence classes of grounded terms determined by formulas of
the form $(\tau_{\sigma_{2}}=\upsilon_{\sigma_{3}})$ such that, for
some $\sigma_{1}$, $\sigma_{1}\,\,(\tau_{\sigma_{2}}=\upsilon_{\sigma_{3}})$
is a node on the branch.) The extension of the predicate \emph{S}
at each world is the domain of that world, which in this case is also
the domain of the model. That is,
$\mathcal{I\mathrm{(}}S,w_{1})=\mathcal{I\mathrm{(}}S,w_{1.1})=\{\{p_{1},d_{1},q_{1.1},r_{1.1}\}\}$.
The individual constant \emph{d} denotes $\{p_{1},d_{1},q_{1.1},r_{1.1}\}$
at $w_{1}$, but does not denote at $w_{1.1}$. That is,
$\mathcal{I\mathrm{(}}d,w_{1})=\{p_{1},d_{1},q_{1.1},r_{1.1}\}$,
but $\mathcal{I\mathrm{(}}d,w_{1.1})$ is undefined. For any valuation
\emph{$\mathcal{V}$} relative to this model\emph{ $\mathcal{M}$}
(since the domain of the model has only one member there is only one
such valuation) $\mathcal{M}_{\mathcal{V}}\mathrm{(\forall x\square
Sx\rightarrow(\mathcal{E}(d)\rightarrow\square
Sd\mathcal{\mathrm{))}=\mathrm{\textrm{0}}}}$.%
\footnote{The model \emph{$\mathcal{M}$} and valuation \emph{$\mathcal{V}$}
given here apply to the language \emph{$\mathfrak{L}$}. Since grounded
terms (i.e., grounded names and parameters) are not symbols of
\emph{$\mathfrak{L}$}
they are assigned no values by either \emph{$\mathcal{M}$} or
\emph{$\mathcal{V}$}.
But if we add the stipulation that\emph{ $\mathcal{V}$} assigns
$\{p_{1},d_{1},q_{1.1},r_{1.1}\}$
to $p_{1},d_{1},q_{1.1}$, and $r_{1.1}$, and we leave \emph{$\mathcal{M}$}
unchanged, the result is a model and a valuation of
\emph{$\mathfrak{L^{\bigstar}}$}
that falsify \emph{faux} (UI). %
}
\subsubsection{A Tableau for (Act3)}
In section 6.1 I noted that a central feature of actualism is expressible
as
\begin{description}
\item [{(Act3)}] $\forall x\mathsf{A}\mathcal{E}(x)$.
\end{description}
Although (Act3) is true in the intended model it is not SAT valid,
as the following tableau shows.
\medskip{}
\begin{tabular}{lllllcccccl}
& & & & $1\,\,\,\,\,\neg\forall x\mathsf{A}\exists y(y=x))$~~~~1. & & & & &
& \tabularnewline
& & & & $1\,\,\,\,\,\neg\mathsf{A}\exists y(y=p_{1}))$~~~~~~2. (From
1 by $\neg\forall$.) & & & & & & \tabularnewline
& & & & \textbf{@} ~$\neg\exists y(y=p_{1})$~~~~~~~~~3. (From 2
by $\mathsf{\neg A}$.) & & & & & & \tabularnewline
& & & & ~~~~~~~~~~~~$\circ$ & & & & & & \tabularnewline
\end{tabular}
\medskip{}
The negated existential rule cannot be applied to line 3 because no
parameter with subscript @ appears on the branch. But this tableau
can be used to provide insight into the distinction between logical
truth and \emph{a priori} truth. For suppose we want to prove that
(Act3) is actually true. A plausible way of proceeding would be to
use the tableau method but start by supposing that (Act3) is false
in the actual world. So we would get:
\medskip{}
\begin{tabular}{lllllcccccl}
& & & & \textbf{@} ~$\neg\forall x\mathsf{A}\exists y(y=x))$~~~~1. & & & &
& & \tabularnewline
& & & & \textbf{@} ~$\neg\mathsf{A}\exists y(y=p_{@}))$~~~~~~2. (From
1 by $\neg\forall$.) & & & & & & \tabularnewline
& & & & \textbf{@} ~$\neg\exists y(y=p_{@})$~~~~~~~~~3. (From 2
by $\mathsf{\neg A}$.) & & & & & & \tabularnewline
& & & & \textbf{@} ~$\neg(p_{@}=p_{@})$~~~~~~~~~~4. (From 3 by
$\neg\exists$.) & & & & & & \tabularnewline
& & & & \textbf{@} ~$(p_{@}=p_{@})$~~~~~~~~~~~~5. (By Self =.) & & & & & &
\tabularnewline
& & & & ~~~~~~~~$\times$ & & & & & & \tabularnewline
\end{tabular}
\medskip{}
The assumption that (Act3) is actually false leads to contradiction.
So if one knows, independently of experience (as we all do), that
the world one inhabits is the actual world, then the reasoning embodied
in the preceding tableau is an \emph{a priori} proof of (Act3).%
\footnote{Possibilists may complain that line 2 begs the question against
them
because it assumes that the object denoted by $p_{@}$ is an actual
object. But as I noted in section 6.1, if quantifiers are given a
possibilist interpretation then (Act3) is valid, a result that possibilists
presumably do not want.%
} (Act3) is true \emph{a priori} even though it is not necessary and
not logically true.
\section{Conclusion}
I've shown that an actualistic and seriously actualistic quantified
modal logic with desirable formal and philosophical properties is
possible. These properties include, most notably, uniform substitution
of complex predicate abstracts for simple ones in logical truths,
replacement of logically equivalent subformulas within sentences \emph{salva
veritate}, and a sound and complete proof system. Indeed by defining
SAT and proving that it has these properties I've shown that such
a logic is actual. I've also compared SAT with several other treatments
of the issues with which it deals. I believe it deserves serious
consideration
in ongoing logical and philosophical discussions of modality.
\section{Appendix: Soundness and Completeness}
It is not difficult to verify that the soundness and completeness
results given here for SAT hold also for SAK, SAB, SAS4, and SAS5.
\subsection{Soundness}
The intuitive idea behind the soundness proof is simple. To demonstrate
soundness of the tableau proof system it is sufficient to show that
if a set of\emph{ }prefixed formulas of \emph{$\mathfrak{L^{\bigstar}}$}
appearing on a tableau branch is satisfiable in a certain sense, then
the set obtained by adding prefixed formulas that result from applying
tableau rules to members of that set is satisfiable in this same sense.
Satisfiability of a set of formulas of \emph{$\mathfrak{L}$ }was
defined in section 3.4. The expanded notion of satisfiability of a
set of prefixed formulas of \emph{$\mathfrak{L^{\bigstar}}$}, used
in the soundness proof,\emph{ }is defined as follows.%
\footnote{The definitions and proofs concerning soundness are similar to
those
of Fitting and Mendelsohn \cite{Fitting1998}, pp. 57-60, 121-124,
152-153. %
}
A set \emph{S} of prefixed formulas of \emph{$\mathfrak{L^{\bigstar}}$}
is \emph{satisfiable in a model} $\mathit{\mathrm{\mathcal{M=\langle
W\mathrm{,}\mathrm{@,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
\emph{relative to a valuation} \emph{$\mathcal{V}$} if there is a
function $\mathit{\mathit{\Theta}}$ that assigns to each prefix $\sigma$
occurring in \emph{S} a world $\mathit{\Theta(\sigma)}\in\mathcal{W}$
such that :
\begin{description}
\item [{1.}] For every prefix $\sigma$ in \emph{S}
$\mathit{\Theta(\sigma)}\mathcal{R}\mathit{\Theta(\sigma)}$,
and if $\sigma.n$ also appears a prefix in \emph{S},
$\mathit{\Theta(\sigma)}\mathcal{R}\mathit{\Theta(\sigma.n)}$.
\item [{2.}] If \textbf{@} occurs as a prefix in \emph{S},
$\mathit{\Theta}$(\textbf{@})
= @.
\item [{3.}] If the parameter $\pi_{\sigma}$ occurs in \emph{S}, then
$\mathcal{V}(\pi_{\sigma})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$.
\item [{4.}] Let $\iota$ be an individual constant of \emph{$\mathfrak{L}$,}
and let $\iota_{\sigma}$ be the grounded name of
\emph{$\mathfrak{L^{\bigstar}}$
}that results from subscripting $\iota$ with the tableau prefix $\sigma$.
If $\iota$ and $\iota_{\sigma}$ both appear in \emph{S}, then
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$
is defined,
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$,
and
$\mathcal{V}(\iota_{\sigma})=\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$.%
\footnote{As specified in section 6.1.1, all grounded terms of
\emph{$\mathfrak{L^{\bigstar}}$}
are treated semantically like variables. Given a model
$\mathit{\mathrm{\mathcal{M}}}$
and a valuation \emph{$\mathcal{V}$} relative to
$\mathit{\mathrm{\mathcal{M}}},$
\emph{$\mathcal{V}$} assigns to each grounded term a single, model-wide
denotation from the domain of the model,
$\mathit{\mathrm{\mathcal{D_{M}}}}.$
Clauses 3 and 4 reflect this, since together they require that any
term grounded with $\sigma$ designates, at each world of the model,
a member of $\mathit{\mathcal{D}(\Theta(\sigma))}$. And of course
$\mathcal{D}\mathit{(\Theta(\sigma))\subseteq\mathit{\mathrm{\mathcal{D_{M}}}}}$.
Notice that $\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$
may be defined even if $\iota_{\sigma}$ does not appear in \emph{S}. %
}
\item [{5.}] For any prefix $\sigma$ and formula $\phi,$ if $\sigma\,\,\phi$
is in \emph{S} (that is, if the pair consisting of $\phi$ prefixed
with $\sigma$ is a member of \emph{S}), then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$.
\end{description}
A\emph{ branch of a tableau is satisfiable} if the set of prefixed
formulas appearing on that branch is satisfiable in some model relative
to some valuation. A \emph{tableau is satisfiable} if one or more
of its branches is.
The connection between a set of prefixed formulas appearing on an
open tableau branch and a model-valuation pair ($\mathcal{M}$,
$\mathcal{V}$)
that satisfies them, relative to a function $\mathit{\mathit{\Theta}}$,
is straightforward. Given a branch that is satisfiable in this sense,
$\mathit{\mathit{\Theta}}$ maps tableau prefixes to worlds of $\mathcal{M}$
in a way that induces on the prefixes the roles of relation $\mathcal{R}$
and world @ (clauses 1 and 2). Clauses 3 and 4 require that a term
grounded with a given prefix denotes an object in the domain of the
world associated with that prefix.%
\footnote{For example, clause 3 requires that the parameter $p{}_{1}$
designates,
throughout the model, an object from the domain of world
$\mathit{\Theta}(1)$.
Clause 4 requires that the grounded name $c_{1.1}$ designates, throughout
the model, an object from the domain of world $\mathit{\Theta}(1.1)$.
By contrast, if no occurrence of the individual constant \emph{c}
has a tableau prefix as a subscript, clause 4 does not require that
\emph{c} be given an assignment by $\mathcal{M}$\emph{ cum }$\mathcal{V}$.
Individual constants are not required to denote at every, or even
any, world.%
} Clause 5 requires that each prefixed formula on the branch be satisfied
at the world corresponding to its prefix.
The Soundness Lemma is the heart of the soundness proof. Once it is
established, the Soundness Theorem itself follows easily. Proof of
the Soundness Lemma (and of the Completeness Lemma in the next section)
will be facilitated by the following Substitution Lemma for
\emph{$\mathfrak{L^{\bigstar}}$.}
\begin{description}
\item [{Substitution~Lemma~(for~\emph{$\mathfrak{L^{\bigstar}}$})}]~
\end{description}
Let $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
be a model of \emph{$\mathfrak{L^{\bigstar}}$}, and let \emph{$\mathcal{V}$}
be a valuation relative to $\mathit{\mathrm{\mathcal{M}}}$. Where
$\psi(\alpha)$ is a formula of \emph{$\mathfrak{L^{\bigstar}}$ }containing
at least one free occurrence of the variable $\alpha$ (but no free
occurrence of any other variable), and $w\in\mathcal{W}$:
\emph{Part 1}. Let $\tau_{\sigma}$ be a grounded term of
\emph{$\mathfrak{L^{\bigstar}}$},
$\mathcal{V}(\tau_{\sigma})\in\mathcal{D}(w)$, and $\psi(\tau_{\sigma})$
the result of replacing all free occurrences of $\alpha$ in $\psi(\alpha)$
with $\tau_{\sigma}$. Suppose $\mathcal{U}$ is the $\alpha$-variant-at-$w$
of $\mathcal{V}$ such that $\mathcal{U}(\alpha)=\mathcal{V}(\tau_{\sigma})$.
Then
$\mathcal{\mathcal{M}_{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{w})}=\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau_{\sigma}),}\mathit{w}}})$.
\emph{Part 2}. Let $\iota$ be an individual constant of
\emph{$\mathfrak{L}$},
$\iota_{\sigma}$ be a grounded name of \emph{$\mathfrak{L^{\bigstar}}$}
(that is, $\iota_{\sigma}$ is the grounded name of
\emph{$\mathfrak{L^{\bigstar}}$}
that results from subscripting $\iota$ with the tableau-node prefix
$\sigma$), $\mathcal{V}(\iota_{\sigma})\in\mathcal{D}(w)$, and
$\psi(\iota_{\sigma})$
the result of replacing all free occurrences of $\alpha$ in $\psi(\alpha)$
with $\iota_{\sigma}$. Suppose $\mathcal{U}$ is the $\alpha$-variant-at-$w$
of $\mathcal{V}$ such that
$\mathcal{U}(\alpha)=\mathcal{V}(\iota{}_{\sigma})$.
Then
$\mathcal{\mathcal{M}_{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{w})}=\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\iota_{\sigma}),}\mathit{w}}})$.
Proof of the Part 1 is straightforward by induction on the complexity
of $\psi(\alpha)$. Since a grounded name is a grounded term, Part
2 is a special case of Part 1. It is convenient to have the Lemma
stated in this form in some of the following proofs. $\blacksquare$
\begin{description}
\item [{Soundness~Lemma.}] Tableau Rules Preserve Satisfiability
\end{description}
If a tableau rule is applied to a satisfiable tableau, the result
is another satisfiable tableau.
\medskip{}
Proof: It is sufficient to restrict attention to application of a
tableau rule to a node or nodes that appear in a satisfiable branch
of a tableau, and to show that at least one satisfiable branch results
from application of the rule. So suppose $\mathit{\mathrm{\mathcal{B}}}$
is a branch of a tableau $\mathit{\mathrm{\mathcal{T}}},$ \emph{S}
is the set of prefixed formulas of \emph{$\mathfrak{L^{\bigstar}}$}
that appear on $\mathit{\mathrm{\mathcal{B}}}$, and there is a model
$\mathit{\mathrm{\mathcal{M}}},$ a valuation \emph{$\mathcal{V}$},
and a function $\mathit{\mathit{\Theta}}$ that together satisfy 1-5.
$\mathit{\mathrm{\mathcal{B}}}$ is thus a satisfiable branch of
$\mathit{\mathrm{\mathcal{T}}}$.
We want to show that whenever a rule is applied to a member of
$\mathit{\mathrm{\mathcal{B}}}$,
the result is at least one branch $\mathit{\mathrm{\mathcal{B}}}^{\prime}$
that extends $\mathit{\mathrm{\mathcal{B}}}$ and is such that, for
the set $S^{\prime}$ of prefixed formulas of
\emph{$\mathfrak{L^{\bigstar}}$}
that appear on $\mathit{\mathrm{\mathcal{B}}}^{\prime}$, there is
a model $\mathit{\mathrm{\mathcal{M}}}{}^{\prime}$ a valuation
$\mathcal{V}^{\prime}$,
and a function $\mathit{\mathit{\Theta{}^{\prime}}}$ that together
satisfy 1-5.
Proofs of the cases for truth functional and modal connectives are
simple and straightforward, as in Fitting and Mendelsohn \cite{Fitting1998},
pp. 58-59. The cases for the actuality connective are trivial.
For the universal quantifier case, assume that the prefixed formula
$\sigma$~~$\mathrm{\forall\alpha\psi(\alpha)}$ is in \emph{S},
that clauses 1-5 hold, and hence that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$.
By clause 10 of section 3.4,
$\mathcal{M}_{\mathcal{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$,
for every valuation \emph{$\mathcal{U}$} that is an
$\alpha$-variant-at-$\mathcal{\mathrm{\mathit{\Theta(\sigma)}}}$
of \emph{$\mathcal{V}$}. By 3 and 4,
$\mathcal{V}(\tau_{\sigma})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$,
for each grounded term $\tau_{\sigma}$ that appears on
$\mathit{\mathrm{\mathcal{B}}}$
(i.e., for each parameter or grounded name with subscript $\sigma$
that appears on $\mathit{\mathrm{\mathcal{B}}}$). So part 1 of the
Substitution Lemma yields
$\mathrm{\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau{}_{\sigma})\mathcal{\mathrm{,\mathit{\Theta(\sigma)})=1}}}}$,
for each grounded term $\tau_{\sigma}$ that appears on
$\mathit{\mathrm{\mathcal{B}}}$.
So the branch $\mathit{\mathrm{\mathcal{B}}}^{\prime}$ that results
from one or more applications of the universal quantifier rule to
$\sigma$~~$\mathrm{\forall\alpha\psi(\alpha)}$ is satisfiable
in $\mathit{\mathrm{\mathcal{M}}}$\emph{ }relative to \emph{$\mathcal{V}$}
and $\mathit{\mathit{\Theta}}$.
For the negated universal quantifier case, assume that the prefixed
formula $\sigma$~~$\neg\mathrm{\forall\alpha\psi(\alpha)}$ is
in \emph{S}, that clauses 1-5 hold, and hence that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\neg\forall\alpha\psi(\alpha),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$.
So
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{0}}}}$.
By clause 10 of section 3.4,
$\mathcal{M}_{\mathcal{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{0}}}}$,
for some valuation \emph{$\mathcal{U}$} that is an
$\alpha$-variant-at-$\mathcal{\mathrm{\mathit{\Theta(\sigma)}}}$
of \emph{$\mathcal{V}$}. Since each node on a tableau branch is just
finitely many steps from the origin, for any given node only finitely
many distinct parameters appear in the nodes up to and including it.
So a parameter $\pi_{\sigma}$ that does not appear on
$\mathit{\mathrm{\mathcal{B}}}$
will always be available for application of the negated universal
quantifier rule. Let $\mathit{\mathcal{U}}^{\prime}$ be the
$\pi_{\sigma}$-variant-at-$\mathcal{\mathrm{\mathit{\Theta(\sigma)}}}$
of \emph{$\mathcal{U}$} such that
$\mathit{\mathcal{U}}^{\prime}(\pi_{\sigma})=\mathcal{U}(\alpha)$.
So by part 1 of the Substitution Lemma,
$\mathcal{M}_{\mathit{\mathcal{U}}^{\prime}}\mathrm{(\psi(\pi_{\sigma}),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{0}}}}$.
Hence
$\mathcal{M}_{\mathit{\mathcal{U}}^{\prime}}\mathrm{(\neg\psi(\pi_{\sigma}),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$.
$\mathit{\mathcal{U}}^{\prime}$ satisfies clauses 1, 2, and 4, since
\emph{$\mathcal{V}$} does. And $\mathit{\mathcal{U}}^{\prime}$ satisfies
clause 3 because it makes all the same assignments to parameters other
than $\pi_{\sigma}$ as \emph{$\mathcal{V}$} does, and because
$\mathit{\mathcal{U}}^{\prime}(\pi_{\sigma})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$.
So the branch $\mathit{\mathrm{\mathcal{B}}}^{\prime}$ that results
from application of the negated universal quantifier rule to
$\sigma$~~$\mathrm{\neg\forall\alpha\psi(\alpha)}$,
and thereby adds the node $\sigma$~~$\neg\mathrm{\psi(\pi_{\sigma})}$
to $\mathit{\mathrm{\mathcal{B}}}$, is satisfiable in
$\mathit{\mathrm{\mathcal{M}}}$\emph{
}relative to $\mathit{\mathcal{U}}^{\prime}$ and
$\mathit{\mathit{\Theta}}$.
For the predicate abstraction cases recall that a predicate abstract
$\langle\lambda\alpha.\psi(\alpha)\rangle$ is satisfied by a term
at a world if and only if the term denotes an object in the domain
of that world and the object satisfies $\psi(\alpha)$. Form 1 of
the rule for unnegated predicate abstraction applies to prefixed formulas
of the form $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$,
where $\iota$ is an individual constant. In this case the predicate
abstract is instantiated with the grounded name $\iota_{\sigma}$,
which may or may not already appear somewhere on
$\mathit{\mathrm{\mathcal{B}}}$.
(If $\iota_{\sigma}$ does already appear on $\mathit{\mathrm{\mathcal{B}}}$,
it was introduce either by form 1 of the atomic formula rule or by
a previous application of the very rule under consideration.) So suppose
$\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$ is in
\emph{S}, that clauses 1-5 hold, and hence that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$.
There are two subcases:
(a) If $\iota_{\sigma}$ already appears on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$ is
defined,
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$,
and
$\mathcal{V}(\iota_{\sigma})=\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$
(by clause 4). Since
$\mathcal{M}_{\mathcal{\mathcal{V}}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$,
there is an $\alpha$-variant-at-$\mathit{\mathit{\Theta(\sigma)}}$
of $\mathcal{V}$, \emph{$\mathcal{U}$,} such that
$\mathcal{\mathcal{U}\mathrm{(\alpha}})=(\mathcal{V}\star\mathcal{I})(\iota,\mathit{\mathit{\Theta(\sigma)}})$
and
$\mathcal{M}_{\mathcal{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$
(clause 12a of section 3.4). But since $\iota$ is an individual constant,
$(\mathcal{V}\star\mathcal{I})(\iota,\mathit{\mathit{\Theta(\sigma)}})=\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$,
and so by the identities already established
$\mathcal{\mathcal{U}\mathrm{(\alpha}})=\mathcal{V}(\iota_{\sigma})$.
So by part 2 of the Substitution Lemma
$\mathcal{M}_{\mathcal{\mathcal{V}}}\mathrm{(\psi(\iota_{\sigma}),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$.
(b) If $\iota_{\sigma}$ does not appear on $\mathit{\mathrm{\mathcal{B}}}$
then, since
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}$,
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$ is
nonetheless defined and
$\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})\in\mathit{\mathcal{D}\mathit{(\Theta(\sigma))}}$
(clause 12a of section 3.4). Furthermore
$\mathcal{M}_{\mathcal{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$,
where \emph{$\mathcal{U}$} is the
$\alpha$-variant-at-$\mathit{\mathit{\Theta(\sigma)}}$
of $\mathcal{V}$ such that
$\mathcal{\mathcal{U}\mathrm{(\alpha}})=(\mathcal{V}\star\mathcal{I})(\iota,\mathit{\mathit{\Theta(\sigma)}})=\mathcal{\mathcal{I}\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$
(by clause 12a of section 3.4 and the definition of
$(\mathcal{V}\star\mathcal{I})$
in section 3.3). But there is no guarantee that
$\mathcal{V}(\iota_{\sigma})=\mathcal{I\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$.
So let $\mathcal{V}^{\prime}$ be the
$\iota_{\sigma}$-variant-at-$\mathit{\mathit{\Theta(\sigma)}}$
of $\mathcal{V}$ such that
$\mathcal{V}^{\prime}(\iota_{\sigma})=\mathcal{\mathcal{I}\mathrm{(}}\iota,\mathit{\mathit{\Theta(\sigma)}})$.
Clearly $\mathit{\mathrm{\mathcal{M}}}$, $\mathcal{V}^{\prime}$,
and $\mathit{\mathit{\Theta}}$ satisfy clauses 1-3 of the definition
given at the beginning of the present section, and when the node
$\sigma\,\,\psi(\iota_{\sigma})$
is added to $\mathit{\mathrm{\mathcal{B}}}$ by application of form
1 of the unnegated predicate abstraction rule, clause 4 is also satisfied.
Let \emph{$\mathcal{U}{}^{\prime}$} be the
$\alpha$-variant-at-$\mathit{\mathit{\Theta(\sigma)}}$
of $\mathcal{V}^{\prime}$ such that
$\mathcal{\mathcal{\mathcal{U}{}^{\prime}}\mathrm{(\alpha}})=\mathcal{V}^{\prime}(\iota_{\sigma})$.
So by part 1 of the Substitution Lemma (with $\mathcal{V}^{\prime}$
as $\mathcal{V}$, $\iota_{\sigma}$ as $\tau_{\sigma}$,
$\mathit{\mathit{\Theta(\sigma)}}$
as $w$, and \emph{$\mathcal{U}{}^{\prime}$} as \emph{$\mathcal{U}$})
$\mathcal{\mathcal{M}_{\mathcal{\mathcal{\mathcal{U}{}^{\prime}}}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=\mathcal{M}_{\mathcal{\mathcal{\mathcal{V}^{\prime}}}}\mathrm{(\psi(\iota_{\sigma}),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}}}}})$.
Since
$\mathcal{M}_{\mathcal{\mathcal{U}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$
and \emph{$\mathcal{U}{}^{\prime}$} differs from \emph{$\mathcal{U}$}
only in what it assigns to $\iota_{\sigma}$, which does not appear
in $\psi(\alpha)$,
$\mathcal{\mathcal{M}_{\mathcal{\mathcal{\mathcal{U}{}^{\prime}}}}}\mathrm{(\psi(\alpha),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$.
Hence
$\mathcal{M}_{\mathcal{\mathcal{\mathcal{V}^{\prime}}}}\mathrm{(\psi(\iota_{\sigma}),\mathcal{\mathrm{\mathit{\mathit{\Theta(\sigma)}})}=}1}$.
So the branch $\mathit{\mathrm{\mathcal{B}}}^{\prime}$ that results
from application of form 1 of the rule for unnegated predicate abstraction
to $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$, and
thereby adds $\sigma\,\,\psi(\iota_{\sigma})$ to
$\mathit{\mathrm{\mathcal{B}}}$,
is satisfiable in $\mathit{\mathrm{\mathcal{M}}}$\emph{ }relative
to $\mathcal{V}$ and $\mathit{\mathit{\Theta}}$, or satisfiable
in $\mathit{\mathrm{\mathcal{M}}}$ relative to $\mathcal{V}^{\prime}$
and $\mathit{\mathit{\Theta}}$, depending on whether $\iota_{\sigma}$
already appears on $\mathit{\mathrm{\mathcal{B}}}$.
Having given detailed proofs for the quantifier rules and one of the
predicate abstraction rules, I'll just sketch the proofs for the remaining
cases.
The proof for form 2 of the predicate abstraction rule is similar
to that for form 1, but simpler, since the grounded term $\tau_{\sigma}$
that is instantiated appears in the premise. The proof for form 3
combines features of the proofs for form 2 and the negated quantifier
rule.
The proofs for the first two forms of the negated predicate abstraction
rule are straightforward in view of the explanation given in section
8.2.4, where they are introduced, and the proofs for predicate abstraction.
Form 3 does not require a separate proof since it can be treated as
a derived rule.
The proofs for the two identity rules are straightforward.
Forms 1 and 2 of the atomic formula rule are similar, respectively,
to forms 1 and 3 of the predicate abstraction rule, and their proofs
are similar. The proof for form 3 of the atomic formula rule is trivial.
$\blacksquare$
\begin{description}
\item [{Theorem~6.}] Tableau Soundness for \emph{$\mathfrak{L}$}
\end{description}
If $\phi$ is a sentence of \emph{$\mathfrak{L}$} and $\Gamma$ is
a set of sentences of \emph{$\mathfrak{L}$}, then if $\phi$ is derivable
from $\Gamma$, $\phi$ is a consequence of $\Gamma$. In abbreviated
form, if $\mathrm{\Gamma\vdash\phi}$, then $\mathrm{\Gamma\vDash\phi}$.
Proof: Suppose that $\phi$ is not a consequence of $\Gamma$. Then
$\Gamma\cup\{\neg\phi\}$ is satisfiable. Hence there is a model
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$,
and a world\emph{ }$w\in\mathit{\mathrm{\mathcal{W}}}$, such that
for any valuation \emph{$\mathcal{V}$} relative to
$\mathit{\mathrm{\mathcal{M}}}$
and each sentence $\psi\in\Gamma\cup\{\neg\phi\}$,
$\mathcal{M}_{\mathcal{V}}(\psi,w)=1$.
So for any finite subset $\Gamma^{\prime}$ of $\Gamma$ and each
$\psi\in\Gamma^{\prime}\cup\{\neg\phi\}$,
$\mathcal{M}_{\mathcal{V}}(\psi,w)=1$.
For any such $\Gamma^{\prime}$ consider the set of ordered pairs
\emph{S} =
$\{\langle1,\psi\rangle\mid\psi\in\Gamma^{\prime}\}\cup\{\langle1,\neg\phi\rangle\}$.
\emph{S} is a set of prefixed formulas of \emph{$\mathfrak{L}$} and
hence of\emph{ $\mathfrak{L^{\bigstar}}$. }If we define the function
$\mathit{\mathit{\Theta}}$ so that $\mathit{\mathit{\Theta}}(1)=w$,
clauses 1-5 at the beginning of this section are satisfied. Thus \emph{S}
is a set of prefixed formulas of \emph{$\mathfrak{L^{\bigstar}}$
}that is satisfiable in $\mathit{\mathrm{\mathcal{M}}}$ relative
to \emph{$\mathcal{V}$}. Since \emph{S} is finite, its members constitute
the initial sentences of a tableau. Call this tableau
$S^{\mathit{\mathrm{\mathcal{T}}}}$.
By definition, $S^{\mathit{\mathrm{\mathcal{T}}}}$ is a satisfiable
tableau.
By the Soundness Lemma, any application of a tableau rule to
$S^{\mathit{\mathrm{\mathcal{T}}}}$
results in another satisfiable tableau. This means that in every such
extension of $S^{\mathit{\mathrm{\mathcal{T}}}}$ there is a branch
$\mathit{\mathrm{\mathcal{B}}}$, a model $\mathit{\mathrm{\mathcal{M}}}$,
and a valuation \emph{$\mathcal{V}$} such that, for every node
$\sigma\,\,\phi$
appearing on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\mathit{\Theta(\sigma)})}=\mathrm{\textrm{1}}}}.$\emph{
}But by the definition of satisfaction, no formula and its negation
can both be assigned the value 1. Hence $\mathit{\mathrm{\mathcal{B}}}$
is not closed, and thus $\phi$ is not derivable from $\mathrm{\Gamma}$.
$\blacksquare$
\subsection{Completeness}
Although the details of the completeness proof are complex, the basic
idea behind it is simple. If a tableau has an open branch in which
all the rules that can be applied have been applied, that branch contains
information sufficient to determine an interpretation and a valuation
under which all the formulas of \emph{$\mathfrak{L^{\bigstar}}$}
on the branch are satisfied. The worlds of this interpretation are
the prefixes of nodes appearing on the branch, and the individuals
are the equivalence classes of grounded terms determined by the identity
statements appearing on the branch. The atomic formulas and grounded
names appearing on the branch determine the assignment of extensions
to predicates and individuals to individual constants, respectively.
The valuation assigns to a grounded term the equivalence class of
which that term is a member, and it makes an arbitrary assignment
of these equivalence classes to variables.
As is common in tableau proof systems, some tableaus will contain
infinitely long branches. This is because some rules may have to be
applied repeatedly to the same node (or pair of nodes) of a tableau.
The rules for necessity, universal quantifier, and substitutivity
of identity fall into this category. I'll call a branch \emph{complete}
if all applicable rules have been applied to all its nodes.
Consider a complete and open branch $\mathit{\mathrm{\mathcal{B}}}$
of a tableau $\mathit{\mathrm{\mathcal{T}}},$ and define a \emph{categorical
model} $\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
and a \emph{categorical valuation} \emph{$\mathcal{V}$} (relative
to\emph{ }$\mathit{\mathrm{\mathcal{M}}}$) \emph{induced by
}$\mathit{\mathrm{\mathcal{B}}}$
as follows.
\begin{description}
\item [{$\mathcal{W}$:}] $\mathcal{W}$ is the set of prefixes that appear
on $\mathit{\mathrm{\mathcal{B}}}$
\item [{@:}] @ is \textbf{@}, if \textbf{@} appears as the prefix of a
node on $\mathit{\mathrm{\mathcal{B}}}$; otherwise @ is 1
\item [{$\mathcal{R}$:}] $\mathcal{R}$ =
$\{\langle\sigma,\sigma\rangle\mid\sigma$
appears on
$\mathit{\mathrm{\mathcal{B}}}$\}$\cup$\{$\langle\sigma,\sigma.n\rangle\mid\sigma$
and $\sigma.n$ both appear on $\mathit{\mathrm{\mathcal{B}}}$\}
\end{description}
In order to define $\mathit{\mathrm{\mathcal{D}}},$ the function
that assigns sets of individuals to the worlds in $\mathcal{W},$
some further notation is needed. As before, let $\sigma_{1}$, $\sigma_{2}$,
$\sigma_{3}$, ... be prefixes of nodes that appear on
$\mathit{\mathrm{\mathcal{B}}}$,
and let $\tau_{\sigma_{1}}$, $\tau_{\sigma_{2}}$, $\tau_{\sigma_{3}}$,
... and $\upsilon_{\sigma_{1}}$, $\upsilon_{\sigma_{2}}$,
$\upsilon_{\sigma_{3}}$,
... be grounded terms. Also let $\mathit{\mathrm{\mathcal{G}}}$ be
the set of grounded terms that appear on $\mathit{\mathrm{\mathcal{B}}},$
and $\mathit{\mathrm{\mathcal{E}}}$ the set of formulas of
\emph{$\mathfrak{L^{\bigstar}}$
}of the form $(\tau_{\sigma_{2}}=\upsilon_{\sigma_{3}})$ such that,
for some $\sigma_{1}$,
$\sigma_{1}\,\,(\tau_{\sigma_{2}}=\upsilon_{\sigma_{3}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$. Since
$\mathit{\mathrm{\mathcal{B}}}$
is a complete branch, and in view of the tableau rules for identity
in section 8.2.5, $\mathit{\mathrm{\mathcal{E}}}$ defines an equivalence
relation on $\mathit{\mathrm{\mathcal{G}}}.$ Let
$\mathit{\mathrm{\mathcal{Y}}}$
be the set of equivalence classes (of members of
$\mathit{\mathrm{\mathcal{G}}}$)
determined by $\mathit{\mathrm{\mathcal{E}}}$. If
$\tau\in\mathit{\mathrm{\mathcal{G}}}$,
let $\overline{\tau}$ denote the member of $\mathit{\mathrm{\mathcal{Y}}}$
of which $\tau$ is a member. (Thus for any tableau prefixes $\sigma_{2}$
and $\sigma_{3}$, and grounded terms $\tau_{\sigma_{2}}$ and
$\upsilon_{\sigma_{3}}$,
$\overline{\tau_{\sigma_{2}}}=\overline{\upsilon_{\sigma_{3}}}$ if
and only if there is a prefix $\sigma_{1}$ such that
$\sigma_{1}\,\,(\tau_{\sigma_{2}}=\upsilon_{\sigma_{3}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$. For example, if
$1.2\,\,(a_{1.2.@}=p_{1.1.2})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ , then $\overline{a_{1.2.@}}$=
$\overline{p_{1.1.2}}$. That is, the grounded name $a_{1.2.@}$ and
the parameter $p_{1.1.2}$ denote the same individual, namely the
equivalence class of grounded terms of which both are members.)
\begin{description}
\item [{$\mathit{\mathrm{\mathcal{D}}}$:}]
$\mathcal{D\mathrm{(}}\sigma_{1})$
= \{$y\mid y\in\mathit{\mathrm{\mathcal{Y}}}$ and at least one member
of $y$ is a grounded term with subscript $\sigma_{1}$\}
\end{description}
So the domain of world $\sigma_{1}$ consists of all and only those
members of $\mathit{\mathrm{\mathcal{Y}}}$ that contain at least
one grounded term with subscript $\sigma_{1}$. Since the domain of
a model is the union of the domains of its worlds (section 3.1),
$\mathcal{D_{M}}=\mathit{\mathrm{\mathcal{Y}}}$.
That is, the domain of the model is the set of equivalence classes
of grounded terms defined on $\mathit{\mathrm{\mathcal{G}}}$ by
$\mathit{\mathrm{\mathcal{E}}}.$
Thus for every prefix $\sigma_{1}\in\mathcal{W}$,
$\mathcal{D\mathrm{(}}\sigma_{1})\subseteq\mathcal{D_{M}}$.
The interpretation $\mathit{\mathrm{\mathcal{I}}}$ of model
$\mathit{\mathrm{\mathcal{M}}}$
makes assignments to the individual constants and predicates of
\emph{$\mathfrak{L}$}.%
\footnote{$\mathit{\mathrm{\mathcal{I}}}$ does not, however, assign values
to the grounded terms of \emph{$\mathfrak{L^{\bigstar}}$ }or to the
variables of \emph{$\mathfrak{L}$}. These are given their values
by \emph{$\mathcal{V}$.} %
} Let $\iota$ be an individual constant of \emph{$\mathfrak{L}$,
}$\sigma_{1}$ a prefix of a node that appears on
$\mathit{\mathrm{\mathcal{B}}}$,
and $\iota_{\sigma_{1}}$ the grounded name (and hence grounded term)
that results from subscripting $\iota$ with $\sigma_{1}$.
\begin{description}
\item [{$\mathit{\mathrm{\mathcal{I}}}$:}] If $\iota_{\sigma_{1}}$ appears
as part of a formula on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathit{\mathrm{\mathcal{I}}}(\iota,\sigma_{1})=\overline{\iota_{\sigma_{1}}}$.
Otherwise $\mathit{\mathrm{\mathcal{I}}}(\iota,\sigma_{1})$ is undefined.
\end{description}
Since $\overline{\iota_{\sigma_{1}}}\in\mathcal{D\mathrm{(}}\sigma_{1})$,
$\mathit{\mathrm{\mathcal{I}}}$ satisfies the constraint imposed
by clause 1 of section 3.2, namely, that if an individual constant
of \emph{$\mathfrak{L}$} designates at a world, its designation is
a member of the domain of that world.
Next, let $\theta$ be an \emph{n}-ary predicate (perhaps =), $\sigma_{1}$
a prefix that appears on $\mathit{\mathrm{\mathcal{B}}}$ (perhaps
\textbf{@}), $\tau_{\sigma_{1}}$ a grounded term,
$\overline{\tau_{\sigma_{1}}}$
the equivalence class of grounded terms such that
$\tau_{\sigma_{1}}\in\overline{\tau_{\sigma_{1}}}$,
$\langle...,\overline{\tau_{\sigma_{1}}},...\rangle$ an \emph{n}-tuple
of equivalence classes of grounded terms of which
$\overline{\tau_{\sigma_{1}}}$
is the \emph{$m^{th}$} member, and $\theta(...\tau_{\sigma_{1}}...)$
an atomic formula of \emph{$\mathfrak{L^{\bigstar}}$} in which all
the individual symbols are grounded terms with subscript $\sigma_{1}$
and of which $\tau_{\sigma_{1}}$ is the \emph{$m^{th}$.}
\begin{description}
\item [{$\mathit{\mathrm{\mathcal{I}}}$:}]
$\mathit{\mathrm{\mathcal{I}}}(\theta,\sigma_{1})=$
\{$\langle...,\overline{\tau_{\sigma_{1}}},...\rangle\mid\sigma_{1}\,\,\theta(...\tau_{\sigma_{1}}...)$
is a node on $\mathit{\mathrm{\mathcal{B}}}$\}
\end{description}
If $\theta$ is the identity predicate, this becomes
\begin{description}
\item [{$\mathit{\mathrm{\mathcal{I}}}$:}]
$\mathit{\mathrm{\mathcal{I}}}(=,\sigma_{1})=$
\{$\langle\overline{\tau_{\sigma_{1}}},\overline{\upsilon_{\sigma_{1}}}\rangle\mid\sigma_{1}\,\,(\tau_{\sigma_{1}}=\upsilon_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$\}
\end{description}
In view of the definitions of set $\mathit{\mathrm{\mathcal{Y}}}$
and function $\mathit{\mathrm{\mathcal{D}}}$, for each
$\sigma_{1}\in\mathcal{W}$,
$\mathit{\mathrm{\mathcal{I}}}(\theta,\sigma_{1})$ assigns an \emph{n}-ary
relation on $\mathcal{D\mathrm{(}}\sigma_{1})$ to the predicate $\theta$.
So $\mathit{\mathrm{\mathcal{I}}}$ satisfies the first part of clause
2 of section 3.2, namely, the requirement that the extension of a
predicate at a world contain only objects from the domain of that
world. Furthermore, if $\theta$ is =,
$\mathit{\mathrm{\mathcal{I}}}(=,\sigma_{1})$
is the set of ordered pairs
$\langle\overline{\tau_{\sigma_{1}}},\overline{\tau_{\sigma_{1}}}\rangle$,
where $\overline{\tau_{\sigma_{1}}}$ is an equivalence class of grounded
terms, and
$\overline{\tau_{\sigma_{1}}}\in\mathcal{D\mathrm{(}}\sigma_{1})$.
That is, for each $\sigma_{1}\in\mathcal{W}$,
$\mathit{\mathrm{\mathcal{I}}}(=,\sigma_{1})$
is the identity relation on $\mathcal{D\mathrm{(}}\sigma_{1})$. So
$\mathit{\mathrm{\mathcal{I}}}$ also satisfies the second part of
clause 2 of section 3.2. This completes the definition of a categorical
model $\mathit{\mathrm{\mathcal{M}}}$ induced by a complete and open
branch $\mathit{\mathrm{\mathcal{B}}}$.
Given a such a model $\mathit{\mathrm{\mathcal{M}}}$, the categorical
valuation \emph{$\mathcal{V}$} relative to $\mathit{\mathrm{\mathcal{M}}}$
is easily defined. Recall (section 8.1.1) that grounded terms of
\emph{$\mathfrak{L^{\bigstar}}$}
(i.e., parameters and grounded names) are treated semantically like
variables and thus have their values assigned by \emph{$\mathcal{V}$.}
Where $\mathit{\mathrm{\mathcal{G}}}$, as before, is the set of grounded
terms that appear on $\mathit{\mathrm{\mathcal{B}}}$, and
$\mathit{\mathrm{\mathcal{A}}}$
is the set of variables of \emph{$\mathfrak{L}$,} \emph{$\mathcal{V}$}
is a function from
$\mathit{\mathrm{\mathcal{G}}}\cup\mathit{\mathrm{\mathcal{A}}}$
into $\mathcal{D_{M}}$ such that
\begin{description}
\item [{$\mathit{\mathrm{\mathcal{V}}}$:}] For every grounded term
$\tau_{\sigma_{1}}\in\mathit{\mathrm{\mathcal{G}}}$,
\emph{$\mathcal{V}(\tau_{\sigma_{1}})=$}$\overline{\tau_{\sigma_{1}}}$,
\item [{$\mathit{\mathrm{\mathcal{V}}}$:}] For every variable
\emph{$\alpha\in\mathit{\mathrm{\mathcal{A}}}$},
\emph{$\mathcal{V}(\alpha)$} is some arbitrarily selected member
of $\mathcal{D_{M}}$.
\end{description}
This completes the definition of a categorical valuation
\emph{$\mathcal{V}$}
induced by a complete and open branch $\mathit{\mathrm{\mathcal{B}}}$
(relative to\emph{ }a categorical model$\mathit{\mathrm{\mathcal{M}}}$
induced by this same branch $\mathit{\mathrm{\mathcal{B}}}$).%
\footnote{It is important to bear in mind in what follows that individual
constants
and grounded names are treated very differently in the semantics of
\emph{$\mathfrak{L^{\bigstar}}$}. In the categorical model and valuation
($\mathit{\mathrm{\mathcal{M}}}$ and \emph{$\mathcal{V}$}) just
defined, this difference may manifest itself in initially surprising
ways. For example, if the grounded names \emph{$b_{1}$}, \emph{$b_{1.1}$},
and \emph{$b_{1.1.1}$} appear on a branch, each will have been introduced
by application of a tableau rule to the individual constant \emph{b}.
Yet it may turn out that, under $\mathit{\mathrm{\mathcal{M}}}$ and
\emph{$\mathcal{V}$},
$\overline{b_{1}}\neq\overline{b{}_{1.1}}\neq\overline{b_{1.1.1}}$. %
}
\begin{description}
\item [{Completeness~Lemma.}] A Categorical Model and Valuation Satisfy
all the Formulas on the Branch that Induces them
\end{description}
Let $\mathit{\mathrm{\mathcal{B}}}$ be a complete and open branch
of a tableau $\mathit{\mathrm{\mathcal{T}}},$ and let
$\mathit{\mathrm{\mathcal{M=\langle W\mathrm{,}\mathrm{@
,}R\mathrm{,}D\mathrm{,}I\rangle}}}$\emph{
}be a categorical model\emph{ }and \emph{$\mathcal{V}$} a categorical
valuation (relative to $\mathit{\mathrm{\mathcal{M}}}$) induced by
$\mathit{\mathrm{\mathcal{B}}}$. For any formula $\phi$ of
\emph{$\mathfrak{L^{\bigstar}}$},
and any prefix $\sigma$:
\medskip{}
Part 1. If $\sigma\,\,\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
Part 2. If $\sigma\,\,\neg\phi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
Proof is by induction on the number of connectives and quantifiers
in $\phi$.
\emph{Basis}: Part 1.
\emph{Case a}. Suppose $\phi$ is an atomic formula made up of the
\emph{n}-ary predicate $\theta$ and \emph{n} grounded terms,
$\tau_{\sigma}$,
all of which have $\sigma$ as their grounding subscript. Represent
$\phi$ as $\theta(...\tau_{\sigma}...)$. By hypothesis
$\mathit{\mathrm{\mathcal{B}}}$
is complete. So, by the definition of $\mathit{\mathrm{\mathcal{I}}}$,
the extension of $\theta$ at $\sigma$ contains
$\langle...,\overline{\tau_{\sigma}},...\rangle$
if and only if $\sigma\,\,\theta(...\tau_{\sigma}...)$ is a node
on $\mathit{\mathrm{\mathcal{B}}}$. And by the definition of
$\mathit{\mathrm{\mathcal{V}}}$,
\emph{$\mathcal{V}(\tau_{\sigma})=$}$\overline{\tau_{\sigma}}$.
So if $\sigma\,\,\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
\emph{Case b}. Suppose $\sigma\,\,\phi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
where $\phi$ is an atomic formula made up of the \emph{n}-ary predicate
$\theta$ and \emph{n} terms, and where these terms may include individual
constants of \emph{$\mathfrak{L}$} as well as grounded terms (parameters
and grounded names). Individual constants of \emph{$\mathfrak{L}$}
are ungrounded (and hence have no subscripts), and parameters and
grounded names may be subscripted with tableau prefixes other than
$\sigma$, the prefix of the node $\sigma\,\,\phi$ with which we
are concerned. By hypothesis $\mathit{\mathrm{\mathcal{B}}}$ is complete,
so all possible applications of all rules will have been made to all
nodes on $\mathit{\mathrm{\mathcal{B}}}$. So if the formula $\phi$
of node $\sigma\,\,\phi$ contains individual constants, repeated
application of form 1 of the atomic formula rule will have added a
node $\sigma\,\,\phi*$, where $\phi*$ is like $\phi$ except that
each occurrence of an individual constant $\iota$ has been replaced
by the corresponding grounded name $\iota_{\sigma}$. So $\iota_{\sigma}$
will appear as part of a formula on $\mathit{\mathrm{\mathcal{B}}}$,
and thus by the definition of $\mathit{\mathrm{\mathcal{I}}}$,
$\mathit{\mathrm{\mathcal{I}}}(\iota,\sigma)=\overline{\iota_{\sigma}}$.
Similarly, if $\phi*$ contains (one or more occurrences of) a grounded
term $\tau$ with a subscript other than $\sigma$, application of
form 2 of the atomic formula rule will have added a node of the form
$\sigma\,\,(\pi_{\sigma}=\tau)$, where $\pi_{\sigma}$ is a parameter
that has not previously appeared on $\mathit{\mathrm{\mathcal{B}}}$.
So by the definitions of $\mathit{\mathrm{\mathcal{Y}}}$ and
$\mathit{\mathrm{\mathcal{V}}}$,
$\overline{\pi_{\sigma}}=\overline{\tau}$, and thus
$\mathcal{V}(\tau)=\overline{\pi_{\sigma}}$.
And application of the substitutivity of identity rule will have added
a node $\sigma\,\,\phi*^{\pi_{\sigma}}$, where $\phi*^{\pi_{\sigma}}$
is like $\phi*$ except that $\tau$ has been replaced by $\pi_{\sigma}$
throughout $\phi*$. Since $\mathit{\mathrm{\mathcal{B}}}$ is complete,
this will have happened for each term appearing in $\sigma\,\,\phi*$
that is grounded with a subscript other than $\sigma$, and occurrences
of distinct terms of this kind will have been replaced by distinct
parameters, each of which was new to the branch when it appeared.
Call the resulting formula $\phi**$. So the node $\sigma\,\,\phi**$
will appear on $\mathit{\mathrm{\mathcal{B}}}$. Each term that appears
in $\phi**$ is subscripted with $\sigma$, and so as in \emph{Case
a} above
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi**,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
And since $\mathcal{V}(\pi_{\sigma})=\mathcal{V}(\tau)$, for each
parameter $\pi_{\sigma}$ that was substituted for a grounded term
$\tau$ in the creation of $\phi**$ from $\phi*$, $\phi**$ will
contain, at each of its individual-term positions, a term that denotes
the same member of $\mathcal{D\mathrm{(}}\sigma)$ as is denoted by
the term in the corresponding position in $\phi*$. So
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi*,\mathcal{\mathrm{\sigma)}=\mathcal{M}_{\mathcal{V}}\mathrm{(\phi**,\mathcal{\mathrm{\sigma)}}}}}$,
and hence
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi*,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
Finally, recall that $\phi*$ was defined as differing from $\phi$
only in containing the grounded name $\iota_{\sigma}$ at places where
$\phi$ contains the corresponding individual constant $\iota$. By
the definition of $\mathit{\mathrm{\mathcal{I}}}$, if $\iota$ is
an individual constant of \emph{$\mathfrak{L}$ }and the grounded
name $\iota_{\sigma}$ appears as part of a formula on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathit{\mathrm{\mathcal{I}}}(\iota,\sigma)=\overline{\iota_{\sigma}}$.
Thus since
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi*,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$,
it follows that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
So if $\sigma\,\,\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
\emph{Basis}: Part 2.
\emph{Case a}. As in \emph{Case a} of Part 1, let $\phi$ be an atomic
formula made up of the \emph{n}-ary predicate $\theta$ and \emph{n}
grounded terms $\tau_{\sigma}$, all of which have $\sigma$ as their
grounding subscript. Represent $\phi$ as $\theta(...\tau_{\sigma}...)$.
Suppose $\sigma\,\,\neg\theta(...\tau_{\sigma}...)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$. By hypothesis
$\mathit{\mathrm{\mathcal{B}}}$
is open, so $\sigma\,\,\theta(...\tau_{\sigma}...)$ is a not a node
on $\mathit{\mathrm{\mathcal{B}}}$. Suppose, for \emph{reductio},
that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\theta(...\tau_{\sigma}...),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
Since $\theta(...\tau_{\sigma}...)$ is an atomic formula of
\emph{$\mathfrak{L^{\bigstar}}$},
by clause 2 of section 3.2 each term $\tau_{\sigma}$ in $\phi$ denotes
a member of $\mathcal{D\mathrm{(}}\sigma)$. And by the definition
of $\mathit{\mathrm{\mathcal{I}}}$ of the categorical model given
earlier in this section, a node of the form
$\sigma\,\,\theta(...\tau_{\sigma}...)$
appears on $\mathit{\mathrm{\mathcal{B}}}$. $\mathit{\mathrm{\mathcal{B}}}$
is thus closed, which contradicts the assumption of the Completeness
Lemma. So by \emph{reductio}
$\mathcal{M}_{\mathcal{V}}\mathrm{(\theta(...\tau_{\sigma}...),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\emph{Case b.} Let $\phi$ be as in \emph{Case b} of Part 1. That
is, $\phi$ is an atomic formula made up of the \emph{n}-ary predicate
$\theta$ and \emph{n} terms, where these terms may include individual
constants of \emph{$\mathfrak{L}$} as well as parameters and grounded
names that are subscripted with $\sigma$ or with tableau prefixes
other than $\sigma$. Suppose $\sigma\,\,\neg\phi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$.
By hypothesis $\mathit{\mathrm{\mathcal{B}}}$ is open, so $\sigma\,\,\phi$
is a not a node on $\mathit{\mathrm{\mathcal{B}}}$. Again suppose,
for \emph{reductio}, that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
Since $\phi$ is an atomic formula of \emph{$\mathfrak{L^{\bigstar}}$},
by sections 3.2 and 3.4 each term in $\phi$ denotes a member of
$\mathcal{D\mathrm{(}}\sigma)$,
even though those terms my be unsubscripted or subscripted with prefixes
other than $\sigma$.%
\footnote{Strictly speaking sections 3.2 and 3.4 present only the semantics
of \emph{$\mathfrak{L}$}. \emph{$\mathfrak{L^{\bigstar}}$},\emph{
}introduced in section 8.1.1, is \emph{$\mathfrak{L}$} plus grounded
names and parameters, which are treated like variables. %
} And by the definition of $\mathit{\mathrm{\mathcal{I}}}$ of the
categorical model $\mathit{\mathrm{\mathcal{M}}}$ given earlier in
this section, a node of the form $\sigma\,\,\theta(...\tau_{\sigma}...)$
appears on $\mathit{\mathrm{\mathcal{B}}}$, where each term $\tau_{\sigma}$
in $\theta(...\tau_{\sigma}...)$ is grounded with $\sigma$ and denotes
the same member of $\mathcal{D\mathrm{(}}\sigma)$ as the term at
the corresponding position in $\phi$ (even though the latter terms
my be unsubscripted or subscripted with a prefix other than $\sigma$).
It can then be shown that $\sigma\,\,\phi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
which contradicts the assumption that $\mathit{\mathrm{\mathcal{B}}}$
is open. So by \emph{reductio}
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
The proof that $\sigma\,\,\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$
is straightforward but complex. Rather than giving a fully general
proof, I give an example that should be sufficient to convince the
reader of its truth. Let $\theta$ be the five-place predicate $F$
and let $\phi$ be the atomic formula $Fa_{1}\, b_{1.2}\, p_{1.1}\, b\, c$.
Also let $\sigma$ be the tableau prefix 1.1. Then by our assumptions
$1.1\,\,\neg Fa_{1}\, b_{1.2}\, p_{1.1}\, b\, c$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
and (for \emph{reductio}) $\mathcal{M}_{\mathcal{V}}(Fa_{1}\, b_{1.2}\,
p_{1.1}\, b\, c,\,\,1.1)=1$.
Since the individual constants $b$ and $c$ appear in an atomic formula
that has the value 1 at world 1.1, by the semantics of \emph{$\mathfrak{L}$}
(sections 3.2 and 3.4 above) $\mathit{\mathrm{\mathcal{I}}}(b,1.1)$
and $\mathit{\mathrm{\mathcal{I}}}(c,1.1)$ are defined and each is
a member of $\mathcal{D\mathrm{(}}1.1)$. And since the members of
$\mathcal{D\mathrm{(}}1.1)$ are equivalence classes of grounded terms
that appear on $\mathit{\mathrm{\mathcal{B}}}$, $b_{1.1}$ and $c_{1.1}$
must both appear somewhere on $\mathit{\mathrm{\mathcal{B}}}$, by
the definition of interpretation $\mathit{\mathrm{\mathcal{I}}}$
of the categorical model $\mathit{\mathrm{\mathcal{M}}}$ given earlier
in this section. But then by this same definition,
$\mathit{\mathrm{\mathcal{I}}}(b,1.1)=\overline{b_{1.1}}$
and $\mathit{\mathrm{\mathcal{I}}}(c,1.1)=\overline{c_{1.1}}$. Similarly,
by the definition of the valuation $\mathit{\mathrm{\mathcal{V}}}$
associated with the categorical model $\mathit{\mathrm{\mathcal{M}}}$
defined earlier in this section, $\mathcal{V}(a_{1})=\overline{a_{1}}$,
$\mathcal{V}(b_{1.2})=\overline{b{}_{1.2}}$, and
$\mathcal{V}(p_{1.1})=\overline{p_{1.1}}$.
So by the semantics of \emph{$\mathfrak{L}$} (sections 3.2 and 3.4
above)
\begin{description}
\item [{1.}]
$\mathrm{\langle\overline{a_{1}},\,\overline{b{}_{1.2}},\,\overline{p_{1.1}},\,\overline{b_{1.1}},\,\overline{c_{1.1}}\rangle\in\mathit{\mathrm{\mathcal{I}}}(\mathit{F},\,1.1)}$.
\end{description}
But then there must be grounded terms subscripted with 1.1 that are
members of the equivalence classes $\overline{a_{1}}$ and
$\overline{b_{1.2}}$.
For the semantics of \emph{$\mathfrak{L}$} (sections 3.2 and 3.4
above), states that a predicate is satisfied by an \emph{n}-tuple
of objects at a world, only if each of those objects is a member of
the domain of that world. Suppose these grounded terms are the parameter
$q_{1.1}$ and the grounded name $d_{1.1}$, respectively. $q_{1.1}$
and $d_{1.1}$ will appear on $\mathit{\mathrm{\mathcal{B}}}$ in
nodes of the form $\sigma_{1}\,\, a_{1}=q_{1.1}$ and $\sigma_{2}\,\,
b_{1.2}=d_{1.1}$,
where $\sigma_{1}$ and $\sigma_{2}$ may be any prefixes. Thus
\begin{description}
\item [{2.}] $\overline{a_{1}}=\overline{q_{1.1}}$ and
$\overline{b_{1.2}}=\overline{d_{1.1}}$.
\end{description}
Substituting $\overline{q_{1.1}}$ for $\overline{a_{1}}$ and
$\overline{d_{1.1}}$
for $\overline{b_{1.2}}$ in 1 yields
\begin{description}
\item [{3.}]
$\mathrm{\langle\overline{q_{1.1}},\,\overline{d{}_{1.1}},\,\overline{p_{1.1}},\,\overline{b_{1.1}},\,\overline{c_{1.1}}\rangle\in\mathit{\mathrm{\mathcal{I}}}(\mathit{F},\,1.1)}$.
\end{description}
But then by the definition of $\mathit{\mathrm{\mathcal{I}}}$ of
the categorical model $\mathit{\mathrm{\mathcal{M}}}$ given earlier
in this section
\begin{description}
\item [{4.}] $1.1\,\, Fq_{1.1\,}d_{1.1\,}p_{1.1\,}b_{1.1}\, c_{1.1}$ is
a node on $\mathit{\mathrm{\mathcal{B}}}$.
\end{description}
From 4 and the fact that $\sigma_{1}\,\, a_{1}=q_{1.1}$ and $\sigma_{2}\,\,
b_{1.2}=d_{1.1}$
appear on $\mathit{\mathrm{\mathcal{B}}}$, the tableau rule for
substitutivity
of identity yields
\begin{description}
\item [{5.}] $1.1\,\, Fa_{1}\, b_{1.2}\, p_{1.1}\, b_{1.1}\, c_{1.1}$
is a node on $\mathit{\mathrm{\mathcal{B}}}$.
\end{description}
Finally, by two applications of form 3 of the tableau rule for atomic
formulas,
\begin{description}
\item [{6.}] $1.1\,\, Fa_{1}\, b_{1.2}\, p_{1.1}\, b\, c$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$.
\end{description}
Hence $\mathit{\mathrm{\mathcal{B}}}$ is closed, which contradicts
the assumption that it is open. So by \emph{reductio}
$\mathcal{M}_{\mathcal{V}}(Fa_{1}\, b_{1.2}\, p_{1.1}\, b\, c,\,\,1.1)=0$.
This completes the proof for \emph{Case b} when $\phi$ is $Fa_{1}\,
b_{1.2}\, p_{1.1}\, b\, c$,
$\sigma$ is 1.1, and $\sigma\,\,\neg\phi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$.
It should be clear that an analogous proof can be given for any atomic
formula made up of an \emph{n}-ary predicate and \emph{n} terms, where
these terms may include individual constants as well as parameters
and grounded names that are subscripted with $\sigma$ or with tableau
prefixes other than $\sigma$. Proof of the basis of the induction
is thus complete.
\emph{Inductive Step}: Assume the result holds for formulas with fewer
than \emph{n} logical operators, and show that it holds for formulas
with \emph{n} operators. There is a case for each of the operators.
\begin{description}
\item [{Conjunction}] $\phi$ is $(\psi\wedge\gamma)$. So we must show
\end{description}
\medskip{}
1. If $\sigma\,\,(\psi\wedge\gamma)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{((\psi\wedge\gamma),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg(\psi\wedge\gamma)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{((\psi\wedge\gamma),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
If $\sigma\,\,(\psi\wedge\gamma)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is a complete branch,
$\sigma\,\,\phi$ and $\sigma\,\,\psi$ also appear on
$\mathit{\mathrm{\mathcal{B}}}$.
So by the inductive assumption
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\sigma)}=\mathrm{1}}}}}}$,
and thus
$\mathcal{M}_{\mathcal{V}}\mathrm{((\psi\wedge\gamma),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
So part 1 holds. On the other hand if $\sigma\,\,\neg(\psi\wedge\gamma)$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then again, since
$\mathit{\mathrm{\mathcal{B}}}$
is complete, either $\sigma\,\,\neg\phi$ or $\sigma\,\,\neg\psi$
appears on $\mathit{\mathrm{\mathcal{B}}}$. So again by the inductive
assumption either
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\sigma)}=\mathrm{0}}}$
or
$\mathcal{M}_{\mathcal{V}}\mathrm{(\theta\phi,\mathcal{\mathrm{\sigma)}=\mathrm{0}}}$
and thus
$\mathcal{M}_{\mathcal{V}}\mathrm{((\psi\wedge\gamma),\mathcal{\mathrm{\sigma)}=\mathrm{0}}}$.
So part 2 also holds.
\begin{description}
\item [{Negation}] $\phi$ is $\neg\psi$. So we must show
\end{description}
\medskip{}
1. If $\sigma\,\,\neg\psi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\neg\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg\neg\psi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\neg\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
If $\sigma\,\,\neg\psi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
this case is covered by part 2 of one of the other cases, including
part 2 of the basis case if $\psi$ is atomic. So part 1 holds. On
the other hand if $\sigma\,\,\neg\neg\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is complete, so is
$\sigma\,\,\psi$.
So by the inductive hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$,
and hence
$\mathcal{M}_{\mathcal{V}}\mathrm{(\neg\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\begin{description}
\item [{Actuality}] $\phi$ is $\mathsf{A}\psi$. So we must show
\end{description}
\medskip{}
1. If $\sigma\,\,\mathsf{A}\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\mathsf{A}\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg\mathsf{A}\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\mathsf{A}\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
If $\sigma\,\,\mathsf{A}\psi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is a complete branch,
$@\,\,\psi$ also appears on $\mathit{\mathrm{\mathcal{B}}}$. So
by the inductive assumption
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{@)}=}1}$,
and thus by the semantics of $\mathsf{A}$
$\mathcal{M}_{\mathcal{V}}\mathrm{(\mathsf{A}\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
So part 1 holds. On the other hand if $\sigma\,\,\neg\mathsf{A}\psi$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then again, since
$\mathit{\mathrm{\mathcal{B}}}$
is complete, $@\,\,\neg\psi$ appears on $\mathit{\mathrm{\mathcal{B}}}$.
So by the inductive assumption
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi,\mathcal{\mathrm{@)}=}0}$,
and thus
$\mathcal{M}_{\mathcal{V}}\mathrm{(\mathsf{A}\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
So part 2 also holds.
\begin{description}
\item [{Necessity}] $\phi$ is $\square\psi$. So we must show
\end{description}
\medskip{}
1. If $\sigma\,\,\mathsf{\square}\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\mathsf{\square}\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg\square\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\square\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
For part 1 there are separate cases for SAK, SAT, SAB, SAS4, and SAS5.
1.a (for SAK) If $\sigma\,\,\mathsf{\square}\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is complete, a node of
the form $\sigma.n\,\,\psi$ appears on $\mathit{\mathrm{\mathcal{B}}}$,
for each prefix $\sigma.n$ that is part of a node on
$\mathit{\mathrm{\mathcal{B}}}$.
So by the inductive hypothesis $\mathcal{M}_{\mathcal{V}}(\psi,\sigma.n)=1$,
for each such $\sigma.n$. But since $\sigma\mathcal{R}\sigma.n$
for each such $\sigma.n$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\square\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
1.b (for SAT) If $\sigma\,\,\mathsf{\square}\psi$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is complete, $\sigma\,\,\psi$
appears on $\mathit{\mathrm{\mathcal{B}}}$, as does a node of the
form $\sigma.n\,\,\psi$, for each prefix $\sigma.n$ that is part
of a node on $\mathit{\mathrm{\mathcal{B}}}$. So by the inductive
hypothesis $\mathcal{M}_{\mathcal{V}}(\psi,\sigma)=1$ and
$\mathcal{M}_{\mathcal{V}}(\psi,\sigma.n)=1$,
for each such $\sigma.n$. But since $\sigma\mathcal{R}\sigma$ and
$\sigma\mathcal{R}\sigma.n$, for each such $\sigma.n$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\square\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
1.c-e (for SAB, SAS4, and SAS5) The proofs of these cases are
straightforward
modifications of 1.a and 1.b.
The proof of part 2 is the same for all systems. If
$\sigma\,\,\neg\square\psi$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then, since
$\mathit{\mathrm{\mathcal{B}}}$
is complete, a node of the form $\sigma.n\,\,\neg\psi$ also appears
on $\mathit{\mathrm{\mathcal{B}}}$, where \emph{n} is an integer
and the prefix $\sigma.n$ has not appeared on
$\mathit{\mathrm{\mathcal{B}}}$
prior to $\sigma\,\,\neg\square\psi$. So by the inductive assumption
$\mathcal{M}_{\mathcal{V}}(\psi,\sigma.n)=0$. But since
$\sigma\mathcal{R}\sigma.n$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\square\psi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
The cases for the quantifier and predicate abstraction rules depend
on the Substitution Lemma of section 7.1.
\begin{description}
\item [{Quantification}] $\phi$ is $\forall\alpha\psi$. So we must show
\end{description}
\medskip{}
1. If $\sigma\,\,\forall\alpha\psi(\alpha)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg\forall\alpha\psi(\alpha)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
If $\sigma\,\,\forall\alpha\psi(\alpha)$ is a node on
$\mathit{\mathrm{\mathcal{B}}}$
then, since $\mathit{\mathrm{\mathcal{B}}}$ is a complete branch,
a node of the form $\sigma\,\,\psi(\tau_{\sigma})$ also appears on
$\mathit{\mathrm{\mathcal{B}}}$, for each grounded term $\tau_{\sigma}$
that appears anywhere on $\mathit{\mathrm{\mathcal{B}}}$. So by the
inductive hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau_{\sigma})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$,
for each such $\tau_{\sigma}$. But then by Part 1 of the Substitution
Lemma, for each such $\tau_{\sigma}$, and for the valuation $\mathcal{U}$
that is the $\alpha$-variant-at-$\sigma$ of $\mathcal{V}$ such
that $\mathcal{U}(\alpha)=\mathcal{V}(\tau_{\sigma})$,
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi(\alpha)\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$.
And since the only members of $\mathcal{D\mathrm{(}}\sigma)$ are
the equivalence classes $\overline{\tau_{\sigma}}$ such that $\tau_{\sigma}$
appears on $\mathit{\mathrm{\mathcal{B}}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$
(by clause 10 of section 3.4). On the other hand if
$\sigma\,\,\neg\forall\alpha\psi(\alpha)$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then, since
$\mathit{\mathrm{\mathcal{B}}}$
is complete, a node of the form $\sigma\,\,\neg\psi(\pi_{\sigma})$
also appears on $\mathit{\mathrm{\mathcal{B}}}$, where $\pi_{\sigma}$
is a parameter that has not appeared on $\mathit{\mathrm{\mathcal{B}}}$
up through (and including) the node
$\sigma\,\,\neg\forall\alpha\psi(\alpha)$.
So by the inductive hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\pi_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
Consider the valuation $\mathcal{U}$ that is the
$\alpha$-variant-at-$\sigma$
of $\mathcal{V}$ such that $\mathcal{U}(\alpha)=\mathcal{V}(\pi_{\sigma})$.
Then by Part 1 of the Substitution Lemma,
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi(\alpha)\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{0}}}}$.
So
$\mathcal{M}_{\mathcal{V}}\mathrm{(\forall\alpha\psi(\alpha),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$
(by clause 10 of section 3.4).
\begin{description}
\item [{Predicate~Abstraction}] $\phi$ is
$\langle\lambda\alpha.\psi(\alpha)\rangle$.
So we must show
\end{description}
\medskip{}
Where $\iota$ is an individual constant:
1. If $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ , then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
2. If $\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\iota)$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
Where $\tau_{\sigma}$ is a grounded term:
3. If $\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
4. If
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
Where $\tau_{\sigma_{1}}$ is a grounded term, and $\sigma_{1}\neq\sigma$:
5. If
$\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
6. If
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
The case where $\tau_{\sigma}$ is a grounded term (involving 3 and
4 above) is the simplest. If
$\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then, since
$\mathit{\mathrm{\mathcal{B}}}$
is a complete branch, a node of the form $\sigma\,\,\psi(\tau_{\sigma})$
also appears on $\mathit{\mathrm{\mathcal{B}}}$ (from application
of form 2 of the predicate abstraction rule). So by the inductive
hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau_{\sigma})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$,
and by part 1 of the Substitution Lemma
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi(\alpha)\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$,
where $\mathcal{U}$ is the $\alpha$-variant-at-$\sigma$ of $\mathcal{V}$
such that $\mathcal{U}(\alpha)=\mathcal{V}(\tau_{\sigma})$. But then
by the semantics of predicate abstraction (clause 12a of section 3.4)
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
So 3 is established.
On the other hand if
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$ then, since
$\mathit{\mathrm{\mathcal{B}}}$
is complete, a node of the form $\sigma\,\,\neg\psi(\tau_{\sigma})$
also appears on $\mathit{\mathrm{\mathcal{B}}}$ (from application
of form 2 of the negated predicate abstraction rule). So by the inductive
hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau_{\sigma})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{0}}}}$,
and by part 1 of the Substitution Lemma
$\mathcal{M}_{\mathcal{U}}\mathrm{(\psi(\alpha)\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{0}}}}$,
where $\mathcal{U}$ is the $\alpha$-variant-at-$\sigma$ of $\mathcal{V}$
such that $\mathcal{U}(\alpha)=\mathcal{V}(\tau_{\sigma})$. But then
by the semantics of predicate abstraction (clause 12a of section 3.4)
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
So 4 is established.
Consider next the case where $\iota$ is an individual constant. The
proof of 1 is exactly like that of 3 except that it appeals to form
1 of the predicate abstraction rule and part 2 of the Substitution
Lemma. The proof of 2 divides into two cases depending on whether
or not $\iota_{\sigma}$ appears on $\mathit{\mathrm{\mathcal{B}}}$.
If it does, the proof is like that of 4, except that it uses form
1 of the negated predicate abstraction rule and part 2 of the Substitution
Lemma. If $\iota_{\sigma}$ does not appear on
$\mathit{\mathrm{\mathcal{B}}}$
then in particular $\sigma\,\,\mathsf{(\iota_{\sigma}=\iota_{\sigma}})$
is not a node on $\mathit{\mathrm{\mathcal{B}}}$, and so by definition
of the canonical model $\mathcal{M}$,
$\mathit{\mathrm{\mathcal{I}}}(\iota,\sigma)$
is undefined for all $\sigma\in\mathcal{W}$. So by clause 12b of
section 3.4
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\iota),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
To prove 5, consider the case where
$\sigma\,\,\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, $\tau_{\sigma_{1}}$
is a grounded term, but $\sigma_{1}\neq\sigma$. By form 3 of the
predicate abstraction rule, both $\sigma\,\,\psi(\tau_{\sigma_{1}})$
and $\sigma\,\,(\pi_{\sigma}=\tau_{\sigma_{1}})$ are nodes on
$\mathit{\mathrm{\mathcal{B}}}$.
So by the substitution of identity rule $\sigma\,\,\psi(\pi_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, and thus by the inductive
hypothesis
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\pi_{\sigma})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$.
Since $\sigma\,\,(\pi_{\sigma}=\tau_{\sigma_{1}})$ is on
$\mathit{\mathrm{\mathcal{B}}}$,
it follows from the basis case of the induction that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\pi_{\sigma}=\tau_{\sigma_{1}})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$,
and hence that
$\mathcal{M}_{\mathcal{V}}\mathrm{(\psi(\tau_{\sigma_{1}})\mathcal{\mathrm{,\sigma)}=\mathrm{\textrm{1}}}}$.
But then by part 1 of the Substitution Lemma and clause 12a of section
3.4
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$.
Finally, the proof of 6 is similar to that of 2 in that it divides
into two cases depending on whether there is a grounded term
$\upsilon_{\sigma}$
and a prefix $\sigma_{*}$ such that
$\sigma_{*}(\upsilon_{\sigma}=\tau_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$. If there is,
$\sigma\,\,\neg\langle\lambda\alpha.\psi(\alpha)\rangle(\upsilon_{\sigma})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, by the substitution
of identity rule, since $\mathit{\mathrm{\mathcal{B}}}$ is complete.
Also if $\sigma_{*}(\upsilon_{\sigma}=\tau_{\sigma_{1}})$ is a node
on $\mathit{\mathrm{\mathcal{B}}}$,
$\overline{\upsilon_{\sigma}}=\overline{\tau_{\sigma_{1}}}$,
by the definition of $\mathit{\mathrm{\mathcal{Y}}}$. So by case
4 above
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\upsilon_{\sigma}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
And since $\overline{\upsilon_{\sigma}}=\overline{\tau_{\sigma_{1}}}$,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
On the other hand if there is no grounded term $\upsilon_{\sigma}$
and no prefix $\sigma_{*}$ such that
$\sigma_{*}(\upsilon_{\sigma}=\tau_{\sigma_{1}})$
is a node on $\mathit{\mathrm{\mathcal{B}}}$, then for all grounded
terms $\upsilon_{\sigma}$,
$\overline{\upsilon_{\sigma}}\neq\overline{\tau_{\sigma_{1}}}$,
by the definition of $\mathit{\mathrm{\mathcal{Y}}}$. So by the definition
of $\mathcal{D}$,
$\mathcal{V}(\tau_{\sigma_{1}})\notin\mathcal{D\mathrm{(}}\sigma)$,
and thus by 12b of section 3.4,
$\mathcal{M}_{\mathcal{V}}\mathrm{(\langle\lambda\alpha.\psi(\alpha)\rangle(\tau_{\sigma_{1}}),\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
$\blacksquare$
\medskip{}
Weak completeness follows immediately from the Completeness Lemma.
\begin{description}
\item [{Theorem~7.}] Tableau Completeness for \emph{$\mathfrak{L}$}
\end{description}
Let $\phi$ be a sentence of \emph{$\mathfrak{L}$} and $\Gamma$
a finite set of sentences of \emph{$\mathfrak{L}$}. If $\phi$ is
a consequence of $\Gamma$, then $\phi$ is derivable from $\Gamma$.
In abbreviated form, if $\Gamma$ is finite and $\mathrm{\Gamma\vDash\phi}$,
then $\mathrm{\Gamma\vdash\phi}$.
Proof: Suppose $\phi$ is not derivable from $\Gamma$. Thus by the
definition of derivability (in section 8.1.2) no tableau beginning
with the members of $\Gamma$ and $\neg\phi$, all prefixed with 1,
is closed. Hence every such tableau has a complete and open branch.
Let $\mathit{\mathrm{\mathcal{B}}}$ be a complete and open branch
of such a tableau. By the Completeness Lemma $\mathit{\mathrm{\mathcal{B}}}$
induces a categorical model $\mathit{\mathrm{\mathcal{M=\langle
W\mathrm{,}\mathrm{@,}R\mathrm{,}D\mathrm{,}I\rangle}}}$
and a categorical valuation \emph{$\mathcal{V}$} (relative to
$\mathit{\mathrm{\mathcal{M}}}$
) such that, for any formula $\phi$ of \emph{$\mathfrak{L^{\bigstar}}$}
and any prefix $\sigma$:
\medskip{}
If $\sigma\,\,\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{1}}}}$;
and
If $\sigma\,\,\neg\phi$ is a node on $\mathit{\mathrm{\mathcal{B}}}$,
then
$\mathcal{M}_{\mathcal{V}}\mathrm{(\phi,\mathcal{\mathrm{\sigma)}=\mathrm{\textrm{0}}}}$.
\medskip{}
Since $\neg\phi$ and each member of $\Gamma$ is a sentence of
\emph{$\mathfrak{L}$}
that appears on $\mathit{\mathrm{\mathcal{B}}}$ with the prefix 1,
$\phi$ is not a consequence of $\Gamma$. $\blacksquare$
\begin{quotation}
\bibliographystyle{plain}
\bibliography{\string"//phil-home.ad.umn.edu/phil-home$/whanson/My
Documents/BibTeX/library\string"}
\end{quotation}
\end{document}
*************************************************************************************
Here's the output from TeXWorks's console output window after I run bibtex.
*****************************************************************************************
This is pdfTeX, Version 3.1415926-2.3-1.40.12 (MiKTeX 2.9)
entering extended mode
("\\phil-home.ad.umn.edu\phil-home$\whanson\My Documents\LyX Documents\SAT
for
PL.tex"
LaTeX2e <2011/06/27>
Babel <v3.8m> and hyphenation patterns for english, afrikaans,
ancientgreek, ar
abic, armenian, assamese, basque, bengali, bokmal, bulgarian, catalan,
coptic,
croatian, czech, danish, dutch, esperanto, estonian, farsi, finnish,
french, ga
lician, german, german-x-2009-06-19, greek, gujarati, hindi, hungarian,
iceland
ic, indonesian, interlingua, irish, italian, kannada, kurmanji, lao, latin,
lat
vian, lithuanian, malayalam, marathi, mongolian, mongolianlmc, monogreek,
ngerm
an, ngerman-x-2009-06-19, nynorsk, oriya, panjabi, pinyin, polish,
portuguese,
romanian, russian, sanskrit, serbian, slovak, slovenian, spanish, swedish,
swis
sgerman, tamil, telugu, turkish, turkmen, ukenglish, ukrainian,
uppersorbian, u
senglishmax, welsh, loaded.
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\article.cls"
Document Class: article 2007/10/19 v1.4h Standard LaTeX document class
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\size10.clo"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\fontenc.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\t1enc.def"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\inputenc.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\base\latin9.def"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\geometry\geometry.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\graphics\keyval.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\oberdiek\ifpdf.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\oberdiek\ifvtex.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\ifxetex\ifxetex.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\geometry\geometry.cfg"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\ams\math\amstext.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\ams\math\amsgen.sty"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\amsfonts\amssymb.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\amsfonts\amsfonts.sty"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\frontendlayer\tikz.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\basiclayer\pgf.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\utilities\pgfrcs.sty"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfutil-common.te
x")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfutil-latex.def
" ("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\ms\everyshi.sty"))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfrcs.code.tex")
) ("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\basiclayer\pgfcore.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\graphics\graphicx.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\graphics\graphics.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\graphics\trig.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\00miktex\graphics.cfg")
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pdftex-def\pdftex.def"
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\oberdiek\infwarerr.sty")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\oberdiek\ltxcmds.sty"))))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\systemlayer\pgfsys.sty"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\systemlayer\pgfsys.code.tex
" ("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfkeys.code.te
x"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfkeysfiltered.c
ode.tex"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\systemlayer\pgf.cfg")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\systemlayer\pgfsys-pdftex.d
ef"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\systemlayer\pgfsys-common-p
df.def")))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\systemlayer\pgfsyssoftpath.
code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\systemlayer\pgfsysprotocol.
code.tex")) ("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\xcolor\xcolor.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\00miktex\color.cfg"))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcore.code.tex
" ("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\math\pgfmath.code.tex"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathcalc.code.tex"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathutil.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathparser.code.tex
")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.code.
tex"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.basic
.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.trigo
nometric.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.rando
m.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.compa
rison.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.base.
code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.round
.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfunctions.misc.
code.tex")))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\math\pgfmathfloat.code.tex"
))
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\basiclayer\
pgfcorepoints.co
de.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcorepathconst
ruct.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcorepathusage
.code.tex")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\basiclayer\
pgfcorescopes.co
de.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoregraphicst
ate.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoretransform
ations.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcorequick.cod
e.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoreobjects.c
ode.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcorepathproce
ssing.code.tex")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\basiclayer\
pgfcorearrows.co
de.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoreshade.cod
e.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoreimage.cod
e.tex"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoreexternal.
code.tex"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\pgf\basiclayer\
pgfcorelayers.co
de.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcoretranspare
ncy.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\basiclayer\pgfcorepatterns.
code.tex")))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\modules\pgfmoduleshapes.cod
e.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\modules\pgfmoduleplot.code.
tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\latex\pgf\compatibility\pgfcomp-version
-0-65.sty")
("C:\Program Files (x86)\MiKTeX
2.9\tex\latex\pgf\compatibility\pgfcomp-version
-1-18.sty"))
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\utilities\pgffor.sty"
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\pgf\utilities\pgfkeys.sty"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgfkeys.code.tex"
)) ("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\utilities\pgffor.code.te
x"))
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\frontendlayer\tikz\tikz.cod
e.tex"
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\libraries\pgflibraryplothan
dlers.code.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\modules\pgfmodulematrix.cod
e.tex")
("C:\Program Files (x86)\MiKTeX
2.9\tex\generic\pgf\frontendlayer\tikz\librarie
s\tikzlibrarytopaths.code.tex")))
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\babel\babel.sty"
*************************************
* Local config file bblopts.cfg used
*
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\00miktex\bblopts.cfg")
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\babel\english.ldf"
("C:\Program Files (x86)\MiKTeX 2.9\tex\generic\babel\babel.def")))
("\\phil-home.ad.umn.edu\phil-home$\whanson\My Documents\LyX Documents\SAT
for
PL.aux")
*geometry* driver: auto-detecting
*geometry* detected driver: pdftex
*geometry* verbose mode - [ preamble ] result:
* driver: pdftex
* paper: <default>
* layout: <same size as paper>
* layoutoffset:(h,v)=(0.0pt,0.0pt)
* modes:
* h-part:(L,W,R)=(125.19194pt, 363.91112pt, 125.19194pt)
* v-part:(T,H,B)=(96.73918pt, 601.49162pt, 96.73918pt)
* \paperwidth=614.295pt
* \paperheight=794.96999pt
* \textwidth=363.91112pt
* \textheight=601.49162pt
* \oddsidemargin=52.92195pt
* \evensidemargin=52.92195pt
* \topmargin=-12.5308pt
* \headheight=12.0pt
* \headsep=25.0pt
* \topskip=10.0pt
* \footskip=30.0pt
* \marginparwidth=65.0pt
* \marginparsep=11.0pt
* \columnsep=10.0pt
* \skip\footins=9.0pt plus 4.0pt minus 2.0pt
* \hoffset=0.0pt
* \voffset=0.0pt
* \mag=1000
* \@twocolumnfalse
* \@twosidefalse
* \@mparswitchfalse
* \@reversemarginfalse
* (1in=72.27pt=25.4mm, 1cm=28.453pt)
ABD: EveryShipout initializing macros
("C:\Program Files (x86)\MiKTeX 2.9\tex\context\base\supp-pdf.mkii"
[Loading MPS to PDF converter (version 2006.09.02).]
) ("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\amsfonts\umsa.fd")
("C:\Program Files (x86)\MiKTeX 2.9\tex\latex\amsfonts\umsb.fd")
("\\phil-home.ad.umn.edu\phil-home$\whanson\My Documents\LyX Documents\SAT
for
PL.toc"
! I can't write on file `"SAT for PL.pdf"'.
Please type another file name for output:
When I try to compile with bibtex (per Stefano's instructions) I get no
console output window at all.
The entire file that I get from
Do the same for a compilation with bibtex (just select bibtex from the
Typeset menu and hit ctrl-T). Cut and paste the console output into an
email message and send it to the list.
Post by William HansonFoiled again, I'm afraid. All that's in the bbl file is
\begin{thebibliography}{}
\end{thebibliography}
Cheers nonetheless.
That means that the bibtex run failed. Run bibtex again from within
TeXworks, and cut and paste the console output into an email message to the
list.
It is hard to help without knowing what is wrong.
Cheers,
S.
--
__________________________________________________
Stefano Franchi
http://stefano.cleinias.org