Re: Fitch's paradox and OWA

Jan Hidders says...
>
>On 3 jan, 18:32, stevendaryl3..._at_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