Fitch's paradox and OWA
in [Logic]
|
From: Daryl McCullough on 3 Jan 2010 12:32 Jan Hidders says... > >On 3 jan, 14:09, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: >> Jan Hidders says... >> >> >The purpose of (3) was only to illustrate the translation of formulas >> >in the original logic to your logic. You are right that by itself it >> >does not show the paradox. But if this translation exists then all >> >formulas used in the proof of the paradox will have their equivalents >> >in your logic. >> >> Yes, but my point is that in the more expressive logic, the >> knowability principle can be expressed as >> >> forall p:P, exists w:W, k(w,p) > >Er, I think you forgot the part where it requires that p is true. Right. Thanks. >But if you fix that, then this is indeed equivalent with the one used in >the Stanford page. This one will still lead to the conclusion that all >truths are known. No, it doesn't. I already went through this. In the Stanford logic, if p is some proposition such that p & ~K(p), then the application of the knowability principle gives (in some world w') K(p & ~K(p)) which is a contradiction. My rule does *not* lead to that conclusion. Instead, we have, for some world w, p & ~k(w,p) If we apply my version of the knowability principle, we get, for some world w' k(w',(p & ~k(w,p))) which is *not* a contradiction. Proposition p is known in world w', but not in world w. For clarification, the propositions in this type theory are *non-modal*. >> The original knowability principle, when translated into this >> new logic, would look something like this: >> >> forall f:W -> P, forall w:W, f(w) -> exists w':W, f(w') & k(w',f(w')) >> >> The "propositions" of modal logic are actually functions on worlds. > >Really? This is actually a stronger principle that implies the >previous one since as a particular case I can take for f the function >that maps each world to the same predicate p in P. Right. It's *too* strong, which is why it leads to a contradiction (together with the principle of non-omniscience). >Also, I don't understand what you mean by "propositions are actually >functions on world" except that the same proposition can have a >different semantics in different worlds, That's exactly what I mean. For each modal proposition p (which varies from world to world) we can associate a function f_p from worlds to nonmodal propositions as follows: f_p(w) == the nonmodal proposition "p is true in world w" >and that was already taken into account in the old semantics. Yes. It's the old *syntax* that was inadequate to express a reasonable knowability principle. -- Daryl McCullough Ithaca, NY
From: Jan Hidders on 3 Jan 2010 13:10 On 3 jan, 18:32, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Jan Hidders says... > > > > > > > > >On 3 jan, 14:09, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > >> Jan Hidders says... > > >> >The purpose of (3) was only to illustrate the translation of formulas > >> >in the original logic to your logic. You are right that by itself it > >> >does not show the paradox. But if this translation exists then all > >> >formulas used in the proof of the paradox will have their equivalents > >> >in your logic. > > >> Yes, but my point is that in the more expressive logic, the > >> knowability principle can be expressed as > > >> forall p:P, exists w:W, k(w,p) > > >Er, I think you forgot the part where it requires that p is true. > > Right. Thanks. > > >But if you fix that, then this is indeed equivalent with the one used in > >the Stanford page. This one will still lead to the conclusion that all > >truths are known. > > No, it doesn't. I already went through this. In the Stanford logic, > if p is some proposition such that p & ~K(p), then the application > of the knowability principle gives (in some world w') > > K(p & ~K(p)) > > which is a contradiction. My rule does *not* lead to that > conclusion. Instead, we have, for some world w, > > p & ~k(w,p) > > If we apply my version of the knowability principle, we get, > for some world w' > > k(w',(p & ~k(w,p))) > > which is *not* a contradiction. Proposition p is known in world w', > but not in world w. Hmm. That only shows that in that particular way you don't get a contradiction. But my claim is that you do get a contradiction for the simple reason that your logic contains the old logic. > >> The original knowability principle, when translated into this > >> new logic, would look something like this: > > >> forall f:W -> P, forall w:W, f(w) -> exists w':W, f(w') & k(w',f(w')) > > >> The "propositions" of modal logic are actually functions on worlds. > > >Really? This is actually a stronger principle that implies the > >previous one since as a particular case I can take for f the function > >that maps each world to the same predicate p in P. > > Right. It's *too* strong, which is why it leads to a contradiction > (together with the principle of non-omniscience). But it doesn't correspond in any way to the semantics of the knowability principle in the old logic. The model theory there says something very different. So in what sense is this the semantics of the old knowability principle? > >Also, I don't understand what you mean by "propositions are actually > >functions on world" except that the same proposition can have a > >different semantics in different worlds, > > That's exactly what I mean. For each modal proposition p > (which varies from world to world) we can associate a function > f_p from worlds to nonmodal propositions as follows: > > f_p(w) == the nonmodal proposition "p is true in world w" > > >and that was already taken into account in the old semantics. > > Yes. It's the old *syntax* that was inadequate to express a > reasonable knowability principle. But until now you have only shown that in the new syntax you can express an equivalent one (you can verify that by looking at the model theories) and one that's even stronger. -- Jan Hidders
From: Daryl McCullough on 3 Jan 2010 14:55 Jan Hidders says... > >On 3 jan, 18:32, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: >> In the Stanford logic, >> if p is some proposition such that p & ~K(p), then the application >> of the knowability principle gives (in some world w') >> >> K(p & ~K(p)) >> >> which is a contradiction. My rule does *not* lead to that >> conclusion. Instead, we have, for some world w, >> >> p & ~k(w,p) >> >> If we apply my version of the knowability principle, we get, >> for some world w' >> >> k(w',(p & ~k(w,p))) >> >> which is *not* a contradiction. Proposition p is known in world w', >> but not in world w. > >Hmm. That only shows that in that particular way you don't get a >contradiction. Well, the point is that the contradiction derived in Fitch's paradox does not go through. It's certainly possible that some other paradox can be derived, but I don't see any evidence of that. >But my claim is that you do get a contradiction for the >simple reason that your logic contains the old logic. It doesn't contain the same *axioms*. In particular, I'm rejecting the "knowability principle" in favor of a variant principle that is (as far as I can see) consistent. >> >> The original knowability principle, when translated into this >> >> new logic, would look something like this: >> >> >> forall f:W -> P, forall w:W, f(w) -> exists w':W, f(w') & k(w',f(w')) >> >> >> The "propositions" of modal logic are actually functions on worlds. >> >> >Really? This is actually a stronger principle that implies the >> >previous one since as a particular case I can take for f the function >> >that maps each world to the same predicate p in P. >> >> Right. It's *too* strong, which is why it leads to a contradiction >> (together with the principle of non-omniscience). > >But it doesn't correspond in any way to the semantics of the >knowability principle in the old logic. It certainly does. It's just a translation of the principle into a more expressive logic. >The model theory there says >something very different. So in what sense is this the semantics of >the old knowability principle? It's the same semantics! Let's try to make this more explicit. You have a set W of possible worlds, a set MP of modal propositions, and for each world w, a set S_w of the elements of MP true in world w. The set S_w is constrained by the following rules: 1. If Kp is in S_w, then p is in S_w (you can only know true statements) 2. And(p,q) is in S_w iff p is in S_w and q is in S_w 3. Or(p,q) is in S_w iff p is in S_w or q is in S_w. 4. Not(p) is in S_w iff p is not in S_w 5. Implies(p,q) is in S_w iff p is not in S_w or q is in S_w 6. <>p is in S_w iff for some w', p is in w' 7. []p is in S_w iff for all w', p is in w' Now, to capture this semantics in type theory, we use the following translations: 1. Introduce a type, W, of all possible worlds. 2. Introduce a type, A, of all atoms (atomic modal propositions). 3. Introduce the predicate t(w,a) saying which atoms are true in which possible worlds. 4. Introduce a predicate k(w,p) saying which propositions are known in which worlds. 5. Define MP, the type of all modal propositions, to be the type of functions from W into P. 6. For each atom a, we associate a corresponding element of MP: p_a == that function f such that f(w) = t(w,a). 7. Define the operator K as follows: Kf == that function g such that g(w) = k(w,p) 8. Define the operator And as follows: And(f,g) == that function h such that h(w) = f(w) & g(w) 9. Similarly for Or, Implies, Not 10. Define the operator <> as follows: <>f == that function g such that g(w) = exists w':W, f(w') 11. Define the operator [] as follows: []f == that function g such that g(w) = forall w':W, f(w') >> >Also, I don't understand what you mean by "propositions are actually >> >functions on world" except that the same proposition can have a >> >different semantics in different worlds, >> >> That's exactly what I mean. For each modal proposition p >> (which varies from world to world) we can associate a function >> f_p from worlds to nonmodal propositions as follows: >> >> f_p(w) == the nonmodal proposition "p is true in world w" >> >> >and that was already taken into account in the old semantics. >> >> Yes. It's the old *syntax* that was inadequate to express a >> reasonable knowability principle. > >But until now you have only shown that in the new syntax you can >express an equivalent one (you can verify that by looking at the model >theories) and one that's even stronger. No, the new "knowability principle" is *not* equivalent. Look, once again, I'm formalizing the knowability principle as: forall p:P, p -> exists w:W, k(w,p) I'm formalizing the non-omniscience principle as: forall w:W, exists p:P, ~k(w,p) These axioms do *not* lead to a contradiction. -- Daryl McCullough Ithaca, NY
From: Jan Hidders on 4 Jan 2010 10:59 On 3 jan, 20:55, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > Jan Hidders says... > > > > > > > > >On 3 jan, 18:32, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: > >> In the Stanford logic, > >> if p is some proposition such that p & ~K(p), then the application > >> of the knowability principle gives (in some world w') > > >> K(p & ~K(p)) > > >> which is a contradiction. My rule does *not* lead to that > >> conclusion. Instead, we have, for some world w, > > >> p & ~k(w,p) > > >> If we apply my version of the knowability principle, we get, > >> for some world w' > > >> k(w',(p & ~k(w,p))) > > >> which is *not* a contradiction. Proposition p is known in world w', > >> but not in world w. > > >Hmm. That only shows that in that particular way you don't get a > >contradiction. > > Well, the point is that the contradiction derived in Fitch's > paradox does not go through. It's certainly possible that some > other paradox can be derived, but I don't see any evidence of > that. Fair enough. But I think I do. > >But my claim is that you do get a contradiction for the > >simple reason that your logic contains the old logic. > > It doesn't contain the same *axioms*. In particular, I'm > rejecting the "knowability principle" in favor of a variant > principle that is (as far as I can see) consistent. Well, I'm not so sure. Your new variant look very similar to how the principle is formulated in my model theory. And there I got the contradiction. > Let's try to make this more explicit. > You have a set W of possible worlds, a set MP of > modal propositions, and for each world w, a set S_w of > the elements of MP true in world w. The set S_w is constrained > by the following rules: > > 1. If Kp is in S_w, then p is in S_w (you can only know true > statements) > 2. And(p,q) is in S_w iff p is in S_w and q is in S_w > 3. Or(p,q) is in S_w iff p is in S_w or q is in S_w. > 4. Not(p) is in S_w iff p is not in S_w > 5. Implies(p,q) is in S_w iff p is not in S_w or q is in S_w > 6. <>p is in S_w iff for some w', p is in w' > 7. []p is in S_w iff for all w', p is in w' That already looks close enough to a model theory to me. A model could be a pair (W, S) with W the set of possible worlds and S : W -> 2^F where F is the set of formulas and satisfies the rules 1-7. I strongly conjecture that those models would be isomorphic to the models in my formulation of the model theory and lead to the same formulas being true. Your mapping to type theory is a bit hard for me to get my head around, so I'll assume for the moment that the above is your model theory. > Now, to capture this semantics in type theory, we use > the following translations: > > 1. Introduce a type, W, of all possible worlds. > 2. Introduce a type, A, of all atoms (atomic modal propositions). > 3. Introduce the predicate t(w,a) saying which atoms are true in > which possible worlds. > 4. Introduce a predicate k(w,p) saying which propositions > are known in which worlds. > 5. Define MP, the type of all modal propositions, to be the type of > functions from W into P. You didn't define / postulate P yet. But a deeper problem is that I don't see why you let modal propositions be different propositions in different worlds. Why is it not enough that their truth value can be different in different worlds? It also makes it hard for me to see whether this formulation is equivalent withe the above one that it is supposed to capture. > 6. For each atom a, we associate a corresponding element of MP: > p_a == that function f such that f(w) = t(w,a). > 7. Define the operator K as follows: > Kf == that function g such that g(w) = k(w,p) Kf should be Kp? > 8. Define the operator And as follows: > And(f,g) == that function h such that h(w) = f(w) & g(w) > 9. Similarly for Or, Implies, Not > 10. Define the operator <> as follows: > <>f == that function g such that g(w) = exists w':W, f(w') > 11. Define the operator [] as follows: > []f == that function g such that g(w) = forall w':W, f(w') > > >> >Also, I don't understand what you mean by "propositions are actually > >> >functions on world" except that the same proposition can have a > >> >different semantics in different worlds, > > >> That's exactly what I mean. For each modal proposition p > >> (which varies from world to world) we can associate a function > >> f_p from worlds to nonmodal propositions as follows: > > >> f_p(w) == the nonmodal proposition "p is true in world w" > > >> >and that was already taken into account in the old semantics. > > >> Yes. It's the old *syntax* that was inadequate to express a > >> reasonable knowability principle. > > >But until now you have only shown that in the new syntax you can > >express an equivalent one (you can verify that by looking at the model > >theories) and one that's even stronger. > > No, the new "knowability principle" is *not* equivalent. > > Look, once again, I'm formalizing the knowability principle > as: > > forall p:P, p -> exists w:W, k(w,p) In my model theory the semantics of the formula that represented it can be formulated as: (with M being the set/class of valid models) Forall (W,w_1) in M, forall w_2 in W, forall f in F, (W,w_2)||-f -> exists w_3 in W, (W,w_3)||-Kf If you fix W we can simplify this to: (JH-KP) forall w_2 in W, forall f in F, w_2||-f -> exists w_3 in W, w_3||-Kf Doesn't that look similar to you? > I'm formalizing the non-omniscience principle as: > > forall w:W, exists p:P, ~k(w,p) I think you forgot that p has to be true in at least one possible world. And the semantics of the NonO formula in my model theory was: (JH-NonO) forall w in W, exists f in F, w||-f and not w||-Kf Again, quite similar, no? In my model theory JH-KP and JH-nonO lead to a contradiction. As far as I can tell yours is very similar to mine. -- Jan Hidders
From: Daryl McCullough on 4 Jan 2010 11:56
Jan Hidders says... > >On 3 jan, 20:55, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote: >> >But my claim is that you do get a contradiction for the >> >simple reason that your logic contains the old logic. >> >> It doesn't contain the same *axioms*. In particular, I'm >> rejecting the "knowability principle" in favor of a variant >> principle that is (as far as I can see) consistent. > >Well, I'm not so sure. Your new variant look very similar to how the >principle is formulated in my model theory. And there I got the >contradiction. Well, as I said, I don't see how the proof of a contradiction could go through. The variant looks similar to your version, because I *intended* it to be the closest variant that did not lead to the contradiction. The main thing that is different is that in my variant, knowledge is about *non-modal* propositions, rather than modal propositions. The distinction is this: If I say "It is raining", that's a modal statement; it's true in some circumstances and false in others. If I say "It is raining on July 12, 2006 in New York City", then that statement is non-modal. If it is ever true, then it is always true. So my formulation of the principle of knowability is that if a *non-modal* proposition is true, then it is known in some possible world. Now, I can easily come up with statements that make this principle false, as well, using self-reference: "This statement is not known to be true in any possible world" But within the syntax that I'm suggesting, such self-reference isn't obviously possible. >> Let's try to make this more explicit. >> You have a set W of possible worlds, a set MP of >> modal propositions, and for each world w, a set S_w of >> the elements of MP true in world w. The set S_w is constrained >> by the following rules: >> >> 1. If Kp is in S_w, then p is in S_w (you can only know true >> statements) >> 2. And(p,q) is in S_w iff p is in S_w and q is in S_w >> 3. Or(p,q) is in S_w iff p is in S_w or q is in S_w. >> 4. Not(p) is in S_w iff p is not in S_w >> 5. Implies(p,q) is in S_w iff p is not in S_w or q is in S_w >> 6. <>p is in S_w iff for some w', p is in w' >> 7. []p is in S_w iff for all w', p is in w' > >That already looks close enough to a model theory to me. Sorry for the confusion. I'm trying to paraphrase *your* model theory. >A model could >be a pair (W, S) with W the set of possible worlds and S : W -> 2^F >where F is the set of formulas and satisfies the rules 1-7. I strongly >conjecture that those models would be isomorphic to the models in my >formulation of the model theory and lead to the same formulas being >true. That was my intention. >Your mapping to type theory is a bit hard for me to get my head >around, so I'll assume for the moment that the above is your model >theory. > >> Now, to capture this semantics in type theory, we use >> the following translations: >> >> 1. Introduce a type, W, of all possible worlds. >> 2. Introduce a type, A, of all atoms (atomic modal propositions). >> 3. Introduce the predicate t(w,a) saying which atoms are true in >> which possible worlds. >> 4. Introduce a predicate k(w,p) saying which propositions >> are known in which worlds. >> 5. Define MP, the type of all modal propositions, to be the type of >> functions from W into P. > >You didn't define / postulate P yet. P was already introduced in another post. It's the type of all (non-modal) propositions. If you like, you can think of a proposition as a (closed) formula. >But a deeper problem is that I don't see why you let modal propositions >be different propositions in different worlds. I'm trying to model facts that vary from world to world using a logic in which statements have definite truth values. It's no different from using set theory to give a semantics to modal logic. Let's take an example: Plants are green. If there are two worlds, w1 and w2, then "Plants are green in world w1" is a *different* proposition than "Plants are green in world w2". One could be false, while the other could be true. To say "It is possible that plants could be purple" is to say: "exists w:W Plants are purple in world w". The statement "Plants are green" without reference to which world you are talking about is an incomplete proposition. It becomes a proposition when you supply a world w. So it is a function from worlds to propositions. In terms of your syntax: w ||- f I would write this as f(w) Once you've made the world explicit, as is the case with w ||- f you no longer have a modal proposition, but just an ordinary proposition. >Why is it not enough that their truth value can be >different in different worlds? You can think of propositions as truth values, if you like. In a classical logic, there are two propositions, "true" and "false". I'm specifically using a non-classical notion of proposition, in which we *don't* identify statements that have the same boolean truth value because knowledge doesn't work that way. If I know that "Superman is 6 feet tall" that doesn't mean that I know that "Clark Kent is 6 feet tall". >It also makes it hard for me to see whether this formulation is >equivalent withe the above one that it is supposed to capture. >> 6. For each atom a, we associate a corresponding element of MP: >> p_a == that function f such that f(w) = t(w,a). >> 7. Define the operator K as follows: >> Kf == that function g such that g(w) = k(w,p) > >Kf should be Kp? Right. >> Look, once again, I'm formalizing the knowability principle >> as: >> >> forall p:P, p -> exists w:W, k(w,p) > >In my model theory the semantics of the formula that represented it >can be formulated as: (with M being the set/class of valid models) > >Forall (W,w_1) in M, forall w_2 in W, forall f in F, (W,w_2)||-f -> >exists w_3 in W, (W,w_3)||-Kf Yes. I'm claiming that this is *not* a sensible formulation of the knowability principle in the case in which f itself involves the knowability operator K. If f is the formula p & ~Kp, then your principle above gives us: (W,w_2) ||- p & ~Kp -> exists w_3 (W,w_3) ||- K(p & ~Kp) which is a contradiction. The problem is that the knowability principle should not (in my opinion) be about modal propositions. To give the simplest example, suppose p is true in exactly one world. Further, suppose that p is not *known* to be true in that world. In that case, it would be ridiculous to say: Since p is true in one world, then it is known to be true in another world. p *isn't* true in any world, so it can't be known to be true in any other world. But if we deal with nonmodal propositions (propositions of the form w ||- p), then we can certainly have the case that p is true only in world w1, but the *fact* that p is true in world w1 is known in world w2. >If you fix W we can simplify this to: > >(JH-KP) forall w_2 in W, forall f in F, w_2||-f -> exists w_3 in W, >w_3||-Kf > >Doesn't that look similar to you? Similar, but just different enough that your formulation leads to a contradiction, and mine doesn't. My two-place "knowledge" operator acts on *non-modal* propositions. In your syntax, the entire expression (w_2 ||- f) is the nonmodal proposition corresponding to my f(w_2). I would write, instead: forall w_2 in W, forall f in F, w_2 ||- f -> exists w_3 in W, w_3 ||- K(w_2 ||- f) -- Daryl McCullough Ithaca, NY |