Thanks for asking. You’re the first to do so. I’ve read a paper suggesting that S5 is too strong a logic for examining existential necessity as it might relate to existential contingency. And so, as I explained in the OP, the Euclidean frame seems to do this after all if one just models objectivity and subjectivity along the lines I described.
The former is existence such that nonexistence is impossible. The latter is contingent existence.
Because existence is the quality that I care to examine, just as a baseball is the thing I desire to hit.
I’m not sure what you mean by that. Presumably, you mean something by “can prove the necessary existence of anything that exists necessarily” which is less trivial than “can prove that anything which exists necessarily exists necessarily” but not quite on the level of “necessarily, everything that exists exists necessarily”, which is what Frylock (and I) found objectionable (implying, as it does, that, for example, the Eiffel tower exists necessarily, which seems absurd). But I’m not sure what exactly your meaning would be if not one of those. At any rate, it seems that the formal statement you have proven in this logic is the latter.
It does seem to me that Frylock’s objection to this particular combined system of first-order logic and S5 modal logic would be the same as mine, that it essentially forces the same set of individuals to exist at all possible worlds, and that there isn’t strong motivation for allowing the quantifier and modal rules to intermingle in a fashion entailing this, except that it’s slightly easier to specify the rules of inference. Which is why I generally argue for other systems combining first-order logic and S5 in more careful manners.
In your model, what does it mean for a proposition to be true in a possible world? What is the interpretation of the accessibility relation? What is the interpretation of a name? Of a quantifier?
If you will answer these pedantic questions, I may be able to get a better grip on what you’re trying to do. As it stands, it looks to me as though you are interpreting erstwhile “possible worlds” as points of view, such that something exists in a world iff it has a point of view identical with everything that exists in that world. But if I’m right about this concerning your model, then the existence quantifier in your model does not stand for existence in the usual sense, but rather, for the having of a point of view. What you’re calling “existential necessity” would not be “necessary existence” but rather “the having of all points of view.”
I doubt I’m right about the interpretation your building for two reasons. First, you seem to be trying to formulate a response to the paper you referenced, but in that paper what is being talked about is necessary existence, not the having of all points of view or anything like that. I can’t see how you can respond to the points in that paper if you aren’t talking about necessary existence. (Then again I haven’t read the entire paper closely.) Second, in another post to me you said you don’t think God has every point of view. On my interpretation, your model is of a logic in which some entity does have every point of view. (Or at least, on my interpretation of what I take to be your model, nothing rules out such an entity.)
So the big question for me is probably: Since you are trying to model objectivity and subjectivity, could you explain (again, I guess?) how objectivity and subjectivity figure into the interpretation of some symbol or symbols in your model?
Now, regarding your theorem
my comment
and your reply
I don’t understand some things. For one thing, my parenthetical “in the domain of discourse” would seem to indicate I’m not giving an “actualist” reading of the theorem. For another, I seem (to me) to simply be offering a straightforward reading of what the theorem says on a standard interpretation:
For all x, there necessarily exists some y such that y is identical to x,
in other words,
For all x, it is the case in every possible world that some y in that possible world is identical to x
in other words
For all x, it is the case in every possible world that x exists in that possible world
in other words
Everything exists in every possible world.
(Note: On my interpretation of what I take to be your model of objectivity, we migh read the theorem instead as saying “Everything has every possible point of view,” but surely that’s not what you want to say either?! Further evidence that my interpretation of what I take to be your model is in some way deficient.)
On an “actualist” reading, “For all x” should be read as “concerning each thing that actually exists,” while on another kind of reading, “For all x” should be read as “concerning each thing that we are talking about (whether it actually exists or not)” Yet another kind of reading would go “concerning each thing that exists in any world whatsoever.” Read “for all x” whichever way you like, in each case you have a very strong statement: Everything (in the relevant sense of “everything”) necessarily exists.
This isn’t an absurd position–some logicians and metaphysicians think it’s true–but it strikes me as not being something you intend to affirm, whether on a standard interpretation (which seems to me to be the right way to try to use S5 to talk about necessary existence, which in turn seems to be what the paper you referenced is trying to talk about) or on several other interpretations I have tried out in trying to understand your project.
As you say, “Necessary existence is true in S5,” by which I take you to just mean that however you interpret an S5 model, the theorem you’ve given can be proven. (It’s been a while since I had to deal with this stuff, but I’ll just stipulate to this. Your proof looked alright to me.) The question for me is, what is the interpretation of that theorem in your model? Interpreted, does it end up saying something you want to affirm, or not? And what is that thing that it says?
Just as an interesting (to me) side note, the dual theorem has to do with more than just what can be derived from the GA.
The theorem says that given any axiom scheme with a conditional as its main connector, and given a system containing the instances of that scheme as axioms, another system containing, not those instances, but rather instances of the dual of the scheme, proves all and only the very same theorems provable under the original given scheme.
The dual of an axiom scheme is the scheme produced by replacing each operator in the scheme with its dual, and switching the places of the antecedent and consequent parts of that scheme. The dual of the necessity operator is the possibility operator, the dual of the universal quantifier is the existential quantifier, the dual of negation is negation, the dual of and is or, and vice versa in all four cases.
(In fact, you can define “dual” completely generally as follows. Given an operator O which takes some number of propositions P1, P2, … Pn as arguments, the dual D of O is defined as an operator which gives the same values for any P1, P2, … Pn as the negation of O when each of P1, P2, … Pn is also negated.)
For some reason I’ve always thought this was kind of cool. The duals of some very plausible and intuitive axiom schema are, in turn, not so plausible or intuitive sounding. (For example, the pair that started me on this topic: the dual of the intuitive <>P -> <>P is the nonintuitive <>P -> P.) But the intuitive and non-intuitive versions, it turns out, sort of mean the same thing, at least for all practical purposes.
Well, here, off the top of my head, seems to be a proof that works in classical logic. The dual of an axiom is readily seen to be equivalent to its contrapositive with all variables negated, by considering all possible connectives. Whenever A is an element of an axiom scheme, so are all substitution instances of A, including A with all its variables negated. And, of course, every statement implies its contrapositive. So, putting all that together, you get what you need.
Can I have a cut of the $5 million if someone offers it to you?
As I’ve said, it’s been a while since I had to deal with this stuff, but to my recollection, you only get <>A -> A when A is provable without any premises. That doesn’t seem so problematic to me. It just amounts to saying that if something is a logical truth, it is a necessary truth (I hope I got my vocab right there) and while that’s not something everyone thinks is correct, most do and it is certainly intuitively plausible.
Incidentally, I made a joke about precisely this notion of duality the other day, which went completely unnoticed, but which I can’t resist the opportunity to link.
Every normal modal logic (in the technical sense of “normal”) gives you A whenever it can prove A without premises, and thus gives you B -> A whenever A can be proved without premises. However, in S5, you actually get <>A -> A for everything (MrDibble did mean to say <>A -> A, per clarification in post #52)
What was at stake was a grade in a course, not $5 million.
I asked if proving the dual theorem would count as a good final project. My teacher said yes, and warned me it would be a lot more difficult than I probably thought. I accepted the (self-imposed) challenge. I sure wish I could remember how the thing went.
Your approach was my first approach. My teacher, with a twinkle in his eye and a kindly smile, explained why it doesn’t work. I don’t remember exactly why, but it turns on the distinction between “X is provable in a system with axiom A” and “A implies X.” Somehow this ended up mattering. Dammit, I forget why.
The problem ended up turning on the fact that while p -> p implies -p -> <>-p, it does not imply p -> <>p.
I’m starting to think I may have formulated the dual theorem incorrectly above. Maybe the theorem is not in terms of axiom schemes, but in terms of axioms, to wit, given an axiom, a system with the dual of the axiom instead is exactly as powerful. That would make sense of my claim that the fact mentioned in the previous paragraph was important somehow. Since p -> p and p -> <>p do not mutually imply each other, it is not trivial to show that a system using one as an axiom is exactly as powerful as a system using the other as an axiom instead. And maybe my proof turned out looking at axiom schemes in a way similar to what you’ve done in your post. Except I feel quite certain that I tried that, and there was something wrong with it.
Oh dammit now I’m confused. I wonder if I were to email the prof if he’d even remember who I was?
If A1 & … & An |- B, then A1 & … & An |- B. As a special case, when n = 0, we have that B can be proved without premises whenever B can, the fact you mentioned above. (Also, in non-classical logics, where <> can’t simply be defined in terms of , you’ll want the condition that if A |- B1 v … v Bn, then <>A |- <>B1 v … v <>Bn; the n = 0 special case becomes that <>A is refutable whenever A is). The importance of the concept is that for any class of Kripke frames, the corresponding logic is normal. (Indeed, I’d say a modal operator doesn’t deserve to use the or <> symbol if it doesn’t satisfy the associated normality condition).
Indeed, it’s impossible to do so: the former system trivially proves p -> p, and the latter system does not. If they were equally powerful, they’d have to mutually imply each other, at least on my interpretation of what “equally powerful” means.
I’m now really curious what the dual theorem you dealt with was. Did it have any more specific name?
Oh, I’m thinking now, maybe the distinction was “Is X provable in a system with axiom A?” means “Add |- A to your system but preserve the rules of inference. Can you produce a cut-free proof of |- X?”, as opposed to just “Can you show A |- X?”.
So perhaps the duality theorem you proved was “When you add |- A to a system and preserve its rules of inference, then you can produce a cut-free deduction of |- dual(A)”.
(I specified cut-free deductions because f you allowed the cut rule (from A |- B and B |- C, derive A |- C), it would trivialize back to there being no distinction)
Great input guys, thanks! For the sake of time, I’ll respond to a specific post from Frylock. The side discussions are interesting, but the notion that you two can get me closer to my goal is too precious to let slip away.
It means that there is at least one actual world in which the proposition is true.
In this case, I interpret it as expressing a view from one world onto another. So, for world W1 where <>A is true, world W2 where A is true in actuality has a view onto W1. And obviously if A is true, then every possible world has a view onto every other possible world.
I’m not sure I understand that question, unless you mean something like the name of a variable, in which case I do distinguish the variable A from its name “A”. The name represents the variable, but the variable may represent something else.
Being self-educated, the only quantifiers I’m familiar with are the universal and existential quantifiers, though I can see why in theory there might be others. But to answer your question directly, when I quantify a statement, I’m basically completing it.
Well, first of all, keep in mind that all I was doing with that particular example was basically answering the question of what can be done with S5, as in what is it good for? I wasn’t using it to solve my OP because, after all, that is what I’m seeking help to achieve. I didn’t want to do anything even approaching the actual existence of some necessary entity because of the assurity that the thread would be derailed into yet another squabble over the MOP. And God knows, there’ve been plenty of those already.
So what I’m trying to do is find the best tool to analyze the kind of relations I described in the OP (and some subsequent posts) of a world W that has access (or a view onto) all possible worlds (including itself) combined with worlds W1…Wn that have access (or views onto) only themselves and the world W but not onto each other. If the Euclidean frame accomodates that model, then S5 would accomodate analyzing it.
Incidentally, I’m not sure what Indisputable’s objection is to having some K statements in an S5 tableau. It seems to me that (1) K statements are subsumed by S5, and (2) X can be read as “actual X”, where actuality is just another modal along with possibility and necessity.
Oh, in the previous post, I meant for everything to be in terms of axiom schemes, as opposed to single axioms (where the task is clearly impossible, as pointed out before). So, the final theorem would be “When you add all instances |- A of some axiom scheme to your system, then you should be able to produce cut-free deductions of |- B for all instances of the dual axiom scheme”. Perhaps. I fear I am running the thread too far off course now, though.
Fuck! I got the bad quote block fixed, but when I tried to fix Indistinguishable’s name the goddamn server locked up. Please read **Indisputable ** as Indistinguishable, and please accept my apology.
Also, please change this gem “It means that there is at least one actual world in which the proposition is true” to read “It means that there is at least one possible world in which the proposition is true.”
ETA: No worries; I suppose it’s a compliment to be considered Indisputable.
I don’t think I ever said anything like objecting to having K statements in an S5 tableau. What I object to is the way you allow your universal and existential quantifiers to interact with your modal operators, as in the proof in #43. There are many S5 systems of first-order logic in which that proof is not considered valid, often because of line 6, which applies the rule of necessitation to a statement with a free variable. Obviously, your proof is valid in such systems as do allow that, but a system can disallow that and still be a perfectly cromulent S5 system of first-order logic (as long as it continues to prove all the instances of the S5 axioms and all the instances of the axioms of first-order logic). For example, in Kripke’s Quantified Modal Logic, that proof fails to go through, even though that system is undeniably an S5 one.
So what I object to is systems mingling modal logic and first-order quantifiers which do not take special care (like preventing necessitation on statements with free variables) to avoid such issues. I object because the conclusions that can be drawn otherwise seem to me absurd on their face (any notion of necessity where the Eiffel tower necessarily exists is not really the notion of necessity we want to capture).
Thanks, Indistinguishable. Again, the perils of autodidacticism. I’m entirely open to supplying **Bryan ** some other example of S5 in action. Feel as free as you wish. (And especially so if it accomodates what I’m asking for in #96.)
For the sake of time, I’ll respond to a specific post from Frylock. The side discussions are interesting, but the notion that you two can get me closer to my goal is too precious to let slip away.