Re: Fitch's paradox and OWA

From: Daryl McCullough <>
Date: 2 Jan 2010 07:14:00 -0800
Message-ID: <>

Jan Hidders says...
>On 2 jan, 00:14, (Daryl McCullough) wrote:
>> Jan Hidders says...
>> >Explicit in the formulas? So you really do want to change the syntax?
>> I'm not advocating a change in the syntax, I'm just saying that the
>> syntax of modal logic is inadequate to capture the intuition behind
>> the knowability principle.
>Doesn't that imply that you want to reformulate it in a different

I wouldn't say that I *want* to; I'm just saying that if I wanted to assert the knowability principle, then I would formulate it in something other than modal logic.

>> I would just use first-order logic semantics, and allow explicit
>> quantification over possible worlds. The point about modal logic
>> is that it is a simpler fragment of full first-order logic, but
>> I think that it is not expressive enough to talk about complex
>> issues of necessity and knowability. Fitch's paradox shows its
>> limitations.
>But is that not what the given model theory already does? It uses set
>theory rather then FOL, but since you want to talk about possible
>worlds and statements about statements, that seems more appropriate to
>me anyway.

I don't think the model theory is rich enough. If you are going to allow nested instances of the knowability operator, then there is the issue of *who* knows what. The fact that proposition p is not known in world w1 is itself a proposition, and that proposition can be known, but *not* in w1. Another world, w2 could know that p is not known in w1. But you can't express that without world indices on the knowability operator.

Now, it could be that we are not interested in what *another* world knows about this world. So we restrict our attention to one-world claims (all knowability operators refer to the same world). That's fine, and in that case, the knowability principle is just false in any nontrivial model of modal logic.

>The given model theory still seems to contain the paradox,
>so you will want to change it. Can you show how?

Now that I think about it, it seems that it would be a mess to formalize. The problem is that if knowability is a two-place predicate (as opposed to an operator), then that means that formulas have to serve double-duty: both as formulas and as terms (that can be arguments to the knowability predicate).

In higher-order type theory, I think we can do it this way: Introduce new types

W = the type of possible worlds
A = the type of atomic propositions
P = the type of all propositions

(the propositions are closed under the operations of and, or, implies, negation, universal and existential quantification)

t : W x A --> P
t(w,a) says "a is true in world w"

k : W x P --> P
k(w,p) says "p is known in world w"

Then the knowability principle could be formalized as:

forall p:P, (p -> exists w:W, k(w,p))

(any true proposition is known to be true in some world).

I think it would be a lot of work to nail down all the details here, but my point is that the knowability principle can be formulated in a way that isn't susceptible to Fitch's proof.

Daryl McCullough
Ithaca, NY
Received on Sat Jan 02 2010 - 16:14:00 CET

Original text of this message