Jan Hidders says...

Yes, but with the correct axiomatization of knowability
predicate, the corresponding proposition will not be true.

I don't see how it is a paradox. Your proposition (3) will
(with the appropriate axiomatization of the knowability
predicate) be provably false.

The only reason in the original proof of Fitch's paradox
to believe (1) (the claim K(p & ~K(p))) is because it follows
from the knowability principle and the principle of non-omniscience.
In the logic that I sketched, I don't believe it follows from
those.

1. Knowability principle: forall p:P, p -> exists w:W (k(w,p))
2. Non-omniscience principle: forall w:W, exists p:P, p & ~k(w,p)

Your statement (3) above does not follow from my 1. and 2. At least,
I don't see how.

--
Daryl McCullough
Ithaca, NY

In article <46afa0f9-e70d-4d21-bf67-7f49cd16bf32 (AT) 21g2000yqj (DOT) googlegroups.com>,
vldm10 says...
In the higher-order type theories that I know of, the liar is not
expressible (which is good, since it would lead to a contradiction).

--
Daryl McCullough
Ithaca, NY

On 2 jan, 22:52, stevendaryl3... (AT) yahoo (DOT) com (Daryl McCullough) wrote:
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. If your logic is complete it will also have the
equivalents of all the used axioms and principles, and so the proof
will still proceed but will just be phrased in a different syntax.

For example, on the Stanford page the formulas (4) and (5) both have
their equivalents in your logic. You should also have the principle
(A) in your logic, but of course translated to your syntax, so in your
logic we should be able to derive the equivalent of (5) from the
equivalent of (4). Et cetera.

-- Jan Hidders

Jan Hidders says...

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)

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.

Yes, but I'm *rejecting* the knowability principle in favor of
a more sensible (non-contradictory) principle. I'm suggesting
a *different* principle, one that *doesn't* lead to a contradiction.

--
Daryl McCullough
Ithaca, NY

On Jan 2, 10:57*pm, stevendaryl3... (AT) yahoo (DOT) com (Daryl McCullough)
wrote:
I guess that some objects can be treated as types if they have some
characteristics in common. We expect the propositions which will have
same properties of concern to logic, i.e. propositions are types.
This is not the case with Liar paradox.
The liar paradox contains a sort of self-reference and the predicate
‘- is true’ and it is applied to name its own sentences.
This paradox is important, for example “in proving the first
incompleteness theorem, Gödel used a slightly modified version of the
liar's paradox”
(see at http://en.wikipedia.org/wiki/Liar_paradox )

There are self-references without predicates ‘- is true’. Let me give
you two examples which are related to other kind of the self-
reference:

Example1.
Here we have two sentence:

Tom is a mathematician. Tom is a mathematician.

They have the same truth value in any model.



Example 2.
I have two sheets of paper. One is marked with P1 and another with P2.
I will put the following sentence into every of the paper:

The sentence which is on paper P1 have red letters.

So on each of the mentioned paper there is the same sentences and
nothing else.
However semantically these sentences are not the same.

(These examples are inspired from the following two books:
John Burdian on Self-Reference by Hughes, G.E;
Classical Mathematical Logic by R.L. Epstein)

It is interesting to find models for the proposition that contains
self-referencing.
Regarding abstract objects it is also interesting the following
question: Can the propositions come to an existence and cease to
exist?

Vladimir Odeljin

On 3 jan, 14:09, stevendaryl3... (AT) yahoo (DOT) com (Daryl McCullough) wrote:
Er, I think you forgot the part where it requires that p is true. 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.

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.

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, and that was already taken
into account in the old semantics.

-- Jan Hidders

Jan Hidders says...
Right. Thanks.

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*.

Right. It's *too* strong, which is why it leads to a contradiction
(together with the principle of non-omniscience).

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"

Yes. It's the old *syntax* that was inadequate to express a
reasonable knowability principle.

--
Daryl McCullough
Ithaca, NY

On 3 jan, 18:32, stevendaryl3... (AT) yahoo (DOT) com (Daryl McCullough) wrote:
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.

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?

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

Jan Hidders says...
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.

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.


It certainly does. It's just a translation of the principle
into a more expressive logic.

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')

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

Jan Hidders says...
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.

Sorry for the confusion. I'm trying to paraphrase *your*
model theory.

That was my intention.

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.

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.

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".

Right.

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.


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