.jpeg)
by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic & Semantics, Entry Directory]
[Nolt, Logics, entry directory]
[The following is summary. All boldface in quotations are in the original unless otherwise noted. Bracketed commentary is my own. As proofreading is incomplete, you will find typos and other districting errors. I apologize in advance.]
Summary of
John Nolt
Logics
Part 5: Nonclassical Logics
Chapter 15: Mildly Nonclassical Logics
15.1 Free Logics
Brief summary:
Leibnizian semantics for modal logic only worked when we dealt strictly with entities that can be said to exist. Were we to deal with a non-existing entity, then we have problems when using the existential quantifier, since it implies the thing’s existence. A solution for this is using a free logic. It is “free” in the sense that it is free from the restriction from only making models with existing entities. One sort of semantics for a free logic is Meinongian semantics. It has both an “inner” domain of existing entities but also another “outer” domain for all existing and as well all non-existing entities. The extensions of all names are found in the outer domain, but only names of existing things have extensions in the inner domain. And the extension of non-quantified predicates is found in the outer domain of existing and non-existing predicates. This allows us to make true statements about the properties and relations of non-existing entities. For example, we might say that it is true that a unicorn has a horn, even though none exist. For, the extension for the predicate “is horned” would be found in the outer domain where unicorns are listed. However, when we use quantifiers, the extensions of the predicates are only found in the inner domain of existing entities. This way, were we to use an existential quantifier for a non-existing entity, the formula would be false. For, the predication would not be fulfilled, as no entity would belong to its proper extension, and this is because, in our example, unicorns are not found in the inner domain of existing entities, which is where we look for quantified expressions. The definition and rules for Meinongian semantics are the following.
DEFINITION A Meinongian valuation or Meinongian model v for a formula or set of formulas of modal predicate logic consists of the following:
1. A nonempty set Wv of objects, called the worlds of v.
2. A nonempty set ℑ of objects, which is called the outer domain of v,
3. For each world w in Wv a nonempty set Dw of ℑ called the inner domain of w,
4. For each name or nonidentity predicate σ of that formula or set of formulas, an extension v(σ) (if σ is a name) or v(σ, w) (if σ is a predicate and w a world in Wv) as follows:
i. If σ is a name, then v(σ) is a member of ℑ.
ii. If σ is a zero-place predicate (sentence letter), v(σ, w) is one (but not both) of the values T or F. |
iii. If σ is a one-place predicate, v(σ, w) is a set of members of ℑ.
iv. If σ is an n-place predicate (n>1), v(σ, w) is a set of ordered n-tuples of members of ℑ.
(Nolt 314-315)
Valuation Rules for Leibnizian-based Meinongian Modal Predicate Free Logic
Given any Leibnizian valuation v, for any world w in Wv:
1. If Φ is a one-place predicate and α is a name, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
2. If Φ is an n-place predicate (n>1) and α1 ... , αn are names, then
v(Φα1, ... , αn, w) = T iff <v(α1), ... , v(αn)> ∈ v(Φ, w);
v(Φα1, ... , αn, w) = F iff <v(α1), ... , v(αn)> ∉ v(Φ, w).
3. If α and β are names, then
v(α = β, w) = T iff v(α) = v (β);
v(α = β, w) = F iff v(α) ≠ v (β).
For the next five rules, Φ and Ψ are any formulas:
4.
v(~Φ, w) = T iff v(Φ, w) ≠ T;
v(~Φ, w) = F iff v(Φ, w) = T.
5 .
v(Φ & Ψ, w) = T iff both v(Φ, w) = T and v(Ψ, w) = T;
v(Φ & Ψ, w) = F iff either v(Φ, w) ≠ T or v(Ψ, w) ≠ T, or both.
6 .
v(Φ ∨ Ψ, w) = T iff either v(Φ, w) = T or v(Ψ, w) = T, or both;v(Φ ∨ Ψ, w) = F iff both v(Φ, w) ≠ T and v(Ψ, w) ≠ T.
7.
v(Φ → Ψ, w) = T iff either v(Φ, w) ≠ T or v(Ψ, w) = T, or both;
v(Φ → Ψ, w) = F iff both v(Φ, w) = T and v(Ψ, w) ≠ T.
8 .
v(Φ ↔ Ψ, w) = T iff either v(Φ, w) = T and v(Ψ, w) = T, or v(Φ, w) ≠ T and v(Ψ, w) ≠ T;
v(Φ ↔ Ψ, w) = F iff either v(Φ, w) = T and v(Ψ, w) ≠ T, or v(Φ, w) ≠ T and v(Ψ, w) = T.
For the next two rules, Φα/β stands for the result of replacing each occurrence of the variable β in Φ by α, and Dw is the domain that v assigns to world w.
9 .
v(∀βΦ, w) = T iff for all potential names α of all objects d in Dw, v(α,d) (Φα/β , w) = T;
v(∀βΦ, w) = F iff for some potential name α of some object d in Dw, v(α,d) (Φα/β , w) ≠ T;
10 .
v(∃βΦ, w) = T iff for some potential name α of some object d in Dw, v(α,d) (Φα/β , w) = T;
v(∃βΦ, w) = F iff for all potential names α of all objects d in Dw, v(α,d) (Φα/β , w) ≠ T; |
11 .
v(□Φ, w) = T iff for all worlds u in Wv, v(Φ, u) = T;
v(□Φ, w) = F iff for some world u in Wv, v(Φ, u) ≠ T;
12 .
v(◊Φ, w) = T iff for some world u in Wv, v(Φ, u) = T;
v(◊Φ, w) = F iff for all worlds u in Wv, v(Φ, u) ≠ T.
(with the beta symbol following quantifiers shown as non-subscript, following the presentation in this section)
‘∃x x = α’, meaning ‘α exists’, can be notated as ‘E!α’.
Summary
Chapter 15: Mildly Nonclassical Logics
Nolt notes that the sorts of logics we have been dealing with so far are all considered types of classical logic, because they have the following features: {1} the logical meaning of the statements in these logics are their truth conditions, {2} the truth values for statements are limited to true and false, and not both and not neither, {3} all names refer to some existing thing. These assumptions are fine when we are using logic for certain applications, but for other applications they are not fitting. In the following chapters Nolt will show ways that these logics fall short, and he will cover a number of alternative logics, nonclassical ones, that provide solutions for these shortcomings. In this chapter in particular Nolt will discuss “some relatively tame departures from classicism” (Nolt 397). In the next chapter we will examine even more radical departures from classical logic. He notes that the division is somewhat arbitrary and also that many logicians do not approve of these departures from classical logic.
All the logics we have examined until now have presupposed that (1) the logical meaning of a statement is its truth conditions, (2) all statements are either true or false but not both, and (3) every name refers to some existing thing. The logics we have developed under these assumptions are called classical logics. But while these assumptions are justifiable for some applications of logic, for others they are not. In this chapter and the next we raise specific challenges to these assumptions. The result, as we shall see, is not anarchy or chaos but an intriguing plurality of nonclassical logics. In this chapter we focus on some relatively tame departures from classicism (hence the chapter title). In the next we shall consider more radical deviations. This division is, however, somewhat arbitrary, and some logicians regard some of the developments even of this chapter as beyond the pale.
(397)
15.1 Free Logics
Nolt observes that in classical predicate logic, we can make a formulation of the existence of some thing without regard to the actual existence of that thing. [The formulations are merely structures which can be used to for philosophical articulations.] But when we are dealing with non-existent entities, we can run into the problem of stating that something exists when it really does not. So there is normally nothing preventing us from writing something like ‘∃x x = α’ where α is any name. This is valid in classical logic. But in ordinary language, we have many names, like ‘Hamlet’ and ‘ the Easter Bunny’ which do not refer to existing entities. However, the statement ‘∃x x = α’ [which might be read something like, there is an x such that x is alpha, or maybe just as, there is an alpha], implies that the thing does exist (397).
Nolt then further explains that the problem is not just with statements about things that are fictional in our world. It also applies to things in other possible worlds where something does not exist, and yet still statements of the form ‘∃x x = α’ would still be valid. Nolt elaborates with an example:
This problem is not confined to fictional names. Even a perfectly respectable name, like ‘Arkansas’, becomes problematic in modal logic, which may entertain the possibility of worlds in which Arkansas does not exist. In such a world, ‘∃x x = a’ is plainly false, reading ‘a’ as ‘Arkansas’; but according to classical predicate logic, ‘∃x x = a’ is a logical truth. Nor is the difficulty confined to alethic modalities. It arises too in tense logic, where we may, for example, consider the actual world at times before Arkansas existed. At such times, once again, ‘∃x x = a’ surely ought to be false.
(Nolt 397)
But suppose that we just use a form with a variable rather than with a name, like ‘∃x x = x’. Here we are merely saying that ‘something self-identical exists’ (397) or that simply ‘something exists’ (398). This is valid in classical logic. For, there is a “stipulation in the classical definition of valuation that domains are non-empty’ (398). Nolt explains that the purpose of this stipulation is so that “names have something to denote” (398). But there is a philosophical problem with this stipulation. [The problem seems to be that we are just assuming something exists, but there is no logical basis for this assumption. Let me quote as I might not have that right.]
But, while true, ‘∃x x = x’ seems not to be a genuine logical truth. “Why is there something, and not rather nothing?” asks the philosopher Martin Heidegger; and the answer, if there is one, surely does not lie in the semantic conventions of classical predicate logic. No merely logical response can placate such questioning. A more modest logic would allow empty domains and would therefore have no such theorems as ‘∃x x = x’.
(Nolt 398)
What we need is a logic that is “capable of handling nondenoting names, names denoting objects that do not exist at a given world, and, perhaps, empty domains” (398). A logic of this sort are called “a free logic, because it is free from the presupposition that a name must denote some existing thing” (398). Nolt then says there are two strategies for developing a free logic, and he will mention both.
In the first strategy, we simply “allow some names to have no denotation at all” (398). He says that this is especially appropriate when we are using fictional names [like ‘Hamlet’ and ‘the Loch Ness Monster’ (397)] or theoretical names that have later been realized to be “based on misconceptions”, with an example of which being ‘the ether’ (398) [and he previously mentioned ‘Phlogiston’ (397)]. Making this adjustment involves us modifying our “valuation rules for atomic sentences containing names, since it is ordinarily presupposed that the names denote something” (398). So suppose we are dealing with classical predicate logic. We normally in this system formulate “the valuation rule for atomic formulas with one-place predicates as follows:”
1. If Φ is a one-place predicate and α is a name, then v(Φα) = T iff v(α) ∈ v(Φ).
(398)
[Let us consider a possible way to think about this rule. Suppose we have the following model. We will suppose we have our world and another possible world where we have fantasy things that exist in it. Let us restrict our worlds to ones with just horses or unicorns and nothing else.
v(h) = horse
v(u) = unicorn
w1 = {h}
w2 = {h, u}
F means “... has four legs”
v(‘F’, w1) = {horse}
v(‘F’, w2) = {horse, unicorn}
v(‘Fh’, w1) = T
v(‘Fh’, w2) = T
v(‘Fu’, w2) = T
but
v(‘Fu’, w1) = F
This last valuation results from the valuation rule, which was “If Φ is a one-place predicate and α is a name, then v(Φα) = T iff v(α) ∈ v(Φ).” So let us fill that in using our example of the the unicorn in world 1: “If ‘F’ is a one-place predicate and ‘u’ is a name, then v(‘Fu’, w1) = T iff v(u) ∈ v(‘F’, w1).” Now, v(u) = unicorn, and v(‘F’, w1) = {horse}. So as we can see, v(u) ∉ v(‘F’, w1), and thus v(‘Fu’, w1) ≠ T. This is an example I selected, and probably it is not good for Nolt’s point. What the model is saying is that in our world, it is false that a unicorn has three legs. Perhaps the idea is that a unicorn still has four legs whether or not it actually exists in reality. I am not sure, but Nolt’s next point is that the fact that v(Φα) does not exist means that we must supplement our rule. The problem might be that I interpreted the “iff” in the formulation to mean that if the extension of the name is not in the extension of the predicate, as with unicorns in world 1, then that means it must not be true. (Here I am using biconditional modus tollens: “From Φ ↔ Ψ and ~Ψ, infer ~Φ. And from Φ ↔ Ψ and ~Φ, infer ~Ψ” (Nolt 102, mentioned in this entry). But perhaps the rule does not tell us what the value would be when the name’s extension is not in the predicates extension on account of the object not being in the domain.)] “But where α has no denotation, v(Φα) does not exist, so this rule must be supplemented by some additional convention” (398).
[Recall that we are still discussing the first strategy for dealing with nonexisting entities, namely that we will allow some names to have no denotation at all.] Nolt then explains that there is more than one way to deal with nondenotiting names. {1} We can say that whenever α does not denote something, v(Φα) would be false. {2} We can specify which predicates belong to non-denoting terms and which others do not; so “although Hamlet does not exist, it is true that he is a character in one of Shakespeare's plays, but false that he is buried in Rome” (398). {3} We can say that Φα is truth-valueless when it does not denote. We will discuss such supervaluational semantics in section 15.3. Nolt will not consider the first two strategies, because they are “problematic in various ways”. [So we will postpone a discussion of this strategy until section 15.3 where we will only address the third option. So we move on to the next strategy.]
For the “second strategy for developing free logics”, we still have all names denoting something, however, the difference here is that we say some of those denoted things are nonexisting (398). The way we would do this is by having two domains. The first one contains all actually existing objects. The second one contains both existing and nonexisting objects. Any of our names can denote any object in “the second and wider domain”. However, “the familiar existential and universal quantifiers range only over the narrower domain of existing things” (398). Nolt says that the name for such a system is Meinongian semantics, and it gets its name from “the philosopher Alexius Meinong, who held that names or definite descriptions that do not denote existing things nevertheless denote objects which, though they do not exist, have ‘being’ ” (399a, boldface mine).
Nolt then says that “Meinongian semantics is especially suited to various forms of modal logic (including tense logics)” (399). Nolt next explains how Meinongian semantics is implemented in alethic modal logic [which is concerned with necessity, possibility, and can be modeled using possible worlds semantics]. [As we noted before, Meinongian semantics involves defining two domains.] The first domain of Meinongian semantics for alethic modality is a world-relative domain that contains all the objects that exist in some particular world. This first domain is called the inner domain. The second domain, called the outer domain, is not world relative, and it contains all those things that can be named. This includes all possible and maybe even all fictional things even if they do not exist in any possible world.
Meinongian semantics is especially suited to various forms of modal logic (including tense logics). In an alethic modal logic, it is usually implemented by defining two domains. The first of these, called the inner domain, is world-relative and represents, as usual, the domain of objects existing in that world. The second, called the outer domain, is, according to the version of Meinongian semantics I shall describe, not world-relative. The outer domain represents the set of all things that can be named, including all things in the inner domains of one's own world as well as merely possible things and perhaps also fictional things – even if these exist in no possible world. It thus contains all the objects that exist in any world of the model and maybe some other objects as well. (In a tense logic, the inner domain of a time is, analogously, the set of things existing at that time; the outer domain contains all things existing at any time in the same time sequence – and perhaps also some things, like fictional objects, that exist outside this sequence.)
(399, boldface mine, except for underlined terms, which are boldface in the original)
Nolt then explains how to evaluate statements like ‘∃x x = α’ in Meinongian semantics. [Recall that the inner domain is the one with all actually existing things and the outer domain is the one with all denotable things regardless of their existence.] We say that the value of ‘∃x x = a’ is true only if the object ‘a’ is found in the inner domain, [that is, if it is an existing thing in some world]. But, suppose that ‘a’ is not in the inner domain but rather is in the outer domain, then it is false.
On a Meinongian semantics, the formula '‘∃x x = a’ is true at a given world w if and only if the object denoted by ‘a’ is in that world’s inner domain. If this object is not in w’s inner domain, but only in the outer domain – that is, if it does not exist at w – then ‘∃x x = a’ is false at w.
(399)
[Recall from before one of the problems with ‘∃x x = x’ in a classical logic. It asserts that something exists, but there is no real basis for this. It could be that nothing exists. The problem was that classical valuation requires sets to be non-empty.] “Moreover, on Meinongian semantics, since names need not denote existing objects, there is no reason not to allow the inner domains of some worlds to be empty, thus falsifying ‘∃x x = x’ at those worlds” (399).
[Recall from section 11.2.1 when we encountered the issue of non-denoting names.
Suppose now that we use the name ‘n’ to denote object β, that is, let v(‘n’) = β. (Note the absence of a world-variable here; the denotation of a rigidly designat- | ing name, unlike truth or the denotation of a predicate, is not world-relative.) Then we would say that the statement ‘Bn’ (“n is blue”) is true in w1, but not in w2, that is, v(‘Bn’, w1) = T, but v(Bn’, w2) = F.
But what are we to say about the truth value of ‘Bn’ in w3, wherein β does not exist? Consider some possible (but nonactual) stone. Is it blue or not blue in the actual world? Both answers are arbitrary. Similarly, it seems arbitrary to make ‘Bn’ either true or false in a world in which ‘n’ has no referent.
(Nolt 311-314)
And recall also how we defined the evaluation of one-place predicates:
Valuation Rules for Leibnizian Modal Predicate Logic
Given any Leibnizian valuation v, for any world w in Wv:
1. If Φ is a one-place predicate and α is a name whose extension v(α) is in Dw, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
(Nolt 315)
So this is the basic structure we saw before, where when the name’s extension is found in the predicate’s extension for some world, then it is true, and it is false otherwise. Nolt now notes that (with our current considerations with Meinongian semantics) the name’s extension may not be a member of Dw. (Recall that Dw includes only the domain of world w and is not all the domains of all worlds.) But, the predicate’s extension in classical modal logic can only be found in Dw. And, we stated in the rule that “α is a name whose extension v(α) is in Dw.” So we cannot evaluate the predicate when the name denotes a nonexisting thing, if we just have this rule.]
Further, Meinongian semantics provides a way of completing the truth conditions for atomic formulas of modal predicate logic, which we left incomplete in Section 11.2. For example, where Dw is the (classical) domain of world w, we there defined the truth conditions for an atomic formula of the form Φα as follows:
If Φ is a one-place predicate and α is a name whose extension v(α) is in Dw, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
The problem is that while the extension of a name need not be a member of Dw, the extensions of predicates are in classical modal logic confined to Dw. Given this restriction, we intentionally formulated the truth conditions to say nothing about the truth value of Φα if v(α) ∉ Dw (i.e., if α denotes an object that does not exist in w), for it would have been arbitrary to stipulate truth conditions where we had assigned no extensions to justify them. Thus, for example, if ‘α’ names Arkansas, ‘S’ is a predicate meaning “is a state,” and w is a world in which Arkansas does not exist, these truth conditions say nothing about the truth value of ‘Sa’ at w. There simply is no structure within classical modal semantics on which to base such a truth value.
(399)
We can solve this problem using Meinongian semantics. We make Dw be the inner domain of world w. And we also construct a second domain, an outer one, and we give it the name ℑ. [I do not follow the next point very well. He writes: “So, for example, for a | one-place predicate Φ, v(Φ, w) is now a subset of ℑ rather than of Dw.” I suppose this is saying that we have all the existing objects in Dw and all the existing and non-existing ones in ℑ. The sets belonging to each predicate will be found as subsets in ℑ. I am just a little confused, because I would think that subsets for predicates taking existing terms would be found also in Dw. But perhaps the idea is that we consider ℑ to be the set we assign to all predicates just so that there is always an extension regardless of which terms are used. I am just guessing.] And not only is the extension of a predicate found in ℑ but also the extension of each name is found in ℑ. However, a name’s extension is not world relative. When we construct models in Meinongian semantics, we need to specify not just the existing objects for which a predicate is true but also which nonexisting ones for which a predicate is true.]
Meinongian semantics provides the needed structure. In a Meinongian semantics, Dw becomes the inner domain of world w and there is in addition an outer domain, which we shall call ℑ. The extensions of predicates, instead of being confined to Dw, are now defined for the outer domain ℑ. So, for example, for a | one-place predicate Φ, v(Φ, w) is now a subset of ℑ rather than of Dw. Similarly, each name denotes an object in ℑ, though the extension of a name – in contrast to that of a predicate – is always rigid, that is, not world-relative. On Meinongian semantics it becomes part of the task of constructing a model to stipulate for each predicate and each world not only which existing objects that predicate is true of in that world, but also which nonexisting objects it is true of in that world. We define extensions of predicates at worlds not simply for all the actual objects in those worlds, but for all nameable objects.
(399-400)
Whether or not we say that it predication is true for some object in some world “seems largely a matter of convention or stipulation” (400). However, after we have made that determination, we can model that status using Meinongian semantics. The Leibnizan semantics from section 11.2 does not allow this, however (400).
[The next idea seems to be the following, but please consult the quotation to follow as I might have this wrong. So Dw contains the set of all existing objects, and ℑ is the set of all existing and non-existing objects. We said also that the extensions of names and predicates are found in ℑ. Perhaps we might say that all expressions that we formulate have some meaning or interpretation. They are not necessarily non-sensical because there is no reference to the terms and predications. However, we have the problem of existential quantification implying the existence of the terms being quantified. The next point seems to be that although the extensions are in the set ℑ of all existing and non-existing entities, the domain over which quantifiers range is restricted to the domain Dw of existing entities. So let me try to work through this idea with an example. Suppose we claim simply that Pegasus is a unicorn. Now, we will symbolize this. Let us say that p = Pegasus and U = is a unicorn. In our set ℑ are many things. Among them are Pegasus and other unicorns. So the extension of ‘p’ is Pegasus, which is in ℑ but it is not in Dw. The extension of U is a set of singles, all of which are unicorns. So it will be something like {<Pegasus>, <[some other unicorn]>, <[etc.]>}. This means that ‘Up’, meaning ‘Pegasus is a unicorn’, is true, because the extension of ‘p’ is found as a member of the extension of ‘U’. But, as we said, quantification only ranges over the domain Dw. So if we have ∃xUx, then it is not enough that Pegasus is in ℑ. We need to see of the extension of U (as determined by means of ℑ) has any members that are also in Dw. But none of the members of U’s extension are found in Dw, because all its members are non-existing entities. Therefore, ∃xUx is false. Let me quote.]
While the extensions of predicates and names are chosen from the outer domain ℑ, we retain the standard quantifier rules, according to which quantifiers range only over the inner domain Dw. Thus, if we decide to make ‘Sa’ (“Arkansas is a state”) true in some world w where neither Arkansas nor any other state exists (i.e., no member of v(‘S’, w) is in Dw), then even though ‘Sa’ is true in w, ‘∃xSx’ is false there. So one way in which Meinongian semantics differs from classical semantics is that it makes the rule ∃I invalid.
(Nolt 400)
[For that last point, recall how Agler in his Symbolic Logic section 8.1.2 defined Existential Introduction:
| Existential Introduction (∃Ι) From any possible substitution instance ‘P(a/x),’ an existentially quantified proposition ‘(∃x)P’ can be derived by consistently replacing at least one individual constant (name) with an existentially quantified variable. | P(a/x) (∃x)P | ∃I |
(Agler 329)
And recall the first simple proof he gave to illustrate it:
Zr ⊢ (∃x)Zx
| 1 | Zr | P |
| 2 | (∃x)Zx | 1∃I |
So here we can see that we begin with an expression with a constant in it. Then, on the basis of the reasoning that if we have such an expression for some term, then we can say that at least one such thing taking that predicate exists. Nolt’s point about this rule being invalid in Meinongian semantics seems to be that just because we have valid formulations that predicate terms, that does not mean they exist, that is to say, the extension for the quantified version of that predicate may not be found in the domain of existing entities. And thus we cannot use this existential introduction rule, because we cannot assume that the extension for some predicate lies in the domain over which the quantifiers range.]
Nolt then says that there is “nothing essential to the understanding of free logic hinges on whether we take a Kripkean or Leibnizian approach to modality” (400) [I am not sure why, but perhaps the idea is that regardless of whether we use a Kripkean or Leibnizian semantics, little of any importance would emerge.] For this reason, Nolt will take a Leibnizian approach because by leaving out the accessibility relation, we will have a simpler set-up. Nolt then characterizes the valuation rules for a Meinongian free logic using Leibnizian semantics in the following way.
DEFINITION A Meinongian valuation or Meinongian model v for a formula or set of formulas of modal predicate logic consists of the following:
1. A nonempty set Wv of objects, called the worlds of v.
2. A nonempty set ℑ of objects, which is called the outer domain of v,
3. For each world w in Wv a nonempty set Dw of ℑ called the inner domain of w,
4. For each name or nonidentity predicate σ of that formula or set of formulas, an extension v(σ) (if σ is a name) or v(σ, w) (if σ is a predicate and w a world in Wv) as follows:
i. If σ is a name, then v(σ) is a member of ℑ.
ii. If σ is a zero-place predicate (sentence letter), v(σ, w) is one (but not both) of the values T or F. |
iii. If σ is a one-place predicate, v(σ, w) is a set of members of ℑ.
iv. If σ is an n-place predicate (n>1), v(σ, w) is a set of ordered n-tuples of members of ℑ.
(Nolt 314-315)
Nolt then will provide the valuation rules for atomic formulas containing n-place predicates where n is greater than zero. [Recall from section 11.2.1 when we were examining the rules for evaluation in Leibnizian semantics that we specified that the extensions must be in Dw. One such rule was:
1. If Φ is a one-place predicate and α is a name whose extension v(α) is in Dw, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
(Nolt 315)
Nolt’s point now is that we can drop that specification for the domain. The idea seems to be that since the extension can be outside Dw in ℑ, that we do not need to specify which domain. But I am not sure why it is not necessary to specify ℑ.]
We may now complete the valuation rules for atomic formulas containing n-place predicates, n>0. These rules need no longer be restricted to the case in which the extensions of the relevant names are in Dw . Instead, they now read simply:
1. If Φ is a one-place predicate and α is a name, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
2. If Φ is an n-place predicate (n>1) and α1 ... , αn are names, then
v(Φα1, ... , αn, w) = T iff <v(α1), ... , v(αn)> ∈ v(Φ, w);
v(Φα1, ... , αn, w) = F iff <v(α1), ... , v(αn)> ∉ v(Φ, w).
(Nolt 401)
Nolt says that
the other valuation rules may be stated precisely as in Section 11.2. Specifically, we have for the existential quantifier:
v(∃βΦ, w) = T iff for some potential name α of all objects d in Dw, v(α,d) (Φα/β , w) = T;
v(∃βΦ, w) = F iff for all potential names α of all objects d in Dw, v(α,d) (Φα/β , w) ≠ T;
(Nolt 401 [note that in section 11.2.1 the ∃β has the beta symbol more as a subscript, but I do not know why. See p.315.])
[So as we can see, unlike with the valuations for non-quantified propositions, we see in this case that the extension must be in Dw. I am not sure if we can do this, but possibly what Nolt is saying is that all the rules are identical except for the two prior to these. So let us write them all out to make the list complete, in case they all still hold.
Valuation Rules for Leibnizian-based Meinongian Modal Predicate Free Logic
Given any Leibnizian valuation v, for any world w in Wv:
1. If Φ is a one-place predicate and α is a name, then
v(Φα, w) = T iff v(α) ∈ v(Φ, w);
v(Φα, w) = F iff v(α) ∉ v(Φ, w).
2. If Φ is an n-place predicate (n>1) and α1 ... , αn are names, then
v(Φα1, ... , αn, w) = T iff <v(α1), ... , v(αn)> ∈ v(Φ, w);
v(Φα1, ... , αn, w) = F iff <v(α1), ... , v(αn)> ∉ v(Φ, w).
3. If α and β are names, then
v(α = β, w) = T iff v(α) = v (β);
v(α = β, w) = F iff v(α) ≠ v (β).
For the next five rules, Φ and Ψ are any formulas:
4.
v(~Φ, w) = T iff v(Φ, w) ≠ T;
v(~Φ, w) = F iff v(Φ, w) = T.
5 .
v(Φ & Ψ, w) = T iff both v(Φ, w) = T and v(Ψ, w) = T;
v(Φ & Ψ, w) = F iff either v(Φ, w) ≠ T or v(Ψ, w) ≠ T, or both.
6 .
v(Φ ∨ Ψ, w) = T iff either v(Φ, w) = T or v(Ψ, w) = T, or both;v(Φ ∨ Ψ, w) = F iff both v(Φ, w) ≠ T and v(Ψ, w) ≠ T.
7.
v(Φ → Ψ, w) = T iff either v(Φ, w) ≠ T or v(Ψ, w) = T, or both;
v(Φ → Ψ, w) = F iff both v(Φ, w) = T and v(Ψ, w) ≠ T.
8 .
v(Φ ↔ Ψ, w) = T iff either v(Φ, w) = T and v(Ψ, w) = T, or v(Φ, w) ≠ T and v(Ψ, w) ≠ T;
v(Φ ↔ Ψ, w) = F iff either v(Φ, w) = T and v(Ψ, w) ≠ T, or v(Φ, w) ≠ T and v(Ψ, w) = T.
For the next two rules, Φα/β stands for the result of replacing each occurrence of the variable β in Φ by α, and Dw is the domain that v assigns to world w.
9 .
v(∀βΦ, w) = T iff for all potential names α of all objects d in Dw, v(α,d) (Φα/β , w) = T;
v(∀βΦ, w) = F iff for some potential name α of some object d in Dw, v(α,d) (Φα/β , w) ≠ T;
10 .
v(∃βΦ, w) = T iff for some potential name α of some object d in Dw, v(α,d) (Φα/β , w) = T;
v(∃βΦ, w) = F iff for all potential names α of all objects d in Dw, v(α,d) (Φα/β , w) ≠ T; |
11 .
v(□Φ, w) = T iff for all worlds u in Wv, v(Φ, u) = T;
v(□Φ, w) = F iff for some world u in Wv, v(Φ, u) ≠ T;
12 .
v(◊Φ, w) = T iff for some world u in Wv, v(Φ, u) = T;
v(◊Φ, w) = F iff for all worlds u in Wv, v(Φ, u) ≠ T.
(with the beta symbol following quantifiers shown as non-subscript, following the presentation in this section)
]
As we noted already, this Meinongian valuation system affects our inference rules, since as we saw it invalidates ∃I. For, “there might be a world (or time) in which it is true that Arkansas is a nonexisting state” (401). Nolt then proves the invalidity of ∃I by making a model where neither Arkansas nor anything else exists.
METATHEOREM: The sequent ‘Sa ⊢ ∃xSx’ is invalid on Meinongian semantics.
PROOF: [See page 401 for details. He builds a model where the outer domain ℑ contains the number 1, but the inner domain of Dw is empty. The name for the number 1 is ‘a’, and there is a predicate ‘S’ whose valuation is the set including just the number 1. Thus the value of ‘Sa’ is true, because the extension of ‘a’ is found in the extension of ‘S’. But since the Dw domain is empty, then there is no assignment that can make ∃xSx true, and thus it is false. This means that in the sequent ‘Sa ⊢ ∃xSx’ the premise is true but the conclusion is false. It therefore is a counterexample to existential introduction.]
(Nolt 401, with my summary in brackets)
So as we can see, the inner domain Dw can be empty, which means in Meinongian semantics, it could be that nothing exists. Thus ‘∃x x = x’ is no longer valid. And Nolt proves this.
METATHEOREM: The formula ‘∃x x = x’ is not valid on Meinongian semantics.
PROOF: [See p.402 for details. Nolt makes a model similar to the one before, where the inner domain Dw is empty, and therefore the value of ‘∃x x = x’ is false. Thus there is a counterexample.]
(402, with my summary in brackets)
Nolt next notes that formulas taking the form ∃x x = α are true in a world only if the extension of α is in the inner domain. And as we know, when it is in the inner domain, that means it is an existing object. Therefore ‘∃x x = α’ can be interpreted as meaning ‘α exists’ (Nolt 402). Nolt then explains that there is a notation convention for this formulation. We can write ‘E!α’ to mean ‘α exists’ (402). Nolt then shows that a restricted version of existential introduction is still valid in Meinongian semantics, and we will use this new notation. [In this proof, we seem to have an argument with two premises. The first premise for some reason involves a substitution, but I do not know why. The basic idea seems to be something like the following. We have a predicate. It has a variable with certain substitutions that would make the formula true. Our first premise will provide one such proper substitution for the variable in the predicate. Our second premise then says that this substituted term exists. I am not sure, but I am supposing that we are thereby saying that it exists in the inner domain. That means we can say that at least one such thing belonging to the predicate exists, because we have already established that in the second premise. So this is similar to existential instantiation, with the difference perhaps being that we must establish the existence of the term that will then be notated with a variable along with the existential quantifier.]
METATHEOREM: Any sequent of the form Φα/β, E!α ⊢ ∃βΦ, where Φα/β is the result of replacing each occurrence of the variable β in Φ by the name α, is valid on Meinongian semantics.
PROOF: [See p.402 for the details. Nolt performs a reductio proof and concludes:]
Therefore all sequents of the formΦα/β, E!α ⊢ ∃βΦ are valid.
So, for example, we might reason concerning a particular rabbit named Allison:
Allison is a rabbit.
Allison exists.
∴ Some rabbit exists. |
In symbols:
Ra, E!a ⊢ ∃xRx
(Nolt 402-403)
So Nolt has provided a Meinongian semantics for quantified Leibnizian modal logic. But we still need inference rules in this system of free logic for quantified expressions. The rules that Nolt will give will apply to all sorts of free logics, and not just to modalized free logics [so I suppose this means these inference rules can apply to a quantified predicate logic that does not provide for modal operators.] For each quantifier there will be a modified introduction and elimination rule. [The modifications will be such that they establish the existence of terms in the inner domain, as we saw before.]
| Free Logic Quantification Inference Rules |
| Free Existential Introduction (F∃I) Let Φ be any formula containing some name α and Φβ/α be the result of replacing at least one occurrence of α in Φ by some variable β not already in Φ. Then from Φ and ∃x x = α infer ∃βΦβ/α. |
| Free Existential Elimination (F∃E) Let ∃βΦ be any existential formula, Ψ any formula, and α any name that occurs neither in Φ nor in Ψ. And let Φα/β be the result of replacing all occurrences of the variable β in Φ by α. Then, given a derivation of Ψ from the hypothesis Φα/β & ∃x x = α, end the hypothetical derivation and from ∃βΦ infer Ψ, provided that α does not occur in any other hypothesis whose hypothetical derivation has not ended or in any assumption. |
| Free Universal Introduction (F∀I) Let Φ be a formula containing a name α, and let Φβ/α be the result of replacing all occurrences of α in Φ by some variable β not already in Φ. Then given a derivation of Φ from the hypothesis ∃x x = α, end the hypothetical derivation and infer ∀βΦβ/α, provided that α does not occur in any other hypothesis whose hypothetical derivation has not yet ended or in any assumption. |
| Free Universal Elimination (F∀E) Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ for some name α. Then from ∀βΦ and ∃x x = α infer Φα/β. |
(Nolt 403)
Nolt says that by adding these four rules to the ones we listed in section 11.4, “we obtain a logic that is sound and complete with respect to the Meinongian semantics outlined here” (403).
[For reference, let us list all the rules the other rules (the rules are compiled at this post):
| ~E | Negation Elimination (Double Negation) | From ~~Φ, infer Φ. |
| ~I | Negation Introduction (Reductio ad Absurdum, Indirect Proof | Given a hypothetical derivation of any formula of the form (Ψ & ~Ψ) from Φ, end the derivation and infer ~Φ. |
| &E | Conjunction Elimination (Simplification) | From (Φ & Ψ), infer either Φ or Ψ. |
| &I | Conjunction Introduction (Conjunction) | From Φ and Ψ, infer (Φ & Ψ). |
| ∨E | Disjunction Elimination (Constructive Dilemma) | From (Φ ∨ Ψ), (Φ→ Θ), and (Ψ→ Θ), infer Θ. |
| ∨I | Disjunction Introduction (Addition) | From Φ, infer either (Φ ∨ Ψ) or (Ψ ∨ Φ). |
| ~E | Conditional Elimination (Modus Ponens) | Given (Φ→ Ψ) and Φ, infer Ψ. |
| →I | Conditional Introduction (Conditional Proof) | Given a hypothetical derivation of Ψ from Φ, end the derivation and infer (Φ→ Ψ). |
| ↔E | Biconditional Elimination | From (Φ ↔ Ψ), infer either (Φ→Ψ) or (Ψ→Φ). |
| ↔I | Biconditional Introduction | From (Φ→ Ψ ) and (Ψ→Φ), infer (Φ ↔ Ψ). |
(Nolt 102)
| MT | Modus Tollens | From Φ → Ψ and ~Ψ, infer ~Φ. |
| CP | Contraposition | From Φ → Ψ, infer ~Ψ → ~Φ. |
| ↔MP | Biconditional Modus Ponens | From Φ ↔ Ψ and Φ, infer Ψ. And from Φ ↔ Ψ and Ψ, infer Φ. |
| ↔MT | Biconditional Modus Tollens | From Φ ↔ Ψ and ~Ψ, infer ~Φ. And from Φ ↔ Ψ and ~Φ, infer ~Ψ. |
| DS | Disjunctive Syllogism | From Φ ∨ Ψ and ~Φ, infer Ψ. And from Φ ∨ Ψ and ~Ψ, infer Φ. |
| HS | Hypothetical Syllogism | From Φ → Ψ and Ψ → Θ, infer Φ → Θ. |
| DN | Double Negation | From Φ, infer ~~Φ. |
| DM | DeMorgan’s Law’s | From ~(Φ ∨ Ψ), infer ~Φ & ~Ψ.From ~Φ & ~Ψ, infer ~(Φ ∨ Ψ). From ~(Φ & Ψ), infer ~Φ ∨ ~Ψ. From ~Φ ∨ ~Ψ, infer ~(Φ & Ψ). From Φ ∨ Ψ, infer ~(~Φ & ~Ψ). From ~(~Φ & ~Ψ), infer Φ ∨ Ψ. From Φ & Ψ, infer ~(~Φ ∨ ~Ψ). From ~(~Φ ∨ ~Ψ), infer Φ & Ψ. |
| COM | Commutation | From Φ & Ψ, infer Ψ & Φ. From Φ ∨ Ψ, infer Ψ ∨ Φ. |
| ASSOC | Association | From (Φ & Ψ) & Θ, infer Φ & (Ψ & Θ). From Φ & (Ψ & Θ), infer (Φ & Ψ) & Θ. From (Φ ∨ Ψ) ∨ Θ, infer Φ ∨ (Ψ ∨ Θ). From Φ ∨ (Ψ ∨ Θ), infer (Φ ∨ Ψ) ∨ Θ. |
| DIST | Distribution | From (Φ & Ψ) ∨ Θ, infer (Φ ∨ Θ) & (Ψ ∨ Θ). From (Φ ∨ Θ) & (Ψ ∨ Θ), infer (Φ & Ψ) ∨ Θ. From (Φ ∨ Ψ) & Θ, infer (Φ & Θ) ∨ (Ψ & Θ). From (Φ & Θ) ∨ (Ψ & Θ), infer (Φ ∨ Ψ) & Θ. |
| MI | Material Implication | From Φ → Ψ, infer ~Φ ∨ Ψ. From ~Φ ∨ Ψ, infer Φ → Ψ. From Φ → Ψ, infer ~(Φ & ~Ψ). From ~(Φ & ~Ψ), infer Φ → Ψ. |
| EFQ | Ex Falso Quodlibet | From Φ and ~Φ, infer any formula Ψ. |
(Nolt 102)
| DUAL | Duality | From either ◊Φ and ~□~Φ, infer the other; from either □Φ and ~◊~Φ, infer the other. |
| K | K rule | From □(Φ → Ψ), infer (□Φ → □Ψ). |
| T | T rule | From □Φ, infer Φ. |
| S4 | S4 rule | From □Φ, infer □□Φ |
| B | Brouwer rule | From Φ, infer □◊Φ. |
| N | Necessitation | If Φ has previously been proven as a theorem, then any formula of the form □Φ may be introduced at any line of a proof. |
| □= | Necessity of identity | From α = β, infer □α = β. |
(Nolt 328)
| Free Logic Quantification Inference Rules |
| Free Existential Introduction (F∃I) Let Φ be any formula containing some name α and Φβ/α be the result of replacing at least one occurrence of α in Φ by some variable β not already in Φ. Then from Φ and ∃x x = α infer ∃βΦβ/α. |
| Free Existential Elimination (F∃E) Let ∃βΦ be any existential formula, Ψ any formula, and α any name that occurs neither in Φ nor in Ψ. And let Φα/β be the result of replacing all occurrences of the variable β in Φ by α. Then, given a derivation of Ψ from the hypothesis Φα/β & ∃x x = α, end the hypothetical derivation and from ∃βΦ infer Ψ, provided that α does not occur in any other hypothesis whose hypothetical derivation has not ended or in any assumption. |
| Free Universal Introduction (F∀I) Let Φ be a formula containing a name α, and let Φβ/α be the result of replacing all occurrences of α in Φ by some variable β not already in Φ. Then given a derivation of Φ from the hypothesis ∃x x = α, end the hypothetical derivation and infer ∀βΦβ/α, provided that α does not occur in any other hypothesis whose hypothetical derivation has not yet ended or in any assumption. |
| Free Universal Elimination (F∀E) Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ for some name α. Then from ∀βΦ and ∃x x = α infer Φα/β. |
(Nolt 403)
]
Nolt will now show us how to make inferences in free logic using our new rules. He begins with this one:
∀x (Fx → Gx), Fa, ∃x x = a ⊢ ∃xGx
(Nolt 404)
[Let us first set it up.
| 1. | ∀x (Fx → Gx) | A |
| 2. | Fa | A |
| 3. | ∃x x = a | A |
We have the universally quantified expression in line 1 and the existence formulation in line 3. Recall now the free universal elimination rule:
Free Universal Elimination (F∀E) Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ for some name α. Then from ∀βΦ and ∃x x = α infer Φα/β.
(Nolt 403)
Let us look closer at the formulation in the rule reading: ∀βΦ. This will be fulfilled by the expression in line 1: ∀x(Fx→Gx). We see the universal quantifier in both. The beta symbol is the equivalent of the x variable. And the phi symbol is the equivalent of the whole conditional statement. So, we have fulfilled that requirement. The next requirement, that we have ∃x x=α, is fulfilled by ∃x x = a. The rule says that when we fulfill these requirements, we can substitute the name that we said exists for the variable in the universally quantified formula. This means that we can use free universal elimination to take ∀x(Fx→Gx) and from it derive Fa → Ga.
| 1. | ∀x (Fx → Gx) | A |
| 2. | Fa | A |
| 3. | ∃x x = a | A |
| 4. | Fa → Ga | 1,3 F∀E |
Now, what can we do next? Recall that our goal proposition is ∃xGx. So we will want a formula with G. We see that we can affirm the antecedent of the new conditional, using line 2, to get Ga. So let us do that next.]
| 1. | ∀x (Fx → Gx) | A |
| 2. | Fa | A |
| 3. | ∃x x = a | A |
| 4. | Fa → Ga | 1,3 F∀E |
| 5. | Ga | 2, 4 →E |
Now how do we go from Ga to ∃xGx? We will need to introduce existential quantification. Recall that the rule for free existential introduction:
Free Existential Introduction (F∃I) Let Φ be any formula containing some name α and Φβ/α be the result of replacing at least one occurrence of α in Φ by some variable β not already in Φ. Then from Φ and ∃x x = α infer ∃βΦβ/α.
(Nolt 403)
So the first requirement is that we have a formula Φ which is structured in such a way that a variable can be substituted for some name in it (with that substitution being for at least one occurence of the name, but possibly more), and that variable must not already be in the formula. The second requirement is that we have ∃x x = α. And from those conditions we can derive an existentially quantified formula (of the first formula) with the substituted variable. So our Φ formula here is Ga, and the ‘a’ can be substituted by x. We also have ∃x x = a, which establishes the existence of ‘a’. This means that we can derive ∃xGx, which was our goal proposition.]
| 1. | ∀x (Fx → Gx) | A |
| 2. | Fa | A |
| 3. | ∃x x = a | A |
| 4. | Fa → Ga | 1,3 F∀E |
| 5. | Ga | 2, 4 →E |
| 6. | ∃xGx | 3, 5 F∃I |
(Nolt 404)
Nolt next makes a proof for:
⊢ ∀x(Fx → ∃yFy)
(Nolt 404)
[So recall the strategic rule for conditional statements: “Hypothesize Φ and work toward the subconclusion Ψ in order to obtain the conditional by →I” (Nolt 99). But before we take that step into consideration, consider the fact that we will need at some point to introduce universal quantification. So recall the rule for free universal introduction.
Free Universal Introduction (F∀I) Let Φ be a formula containing a name α, and let Φβ/α be the result of replacing all occurrences of α in Φ by some variable β not already in Φ. Then given a derivation of Φ from the hypothesis ∃x x = α, end the hypothetical derivation and infer ∀βΦβ/α, provided that α does not occur in any other hypothesis whose hypothetical derivation has not yet ended or in any assumption.
(Nolt 403)
So as we can see, this rule involves a hypothesis of ∃x x = α. From this hypothesis, within its subproof, we need to derive a formula that contains some name that can be substituted with a variable. After we derive that formula, we then derive into the outer proof that formula now with all occurences of the name substituted with the variable, and we universally quantify over it. So what we will want to derive using this rule is the universally quantified formula ∀x(Fx → ∃yFy). As we can see, there is a conditional where both the antecedent and the consequent have the same predicate. But the consequent has an existential quantification. So if our last step is free universal introduction, then that means we will be substituting x for the name in the antecedent. We will use ‘a’ as our name. So prior to this step we will have Fa → ∃yFy. As we saw above from the strategic rule, to get this structure we first assume the antecedent, Fa, and then we derive the consequent. In order to derive that, we can apply free existential introduction to Fa, so long as we have ∃x x = a. If you recall from the rule for free universal introduction, we also needed ∃x x = a as a hypothesis. So it is convenient that we first hypothesize ∃x x = a, which will allow us to use both free existential introduction and free universal introduction in the ways just mentioned.]
| 1. | | ∃x x = a | H (for F∀I) |
| 2. | | | Fa | A |
| 3. | | | ∃yFy | 1, 2 F∃I |
| 4. | | Fa → ∃yFy | 1-3 →I |
| 5. | ∀x(Fx → ∃yFy) | 1-4 F∀I |
(Nolt 404)
Nolt next makes the proof for:
∃xFx ⊢ ∃x⋄Fx
(Nolt 404)
[Nolt will introduce a a theorem that was proven in a prior section, so it will hard to work out this proof on our own. The rule that he will eventually use is free existential elimination.
Free Existential Elimination (F∃E) Let ∃βΦ be any existential formula, Ψ any formula, and α any name that occurs neither in Φ nor in Ψ. And let Φα/β be the result of replacing all occurrences of the variable β in Φ by α. Then, given a derivation of Ψ from the hypothesis Φα/β & ∃x x = α, end the hypothetical derivation and from ∃βΦ infer Ψ, provided that α does not occur in any other hypothesis whose hypothetical derivation has not ended or in any assumption.
(Nolt 403)
So we will make a hypothesis of the form ‘Φα/β & ∃x x = α’, where ‘Φα/β ’ is a formula where all the occurances of some variable are replaced with a name. Now also, the formula in this hypothesis needs to have a predicate found in some existentially quantified expression that is already given, and the variable that is replaced in ‘Φα/β ’ needs to be the variable in that same existentially quantified expression. So we have as a premise ‘∃xFx’ . This means that our predicate is ‘F’ and our variable is x. So that will go in the first line. Then, following free existential elimination, we hypothesize a structure of the form ‘Φα/β & ∃x x = α’. We already said that our Φ is ‘F’. We will arbitrarily decide that our name will be ‘a’. So that means we hypothesize specifically ‘Fa & ∃x x = a’. Free existential elimination says that we from this hypothesis derive some other formula, then on the basis of the given ‘∃xFx’ and the hypothesized derivation in the subproof, we obtain that same hypothetically derived formula in the main proof. In our case, we will want this derived formula to be out goal proposition of ‘∃x⋄Fx’. So from our hypothesis ‘Fa & ∃x x = a’ we need to derive ‘∃x⋄Fx’. Nolt will do this in part by using a theorem proven from before, which will give us ‘⋄Fa’. Then from this we will derive ‘∃x⋄Fx’ using free existential introduction.]
| 1. | ∃xFx | A |
| 2. | | Fa & ∃x x = a | H (for F∃E) |
| 3. | | Fa | 2 &E |
| 4. | | ⋄Fa | 3 P ⊢ ⋄P |
| 5. | | ∃x x = a | 2 &E |
| 6. | | ∃x⋄Fx | 4, 5 F∃I |
| 7. | ∃x⋄Fx | 1, 2-6 F∃E |
(Nolt 404)
Nolt will now prove:
⊢ ∀xFx → (~Fa → ~∃x x = a)
(Nolt 405)
[Recall our strategic rule from above that when we want to prove a conditional, we hypothesize the antecedent and try to derive the consequent. Nolt will do this for the main operator and then again for the nested conditional. This means that in the nested conditional we need to derive ‘~∃x x = a’. Recall then the strategic rule for negated atomic formulas. “Hypothesize Φ and work toward a subconclusion of the form Ψ & ~Ψ in order to obtain ~Φ by ~I” (Nolt 99). This means that Nolt will make a third assumption ‘∃x x = a’.
| 1. | | ∀xFx | H (for →I) |
| 2. | | | ~Fa | H (for →I) |
| 3. | | | | ∃x x = a | H (for ~I) |
Now, we need to find a contradiction so that we can derive ‘~∃x x = a’. We have already ‘~Fa’, so can we obtain ‘Fa’? We also have ‘∀xFx’. Recall free universal elimination: “Free Universal Elimination (F∀E). Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ for some name α. Then from ∀βΦ and ∃x x = α infer Φα/β.” Our ‘∀βΦ’ formula is ‘∀xFx’. We also have ‘∃x x = a’. We have fulfilled our requirements. This means that we can derive ‘Fa/x’. Thus we get ‘Fa’, which will provide a contradiction on the basis of which we derive ‘~∃x x = a’ in our second subproof.
| 1. | | ∀xFx | H (for →I) |
| 2. | | | ~Fa | H (for →I) |
| 3. | | | | ∃x x = a | H (for ~I) |
| 4. | | | | Fa | 1, 3 F∀E |
| 5. | | | | Fa & ~Fa | 2, 4 &I |
| 6. | | | ~∃x x = a | 3-5 ~I |
Then, as planned we can obtain ‘~Fa → ~∃x x = a’ in our first subproof and then ‘∀xFx → (~Fa → ~∃x x = a)’ in our main proof, which was the goal proposition.]
| 1. | | ∀xFx | H (for →I) |
| 2. | | | ~Fa | H (for →I) |
| 3. | | | | ∃x x = a | H (for ~I) |
| 4. | | | | Fa | 1, 3 F∀E |
| 5. | | | | Fa & ~Fa | 2, 4 &I |
| 6. | | | ~∃x x = a | 3-5 ~I |
| 7. | | Fa → ~∃x x = a | 2-6 →I |
| 8. | ∀xFx → (Fa → ~∃x x = a) | 1-7 →I |
(Nolt 405)
Nolt then does a final proof that will also use modal logic rules.
□∀xFx, ⋄∃x x = a ⊢ ⋄Fa
(Nolt 405)
[Nolt will import a theorem in one of the steps, so it will be hard for us to work through it on our own. Recall from section 11.4 how Nolt shows us a useful strategy of combining rules N and K, which are: “N Necessitation: If Φ has previously been proven as a theorem, then any formula of the form □Φ may be introduced at any line of a proof;” and “K rule: From □(Φ → Ψ), infer (□Φ → □Ψ)” (Nolt 328). So first let us observe Nolt setting up the proof and using these rules.]
| 1. | □∀xFx | A |
| 2. | ⋄∃x x = a | A |
| 3. | □(∀xFx → (~Fa → ~∃x x = a)) | N (∀xFx → (~Fa → ~∃x x = a)) |
| 4. | □∀xFx → □(~Fa → ~∃x x = a) | 3 K |
We want to prove ‘⋄Fa’. We see in line 4 that we have its negation. This means that were we to use modus ponens (conditional elimination) to obtain the consequent of line 4, and then use modus tollens to obtain the negation of the antecedent, we would roughly have a path for arriving at our goal proposition. But we will also need to convert its modal operator to possibility. For now, let us first obtain that consequent.
| □∀xFx | A | |
| 2. | ⋄∃x x = a | A |
| 3. | □(∀xFx → (~Fa → ~∃x x = a)) | N (∀xFx → (~Fa → ~∃x x = a)) |
| 4. | □∀xFx → □(~Fa → ~∃x x = a) | 3 K |
| 5. | □(~Fa → ~∃x x = a) | 1, 4 →E |
As we can see, we have the basis to for MT in line 2. What we would need to do is convert to a necessity operator, while also distributing the necessity operator in line 5. So let us do those things.
| 1. | □∀xFx | A |
| 2. | ⋄∃x x = a | A |
| 3. | □(∀xFx → (~Fa → ~∃x x = a)) | N (∀xFx → (~Fa → ~∃x x = a)) |
| 4. | □∀xFx → □(~Fa → ~∃x x = a) | 3 K |
| 5. | □(~Fa → ~∃x x = a) | 1, 4 →E |
| 6. | □~Fa → □~∃x x = a | 5 K |
| 7. | ~□~∃x x = a | 2 DUAL |
Now we have what we need to obtain the negation of the antecedent in line 6.
| 1. | □∀xFx | A |
| 2. | ⋄∃x x = a | A |
| 3. | □(∀xFx → (~Fa → ~∃x x = a)) | N (∀xFx → (~Fa → ~∃x x = a)) |
| 4. | □∀xFx → □(~Fa → ~∃x x = a) | 3 K |
| 5. | □(~Fa → ~∃x x = a) | 1, 4 →E |
| 6. | □~Fa → □~∃x x = a | 5 K |
| 7. | ~□~∃x x = a | 2 DUAL |
| 8. | ~□~Fa | 6, 7 MT |
This gives us a structure that we can convert into our goal proposition.]
| 1. | □∀xFx | A |
| 2. | ⋄∃x x = a | A |
| 3. | □(∀xFx → (~Fa → ~∃x x = a)) | N (∀xFx → (~Fa → ~∃x x = a)) |
| 4. | □∀xFx → □(~Fa → ~∃x x = a) | 3 K |
| 5. | □(~Fa → ~∃x x = a) | 1, 4 →E |
| 6. | □~Fa → □~∃x x = a | 5 K |
| 7. | ~□~∃x x = a | 2 DUAL |
| 8. | ~□~Fa | 6, 7 MT |
| 9. | ⋄Fa | 8 DUAL |
(Nolt 405)
From:
Nolt, John. Logics. Belmont, CA: Wadsworth, 1997.
Or if otherwise noted:
Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman & Littlefield, 2013.
.
