Fitch's paradox and OWA
Nilone
assumption?
Jan Hidders
> Does Fitch's paradox prove an inherent contradiction in the open-world
> assumption?
Only if you assume that the database contains everything that is
known. It rarely does. :-)
Besides, do you really believe that everything that is true can be
known? ;-)
-- Jan Hidders
paul c
Heh... not to mention vice-versa, the chronic slant of so many!
Daniel Pitts
> Does Fitch's paradox prove an inherent contradiction in the open-world
> assumption?
disproved it somewhat with his theorem.
G�del theorem proves that in any system of sufficient reasoning power,
there are truths about the system which can not be derived from within
the system. There is no contradiction, unless your truths somehow
include "all truths are provable", which is close to what Fitch has said.
Actually, it could be that Fitch simply proved that a knowable truth is
knowable, when he intended to prove something else.
--
Daniel Pitts' Tech Blog: <http://virtualinfinity.net/wordpress/>
Gene Wirchenko
A segue to the continuum hypothesis?
Sincerely,
Gene Wirchenko
Nilone
"All truths are known" is only problematic if you assume that truth
exists independent of cognition. From a phenomenalistic point of
view, both entities and predicates exist purely in the mind, which
means that all truths are known, but doesn't exclude the possibility
of creating new truths based on sense data. I'm currently leaning in
this direction (in the sense that Mach espoused), especially after
coming across relational quantum mechanics.
But I'm getting off-topic here. It seems to me now that Fitch's
paradox just illustrates the distinction between OWA and CWA formally.
paul c
To be more clear/blunt, in the context of the RM, D&D have it that it is
a value of the relation that has no attributes. This may seem obscure
in general language, but in the db machine context it is much
simpler/clearer than the above.
Nilone
A relation with no attributes is a simple proposition, so you're
saying the chosen assumption is a value in the db, right? I prefer
this, although TTM states they subscribe to CWA.
Is it necessarily a db-wide choice, or could it be useful to
distinguish the choice per relation?
Jan Hidders
> On Dec 16, 11:09 pm, Jan Hidders <hidd...@gmail.com> wrote:
>
> > On 16 dec, 12:07, Nilone <rea...@gmail.com> wrote:
>
> > > Does Fitch's paradox prove an inherent contradiction in the open-world
> > > assumption?
>
> > Only if you assume that the database contains everything that is
> > known. It rarely does. :-)
>
> > Besides, do you really believe that everything that is true can be
> > known? ;-)
>
> exists independent of cognition.
Which in my world view it is. It's positively weird to say that
Fermat's last theorem was not true until a proof was found. If you
want to do so, be my guest, but I'd argue you would be using another
definition of truth than I am.
-- Jan Hidders
Nilone
Good point. I'm not sure that's what I want to say, either. I'll
give it some more thought.
Reinier Post
>Does Fitch's paradox prove an inherent contradiction in the open-world
>assumption?
I don't understand the paradox.
http://plato.stanford.edu/entries/fitch-paradox/
explains:
suppose that
(KP) all truths are knowable, i.e. can be known by somebody at some time
and
(NonO) not all truths are known now
then
(1) there is an unknown truth p
and then
(2) p is true and unknown is itself a truth
and hence, by KP,
(3) (p is true and unknown) can be known by somebody at some time
"However, it can be shown independently that it is impossible
to know this conjunction. Line 3 is false."
I'm eager to see that demonstration. Clearly, if p is unknown (1),
then so is the truth than p is true and unknown (2), but KP doesn't
contradict that - all it says is that p may be known, perhaps at some
other time, and indeed, at that same time, the statement that p was true
but unknown will also be known to be true.
They seem to mess up the scoping of K and P, simplifying their language
until paradoxes become inevitable; the paradox results from that,
as far as I can see. In any case, the paradox depends
on the exact formalization on K and P, which isn't given.
Once again, I'm left with the feeling that these Stanford guys
could use some field experience in database design.
--
Reinier
Mr. Scott
"Reinier Post" <r...@raampje.lan> wrote in message
news:4b2ab63e$0$28714$703f...@news.kpn.nl...
> Nilone wrote:
>
>>Does Fitch's paradox prove an inherent contradiction in the open-world
>>assumption?
>
> I don't understand the paradox.
>
> http://plato.stanford.edu/entries/fitch-paradox/
>
> explains:
>
> suppose that
>
> (KP) all truths are knowable, i.e. can be known by somebody at some time
>
> and
>
> (NonO) not all truths are known now
>
> then
>
> (1) there is an unknown truth p
>
> and then
>
> (2) p is true and unknown is itself a truth
>
> and hence, by KP,
>
> (3) (p is true and unknown) can be known by somebody at some time
>
> "However, it can be shown independently that it is impossible
> to know this conjunction. Line 3 is false."
>
Your addition of 'now' to (NonO) is the cause of your confusion. Go back
and re-read what you cited.
If K is the epistemic operator meaning 'it is known by someone at some time
that,' then not K would have to deny that, meaning 'it is not known by
anyone at any time that,' so with that in mind....
(KP) forall p(p implies possibly Kp): all truths are knowable by somebody at
some time.
(NonO) exists p(p and not Kp): there is a truth that is not known by anybody
at any time.
These are contradictory. If all truths are knowable by somebody at some
time then there can't be a truth that is not known by anybody at any time.
Reinier Post
>
>"Reinier Post" <r...@raampje.lan> wrote in message
>news:4b2ab63e$0$28714$703f...@news.kpn.nl...
>> Nilone wrote:
>>
>>>Does Fitch's paradox prove an inherent contradiction in the open-world
>>>assumption?
>>
>> I don't understand the paradox.
>>
>> http://plato.stanford.edu/entries/fitch-paradox/
>>
>> explains:
[...]
>Your addition of 'now' to (NonO) is the cause of your confusion. Go back
>and re-read what you cited.
I just did.
>If K is the epistemic operator meaning 'it is known by someone at some time
>that,' then not K would have to deny that, meaning 'it is not known by
>anyone at any time that,' so with that in mind....
Yes indeed, that's how they define K ... I should have seen that
the first time around. Thank you.
>(KP) forall p(p implies possibly Kp): all truths are knowable by somebody at
>some time.
>
>(NonO) exists p(p and not Kp): there is a truth that is not known by anybody
>at any time.
>
>These are contradictory. If all truths are knowable by somebody at some
>time then there can't be a truth that is not known by anybody at any time.
Now, the contradiction is direct: KP says that all
truths are knowable while NonO says that some truth isn't.
There is no paradox, just a contradiction.
But that's not how NonO is introduced:
| And suppose that collectively we are non-omniscient, that there is an unknown truth:
|
| (NonO) ∃p(p ∧ ¬Kp).
See: here they say 'unknown', not 'unknowable'. Hence my confusion.
Once it's merely 'unknown' I believe the scoping issue arises.
--
Reinier
Mr. Scott
"Reinier Post" <r...@raampje.lan> wrote in message
>
> See: here they say 'unknown', not 'unknowable'. Hence my confusion.
> Once it's merely 'unknown' I believe the scoping issue arises.
>
Now I'm getting confused. I agree that there is something that doesn't sit
right: it doesn't make sense for something being knowable to imply that it
is known, or for something being unknown to imply that it is unknowable.
But supposing that (NonO) is true throws a wrench into the works. If one
supposes that there is a truth that is not known by anybody at any time,
then it is necessary that there is a truth that is not known by anybody at
any time, and that if it is necessary that there is a truth that is not
known by anybody at any time, then it is not possible for that truth to be
known by somebody at some time. On the page you cited, these are instances
of lines (C) and (D), respectively. When something is actually true, it is
necessary that it is possible, but when something is supposed to be true, it
is necessary that it is not just possible but true.
Jan Hidders
>
> > See: here they say 'unknown', not 'unknowable'. Hence my confusion.
> > Once it's merely 'unknown' I believe the scoping issue arises.
>
> Now I'm getting confused. I agree that there is something that doesn't sit
> right: it doesn't make sense for something being knowable to imply that it
> is known, or for something being unknown to imply that it is unknowable.
> But supposing that (NonO) is true throws a wrench into the works. If one
> supposes that there is a truth that is not known by anybody at any time,
> then it is necessary that there is a truth that is not known by anybody at
> any time, and that if it is necessary that there is a truth that is not
> known by anybody at any time, then it is not possible for that truth to be
> known by somebody at some time. On the page you cited, these are instances
> of lines (C) and (D), respectively. When something is actually true, it is
> necessary that it is possible, but when something is supposed to be true, it
> is necessary that it is not just possible but true.
I agree with Reinier that there is a scoping issue here that causes
the strange conclusion. Since the logic includes the notion of
"possible" we need to take into account that the model theory changes
and therefore also what it means for a proposition represented by a
formula to be true. In the setting of the paradox the truth of a
formula is necessarily defined wrt. to a model that describes all
possible situations, or "the set of all possible worlds" as it is
usually called. For example, <>f means that in at least one possible
world f holds, and []f means that it holds in all possible worlds. As
usual a proposition is assumed to be true iff it holds in all possible
worlds. If it holds in only some possible worlds it is assumed to be
only possibly true.
So what happens to the paradox if we take that into account? Let's
look at what KP says:
KP: For all propositions p it holds that if p is true in all possible
worlds then there is at least one possible world in which it is known.
(NOTE1: That is actually not what the formula on the Stanford page
says. It has the meaning "In all possible worlds it holds that if p is
true in that world then there a possible world in which p is known."
which is a slightly stronger statement.)
And NonO:
NonO: There is a proposition p such that it holds in all possible
worlds but is not known in any of them.
(NOTE2: Also here the formula in the Stanford page says something
subtly different: "In all possible worlds there is a formula p that is
true in that world but not known in that world." This is actually a
weaker statement and does not contradict KP. The formula should have
said: Exists p ([]p -> []~Kp). )
It will be clear that KP and NonO as I've stated them immediately
contradict each other. The reasoning of the paradox now proceeds as
follows: if you accept KP then you cannot accept NonO and therefore
must accept it's negation. Fair enough. Let's write this negation
down:
NotNonO: There is no proposition p such that it holds in all possible
worlds but is not known in any of them.
Or, equivalently:
NotNonO2: For all propositions p it holds that if it holds in all
possible worlds then it is known in at least one possible world.
But wait! Did we not see that before? Of course we did, this is
exactly KP. So basically what we have concluded until now is that if
you accept KP then you also accept KP. At least it has the benefit of
being very probably correct. :-)
Anyway, on with the reasoning of the paradox. How does it proceed from
NotNonO? If you look on the Stanford page you see that this is
formulated in formula (10). But what this formula says is:
StanfordNotNonO: In all possible worlds there is no proposition p that
holds in that world and is not known in that world.
But this is of course very different NotNonO, which is what it should
have said.
-- Jan Hidders
Jan Hidders
Summary:
In a possible-worlds setting (which you have to be in if you talk
about "possible" and "necessary") the inference rule "reductio ad
absurdum" is not always valid, i.e., you cannot conclude from the
observation that "the assumption of P leads to a contradiction" that
~P.
The reason for this is very simple. The truth of P means in a possible-
worlds setting that P is true in all possible worlds, i.e., it is a
necessary truth. So if the assumption of P leads to a contradiction
then we can conclude that P is not a necessary truth, but *not* that P
is necessarily false. In other words, if P (or equivalently, []P)
leads to a contradiction then we can conclude that ~[]P (or
equivalently, <>~P) but not that []~P.
Without the "reductio ad absurdum" inference rule we cannot derive
proposition (10) on the Stanford page and the chain of inference of
the paradox is broken.
Fitch's paradox is no more. :-)
-- Jan Hidders
Marshall
From plato.stanford.edu:
"As for the knowability proof itself, there continues to be no
consensus on whether and where it goes wrong."
So ... you gonna publish that? Give those modal logic guys
a kick in the pants? :-)
Marshall
Jan Hidders
Only after checking carefully whether I'm right. :-) Unfortunately it
turns out that I was wrong. But in the process I did find what I think
is really the problem with the paradox.
You can "check" the reasoning by writing down a model theory for the
logic and see if all the inferences are actually valid there. In this
case the model theory is a bit more complicated than usual because we
are reasoning about possible worlds.
Basically a model will now look like a pair (W,w) where W is the set
of all possible worlds and w is the world we are in right now which
must of course be an element of W. In normal propositional logic a
single world is described by the set of true atomic propositions. In
the setting of the paradox it also contains propositions of the form
Kf where f is some formula, which say that f is known in that world. I
will call those atomic propositions and Kf propositions collectively
basic propositions.
So a world could for example be {a, b, Ka} where a and b are true, but
only a is actually known. A complete model could for example be ({w1,
w2, w3}, w1) where w1 = {a,b,Ka}, w2 = {a,Ka} and w3 = {b,Kb}.
For normal logic operators the model theory is straightforward:
- (W,w) |- f1 & f2 iff (W,w) |- f1 and (W,w) |- f2
- (W,w) |- ~f1 iff not (W,w) |- f1
etc.
For the basic proposition and the K-facts:
- (W,w) |- a iff a in w
- (W,w) |- Kf iff Kf in w
For the modal operators:
- (W,w) |- []f iff (W,w') |- f for all w' in W
- (W,w) |- <>f iff (W,w') |- f for some w' in W
It can be verified that in this model theory all the inference steps
used in the paradox are always valid. For the assumptions (A), (B),
(C) and (D) on the Stanford page <http://plato.stanford.edu/entries/
fitch-paradox/> it holds that (D) is always valid in the above model
theory. So we can question the validity of (A), (B) and (C). As it
turns out (I will not explain that here) you don't need (A) and (B)
to get the result of the paradox, so I'm going to focus on (C).
If we reformulate the meaning of (C) in the model theory we get:
(mC) If (W,w) |- f then (W,w) |- []f.
Given the semantics of []f this is equivalent with:
(mC') If (W,w) |- f then (W,w') |- f for all w' in W.
Note that in particular this will hold for f's that are basic
propositions or negations of basic propositions. Since the basic
propositions hold for (W,w') iff they are elements of w', and their
negation only holds if they are not elements of w', it follows that w
and w' must always contain exactly the same elements, and therefore in
fact be the same world. In other words, (C) says effectively that
there is always only one possible world. Knowing this, it is not
surprising we get such unintuitive results, because it means that
everything that is possible, i.e., true in one of the possible worlds,
is actually necessary, i.e., true in all possible worlds. This also
explains how, from the assumption that every truth is possibly known,
we can come to the conclusion that every truth is necessarily known.
Conclusion: axiom (C) is not a modest modal assumption at all, and in
fact quite absurd.
-- Jan Hidders
Daryl McCullough
>If we reformulate the meaning of (C) in the model theory we get:
>
>(mC) If (W,w) |- f then (W,w) |- []f.
>
>Given the semantics of []f this is equivalent with:
>
>(mC') If (W,w) |- f then (W,w') |- f for all w' in W.
I don't think that that is correct. Rule (C) says that
if p is a *theorem* (that is, p is provable) then it is
necessarily true (and so is true in all worlds).
In Kripke semantics, we distinguish between what is true
in one world and what is provable. So you should be writing
(W,w) ||- f
to mean f is true in world w (where W is the set of all possible
worlds) instead of
(W,w) |- f
I'm not sure what the latter would mean.
--
Daryl McCullough
Ithaca, NY
Daryl McCullough
don't have any problems with the paradox, because I don't
accept the premise: Every true proposition is potentially knowable.
It seems to me that sufficiently complex true propositions may never
be known. Certainly there are candidate mathematical truths, such
as Goldbach's conjecture, that we have no idea how to ever prove,
so it seems plausible (to me) that we may never come to know that
they are true.
Nam Nguyen
> By the way, I haven't thought about it a huge amount, but I
> don't have any problems with the paradox, because I don't
> accept the premise: Every true proposition is potentially knowable.
> It seems to me that sufficiently complex true propositions may never
> be known.
But how can we know it's true in the first place, when its being true
can't be known?
> Certainly there are candidate mathematical truths, such
> as Goldbach's conjecture, that we have no idea how to ever prove,
> so it seems plausible (to me) that we may never come to know that
> they are true.
Let me add more to what you've said.
One of the shortcomings of modern mathematical logic is that it assumes
every single formula written in the language of arithmetic "must be"
arithmetically either true or false.
There is a class of formulas (written in the language) whose arithmetic
truths or falsehoods can't be established as a matter of principle. [The
existence of this class could be demonstrated]. GC and the formula "There
are infinite counter examples of GC" are candidates of being in such class.
Marshall
>
> One of the shortcomings of modern mathematical logic is that it assumes
> every single formula written in the language of arithmetic "must be"
> arithmetically either true or false.
If it's actually the case (that every statement of basic arithmetic
is either true or false) then it's not a shortcoming to say so.
On the contrary, that would be a virtue.
Do you have any reason to believe that there exist statements
of arithmetic that *don't* fall in to one of those two categories?
Note that not being able to know which one it is is not the same
thing as it actually being something other than true or false.
(I'm guessing you actually disagree with that last sentence,
though.)
Marshall
Daryl McCullough
>
>Daryl McCullough wrote:
>> By the way, I haven't thought about it a huge amount, but I
>> don't have any problems with the paradox, because I don't
>> accept the premise: Every true proposition is potentially knowable.
>
>> It seems to me that sufficiently complex true propositions may never
>> be known.
>
>But how can we know it's true in the first place, when its being true
>can't be known?
I didn't say that we can *know* it is true. That's my point---something
can be true without anyone knowing that it is true. It might be true,
for example, that there is an even number of grains of sand in the world, but we
may never find that out. Is e^pi rational? We may never find out.
Marshall
wrote:
I believe Nam is roughly of the opinion that if we can't know which
one of {true, false} a sentence is, then we have no basis for saying
it must be one or the other. I seem to recall being less than
completely
clear on that point myself sometime in the past, in re the halting
problem, and getting a sound sci.logic thrashing by some guy
as a result. His name was Darren McColor, or anyway it was
something like that. Boy was I embarrassed!
Marshall
Barb Knox
<e3cb76b6-8d77-4a92...@k17g2000yqh.googlegroups.com>,
Marshall <marshal...@gmail.com> wrote:
> On Dec 30, 6:22�pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >
> > One of the shortcomings of modern mathematical logic is that it assumes
> > every single formula written in the language of arithmetic "must be"
> > arithmetically either true or false.
By the nature of the construction of predicate logic, every arithmetic
formula must be either true or false in the standard model of the
natural numbers.
But, we have no satisfactory way to fully characterise that standard
model! We all think we know what the natural numbers are, but Goedel
showed that there is no first-order way to define them, and I don't know
of *any* purely formal (i.e., syntactic) way to do do. (The usual ways
to define them are not fully syntactic, but rely on "the full semantics"
of 2nd-order logic, or "a standard model" of set theory, both of which
are more complicated than just relying on "the Standard Model" of
arithmetic in the first place.)
So, we can say we have a fully-pinned-down notion of arithmetical truth,
but only in terms of a background (the Standard Model) which we can't
fully pin down.
> If it's actually the case (that every statement of basic arithmetic
> is either true or false) then it's not a shortcoming to say so.
> On the contrary, that would be a virtue.
Speaking philosophically (since I'm posting from sci.philoisophy.tech),
entities which in some sense exist but are thoroughly inaccessible seem
to be of little value. This applies to the truth values of any
statements which can never be known to be true or false.
> Do you have any reason to believe that there exist statements
> of arithmetic that *don't* fall in to one of those two categories?
> Note that not being able to know which one it is is not the same
> thing as it actually being something other than true or false.
>
> (I'm guessing you actually disagree with that last sentence,
> though.)
>
>
> Marshall
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum videtur.
| BBB aa a r bbb |
-----------------------------
Nam Nguyen
> On Dec 30, 6:22 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> One of the shortcomings of modern mathematical logic is that it assumes
>> every single formula written in the language of arithmetic "must be"
>> arithmetically either true or false.
>
> If it's actually the case (that every statement of basic arithmetic
> is either true or false) then it's not a shortcoming to say so.
> On the contrary, that would be a virtue.
It _would_ be a virtue, yes, but only, as you said, "_If_ it's actually
the case"! But is it?
>
> Do you have any reason to believe that there exist statements
> of arithmetic that *don't* fall in to one of those two categories?
Yes. There are statements written in the lanaguage of arithmetic that
no one could possibly assign a truth value to them. For example:
(1) There are infinite counter examples of GC.
Tell me what you'd even suspect as a road-map to assign true or false to (1)?
> Note that not being able to know which one it is is not the same
> thing as it actually being something other than true or false.
Similarly as in provably-undecidable case (though not identical), there's
a 3rd scenario: you can't assign arithmetic truth or falsehood a a certain
formula, and in which case the formula is neither true or false! (Of course
in such case you could assume it's true or false - but not both - at will.)
>
> (I'm guessing you actually disagree with that last sentence,
> though.)
Of course. But I've also cited reasons.
Daryl McCullough
>I believe Nam is roughly of the opinion that if we can't know which
>one of {true, false} a sentence is, then we have no basis for saying
>it must be one or the other.
But typically, for some statements such as "The Greek philosopher
Plato was left-handed" I don't know whether the statement is true
or not, and I also don't know whether anyone else knows whether it
is true or not, and I don't know whether it is *possible*, at this
late date, to find out whether it is true or not. But surely, it's
either true or false, right?
Nam Nguyen
No. Not surely. Since by our assumption here is nobody would know about
his handed-ness, his nervous system to both arms might not have functioned
at all to begin with and hence whether or not he was left-handed is moot
and is not-truth assignable. As well, there are people are strong equally
on both arms and therefore handed-ness is not applicable to them.
Nam Nguyen
Don't want to beat a dead horse so to speak but not knowing a truth because
its proof (knowledge) is _finitely_ larger than what one can possibly know
is *not* the same as not knowing a truth value because the statement is not
*genuinely* truth-assigned-able. The "sand in the world" being an even number
example above is of the 1st kind: not the 2nd kind.
Bob Badour
The term is ambidextrous and ambidextrous is not left-handed so the
predicate would be false if that were the case.
It doesn't get tricky until handedness is equally strong in both arms
but not for the same things like a person who writes left-handed but
shoots right-handed etc.
--
is there something in it for them, like maybe bailouts, if they can
panic us into doing something politically to cover them?
November 19, 2007 - John S Bolton
Nam Nguyen
> Nam Nguyen wrote:
>
>> Daryl McCullough wrote:
>>
>>> Marshall says...
>>>
>>>> I believe Nam is roughly of the opinion that if we can't know which
>>>> one of {true, false} a sentence is, then we have no basis for saying
>>>> it must be one or the other.
>>>
>>> But typically, for some statements such as "The Greek philosopher
>>> Plato was left-handed" I don't know whether the statement is true
>>> or not, and I also don't know whether anyone else knows whether it
>>> is true or not, and I don't know whether it is *possible*, at this
>>> late date, to find out whether it is true or not.
>>
>>> But surely, it's either true or false, right?
>>
>> No. Not surely. Since by our assumption here is nobody would know about
>> his handed-ness, his nervous system to both arms might not have
>> functioned
>> at all to begin with and hence whether or not he was left-handed is moot
>> and is not-truth assignable. As well, there are people are strong equally
>> on both arms and therefore handed-ness is not applicable to them.
>
> The term is ambidextrous and ambidextrous is not left-handed so the
> predicate would be false if that were the case.
The _analogy_ was under the assumption that we'd logically live under a binary
world where the negation of "left-handed" is "right-handed". I don't think we
were arguing about precise meanings of biological/physiological matters.
My point still stands: if it's _impossible_ (as opposed to just being difficult)
to assign truth values to a formula then the formula is neither true nor false,
which means that collectively the naturals isn't a _complete_ model of Q or its
extensions.
Jan Hidders
> Jan Hidders says...
>
> >If we reformulate the meaning of (C) in the model theory we get:
>
> >(mC) If (W,w) |- f then (W,w) |- []f.
>
> >Given the semantics of []f this is equivalent with:
>
> >(mC') If (W,w) |- f then (W,w') |- f for all w' in W.
>
> I don't think that that is correct. Rule (C) says that
> if p is a *theorem* (that is, p is provable) then it is
> necessarily true (and so is true in all worlds).
My apologies. Everywhere where I wrote (W,w) |- f I actually meant
(W,w) ||- f.
So what I wanted to say with the above is the following. You are of
course right that what (C) really says is:
(C) if |- f then |- []f
And, assuming that for all f it holds that |- f iff ||- f, this is in
fact confirmed by the model theory. However, in the inference process
of the paradox as described on the Stanford page the rule is used as
if it says f |- []f or |- f->[]f, and that would have the much
stronger model-theoretic meaning that I described.
Their reasoning can be simplified to this:
(1) p & ~Kp (assumption, for arbitrary variable p)
(2) <>Kp (from (1) using KP)
(3) []~Kp (from (1) using (C))
(4) ~<>Kp (from (3) using (D)
(5) ~(p & ~Kp) (from (1) and contradicting (2) and (4))
(6) Forall p (~(p & ~Kp)) (forall introduction)
(7) Forall p (p -> Kp) (propositional reasoning)
The error in the reasoning is caused by the omission of |- before each
formula. If you add that, it is clear that at step (5) it is concluded
erroneously that |- ~(p & ~Kp) but it should have said that "it is not
true that |- (p & ~Kp)", which is of course not the same thing.
-- Jan Hidders
Daryl McCullough
>So what I wanted to say with the above is the following. You are of
>course right that what (C) really says is:
>
>(C) if |- f then |- []f
>
>And, assuming that for all f it holds that |- f iff ||- f, this is in
>fact confirmed by the model theory. However, in the inference process
>of the paradox as described on the Stanford page the rule is used as
>if it says f |- []f or |- f->[]f, and that would have the much
>stronger model-theoretic meaning that I described.
I don't see a rule saying f |- []f. Where did you see that?
I don't think that's a sensible modal logic rule. That is
essentially saying that there is no difference between
f and []f. (Usually, the accessibility relation on worlds
is set up so that []f -> f. So if we add f -> []f, then
f and []f are logically equivalent.)
>Their reasoning can be simplified to this:
>
>(1) p & ~Kp (assumption, for arbitrary variable p)
>(2) <>Kp (from (1) using KP)
>(3) []~Kp (from (1) using (C))
No, we don't have |- ~Kp. We only have (W,w) ||- ~Kp.
So we can't conclude |- []~Kp.
Daryl McCullough
That was my point. There can be statements that are true, but which
we will never know that they are true. There can also be statements
that are true, but which we have no way of ever knowing that they are
true. For example, I flip a coin, and before I see whether it lands
heads up or tails up, it is run over by train, smashing it into a
flat, smooth chip of metal. Now, there is no way of ever knowing
whether it was heads-up or tails-up. But it is possible that
"It was heads-up before it was smashed" is true.
Statements can be true even if there is no way to ever know that they
are true.
--
Daryl McCullough
Ithaca, NY
Daryl McCullough
>
>Daryl McCullough wrote:
>> Marshall says...
>>
>>> I believe Nam is roughly of the opinion that if we can't know which
>>> one of {true, false} a sentence is, then we have no basis for saying
>>> it must be one or the other.
>>
>> But typically, for some statements such as "The Greek philosopher
>> Plato was left-handed" I don't know whether the statement is true
>> or not, and I also don't know whether anyone else knows whether it
>> is true or not, and I don't know whether it is *possible*, at this
>> late date, to find out whether it is true or not.
>
>
>> But surely, it's either true or false, right?
>
>No. Not surely. Since by our assumption here is nobody would know about
>his handed-ness, his nervous system to both arms might not have functioned
>at all to begin with and hence whether or not he was left-handed is moot
>and is not-truth assignable.
Well, it is certainly *possible* that "Plato was left-handed" is a statement
that is both true and unknowable (at this late date).
Marshall
> Nam Nguyen wrote:
> > Daryl McCullough wrote:
> >> Marshall says...
>
> >>> I believe Nam is roughly of the opinion that if we can't know which
> >>> one of {true, false} a sentence is, then we have no basis for saying
> >>> it must be one or the other.
>
> >> But typically, for some statements such as "The Greek philosopher
> >> Plato was left-handed" I don't know whether the statement is true
> >> or not, and I also don't know whether anyone else knows whether it
> >> is true or not, and I don't know whether it is *possible*, at this
> >> late date, to find out whether it is true or not.
>
> >> But surely, it's either true or false, right?
>
> > No. Not surely. Since by our assumption here is nobody would know about
> > his handed-ness, his nervous system to both arms might not have functioned
> > at all to begin with and hence whether or not he was left-handed is moot
> > and is not-truth assignable. As well, there are people are strong equally
> > on both arms and therefore handed-ness is not applicable to them.
>
> The term is ambidextrous and ambidextrous is not left-handed so the
> predicate would be false if that were the case.
>
> It doesn't get tricky until handedness is equally strong in both arms
> but not for the same things like a person who writes left-handed but
> shoots right-handed etc.
Bob,
Nam is a kook; you can safely ignore anything he says.
Marshall
PS. Ah, the years of history! Too bad no one on sci.logic will get it.
Daryl McCullough
the conclusion that Fitch's paradox is invalid. Or perhaps the
statement of the knowability principle is wrong.
Here's the proof of the contradiction:
1. (Knowability principle) For all p: p -> <> K(p)
where <>Phi means "Phi is possibly true" and K(Phi) means
"Phi is known".
2. (Non-omniscience principle) For some p: p & ~K(p)
3. Letting p0 be the true but unknown proposition, we have
p0 & ~K(p0)
4. From 1&3, we have <>K(p0 & ~K(p0))
At this point, let me switch to possible world semantics: <> Phi
means "Phi is true in some world". So let's switch to the world
in which K(p0 & ~K(p0)) is true. In that world we have
5. K(p0 & ~K(p0))
From this it follows:
6. K(p0) & K(~K(p0))
But only true things are knowable, so from K(~K(p0)) it
follows that ~K(p0). So we have
7. K(p0) & ~K(p0)
which is a contradiction.
The mistake becomes clearer if we explicitly introduce
possible worlds. Let's use w ||- Phi to mean "Phi is true
in world w" and K_w(Phi) to mean "Phi is known in world
w". Let's introduce w0 to mean "our world". Then the
proof becomes the following:
1. (Knowability principle) for all p: (w0 ||- p) -> exists w, K_w(p)
In other words, if p is true in our world, then there exists another
world in which p is knowable.
2. (Non-omniscience principle) for some p: w0 ||- p & ~K_w0(p)
3. Introducing the constant p0 for this unknown proposition, we
have: w0 ||- p0 & ~K_w0(p0)
4. From 1&3, we have exists w, K_w(p0 & ~K_w0(p0))
5. Letting w' be a name for some world making the existential true,
we have: K_w'(p0 & ~K_w0(p0))
From this it follows:
6. K_w'(p0) & K_w'(~K_w0(p0))
Since only true things are knowable, we have:
7. K_w'(p0) & ~K_w0(p0)
That's no contradiction at all! The proposition p0 is
known in one world, w', but not in another world, w0.
It only becomes a contradiction when you erase the
world suffixes.
Marshall
wrote:
> Jan Hidders says...
>
> >So what I wanted to say with the above is the following. You are of
> >course right that what (C) really says is:
>
> >(C) if |- f then |- []f
>
> >And, assuming that for all f it holds that |- f iff ||- f, this is in
> >fact confirmed by the model theory. However, in the inference process
> >of the paradox as described on the Stanford page the rule is used as
> >if it says f |- []f or |- f->[]f, and that would have the much
> >stronger model-theoretic meaning that I described.
>
> I don't see a rule saying f |- []f. Where did you see that?
He didn't say that there was an explicitly stated rule of
that form. He said that in step 8 of the derivation, they
use a rule that was explicitly stated as
If |- f then |- []f
but they use it *as if* the rule was
f |- []f
Reading that page, it looks like what he is saying accurately
describes the step taken, but I know very little about
modal logic.
> I don't think that's a sensible modal logic rule.
That's his point, as I understand it.
Marshall
Marshall
>
> My point still stands: if it's _impossible_ (as opposed to just being difficult)
> to assign truth values to a formula then the formula is neither true nor false,
Your point is still wrong.
> which means that collectively the naturals isn't a _complete_ model of Q or its
> extensions.
Your conclusion is also still wrong, unsurprisingly.
Marshall
Marshall
> Marshall <marshall.spi...@gmail.com> wrote:
>
> By the nature of the construction of predicate logic, every arithmetic
> formula must be either true or false in the standard model of the
> natural numbers.
>
> But, we have no satisfactory way to fully characterise that standard
> model! We all think we know what the natural numbers are, but Goedel
> showed that there is no first-order way to define them, and I don't know
> of *any* purely formal (i.e., syntactic) way to do do.
I was more under the impression that Goedel showed there
was no complete finite theory of them, rather than no
way to define them. Are you saying those are equivalent?
> (The usual ways
> to define them are not fully syntactic, but rely on "the full semantics"
> of 2nd-order logic, or "a standard model" of set theory, both of which
> are more complicated than just relying on "the Standard Model" of
> arithmetic in the first place.)
Here's a possible definition:
nat := 0 | succ nat
x + 0 = x
x + succ y = succ x+y
x * 0 = 0
x * succ y = x + (x * y)
Is there some way this definition is not fully syntactic?
It uses no quantifying over predicates, so it can't be
using second order logic.
It certainly seems to me that the above is fully syntactic,
and is a complete definition of basic arithmetic. Are
there statements that are true of this definition that
can't be captured by any finite theory? Sure there
are, but that has nothing to do with whether it's
a proper syntactic definition. To say it's not a syntactic
definition, you have to point out something about
it that's not syntactic, or not correct as a model
of the naturals.
> > If it's actually the case (that every statement of basic arithmetic
> > is either true or false) then it's not a shortcoming to say so.
> > On the contrary, that would be a virtue.
>
> Speaking philosophically (since I'm posting from sci.philoisophy.tech),
> entities which in some sense exist but are thoroughly inaccessible seem
> to be of little value. This applies to the truth values of any
> statements which can never be known to be true or false.
While I have sympathy for that position, I don't think it's
tenable in the long run. Or anyway, it's not tenable to go
from "of little value" to suggesting that we should, say,
not attend to the real numbers because of the existence
of uncomputable numbers, or suggest that statements
that are undecidable one way or the other are somehow
neither true nor false. What they are is undecidable.
Marshall
Nam Nguyen
> On Dec 31, 12:18 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
>> My point still stands: if it's _impossible_ (as opposed to just being difficult)
>> to assign truth values to a formula then the formula is neither true nor false,
>
> Your point is still wrong.
Why? Are you saying all formulas (written in the language of arithmetic) must
have to be truth-definable? Do you have a reason so? Or are you just saying
that - as usual it seems?
>
>
>> which means that collectively the naturals isn't a _complete_ model of Q or its
>> extensions.
>
> Your conclusion is also still wrong, unsurprisingly.
What isn't unsurprising is your "refute" does have any technical details
to back it up.
Sigh! Does every technical debate have to be personal fight of sort to you?
Nam Nguyen
I meant "What is unsurprising ..."
Nam Nguyen
I do hate typo; and here's the correct version:
"What is unsurprising is your "refute" doesn't have any technical details
Daryl McCullough
>
>On Dec 31, 7:10=A0am, stevendaryl3...@yahoo.com (Daryl McCullough)
>wrote:
>> I don't see a rule saying f |- []f. Where did you see that?
>
>He didn't say that there was an explicitly stated rule of
>that form. He said that in step 8 of the derivation, they
>use a rule that was explicitly stated as
> If |- f then |- []f
>but they use it *as if* the rule was
> f |- []f
No, I don't think they did that. What they did was
to assume K(p & ~K(p)), and show that that leads to
a contradiction. That's a proof of ~K(p & ~K(p)).
So we have |- ~K(p & ~K(p)). Then we can apply the
rule "If |- f, then |- [] f" to conclude
[]~K(p & ~K(p))
Nam Nguyen
> On Dec 30, 8:16 pm, Barb Knox <s...@sig.below> wrote:
>> Marshall <marshall.spi...@gmail.com> wrote:
>>
>> By the nature of the construction of predicate logic, every arithmetic
>> formula must be either true or false in the standard model of the
>> natural numbers.
>>
>> But, we have no satisfactory way to fully characterise that standard
>> model! We all think we know what the natural numbers are, but Goedel
>> showed that there is no first-order way to define them, and I don't know
>> of *any* purely formal (i.e., syntactic) way to do do.
>
> I was more under the impression that Goedel showed there
> was no complete finite theory of them, rather than no
> way to define them.
Godel didn't show any of the 2 you've mentioned.
> Are you saying those are equivalent?
If I'm the one answering this question then "No": defining a model of a formal
system is not the same as demonstrating anything about a formal system that's
supposed to be about the model. Naturally.
>
>
>> (The usual ways
>> to define them are not fully syntactic, but rely on "the full semantics"
>> of 2nd-order logic, or "a standard model" of set theory, both of which
>> are more complicated than just relying on "the Standard Model" of
>> arithmetic in the first place.)
>
> Here's a possible definition:
>
> nat := 0 | succ nat
>
> x + 0 = x
> x + succ y = succ x+y
>
> x * 0 = 0
> x * succ y = x + (x * y)
>
> Is there some way this definition is not fully syntactic?
Yes: The part "nat := 0 | succ nat" isn't syntactical. [In the context
of FOL, being syntactical is being part of a FOL language/formula which
this part doesn't seem to be].
>
> It certainly seems to me that the above is fully syntactic,
> and is a complete definition of basic arithmetic.
That's *not* the canonical knowledge of arithmetic: what happens to the usual
syntactical symbol '<', in your "complete definition"?
> Are
> there statements that are true of this definition that
> can't be captured by any finite theory? Sure there
> are, but that has nothing to do with whether it's
> a proper syntactic definition. To say it's not a syntactic
> definition, you have to point out something about
> it that's not syntactic, or not correct as a model
> of the naturals.
Setting aside the missing "<", what you've defined up there is
*in no way* conforming with the _FOL definition of a model_ which
the naturals is supposed to be collectively. For example, what's
the set of 2-tuples that would correspond to your '+'?
>
>
>>> If it's actually the case (that every statement of basic arithmetic
>>> is either true or false) then it's not a shortcoming to say so.
>>> On the contrary, that would be a virtue.
>> Speaking philosophically (since I'm posting from sci.philoisophy.tech),
>> entities which in some sense exist but are thoroughly inaccessible seem
>> to be of little value. This applies to the truth values of any
>> statements which can never be known to be true or false.
>
> While I have sympathy for that position, I don't think it's
> tenable in the long run. Or anyway, it's not tenable to go
> from "of little value" to suggesting that we should, say,
> not attend to the real numbers because of the existence
> of uncomputable numbers, or suggest that statements
> that are undecidable one way or the other are somehow
> neither true nor false. What they are is undecidable.
First order undecidable formulas are in a different class than those
that aren't model-able, aren't truth assigned-able.
I asked you before:
"(1) There are infinite counter examples of GC.
Tell me what you'd even suspect as a road-map to assign true or
false to (1)?"
Now if you let (1') be defined as:
(1') df= (1) /\ A1 /\ A2 /\ ... A9
where A1 - A9 are Q's axioms (a la Shoenfield). Tell us, Marshall, what models or
what kinds of models that you think you could assign 'true' or 'false' to
(1')? If you really can't - which I don't think you can - then don't you at
least think of the possibility that there are arithmetic statements that can't
be true or false?
Why is it that a statement has to be true or false while _there's no way_ to
assign a truth value to it any way? Other than we might have grown up accustomed
to it, what kind of reasoning is that?
Ok I might sound a bit rhetorical here. But can you technically answer my question
about (1')?
Nam Nguyen
> Nam Nguyen says...
>> Daryl McCullough wrote:
>>> Nam Nguyen says...
>>>> Daryl McCullough wrote:
>>>>> By the way, I haven't thought about it a huge amount, but I
>>>>> don't have any problems with the paradox, because I don't
>>>>> accept the premise: Every true proposition is potentially knowable.
>>>>> It seems to me that sufficiently complex true propositions may never
>>>>> be known.
>>>> But how can we know it's true in the first place, when its being true
>>>> can't be known?
>>> I didn't say that we can *know* it is true. That's my point---something
>>> can be true without anyone knowing that it is true. It might be true,
>>> for example, that there is an even number of grains of sand in the world,
>>> but we may never find that out. Is e^pi rational? We may never find out.
>> Don't want to beat a dead horse so to speak but not knowing a truth because
>> its proof (knowledge) is _finitely_ larger than what one can possibly know
>> is *not* the same as not knowing a truth value because the statement is not
>> *genuinely* truth-assigned-able. The "sand in the world" being an even number
>> example above is of the 1st kind: not the 2nd kind.
>
> That was my point.
So, are you with me that there could be statements that are neither true or false,
on the ground that we can't assign a truth value to them; i.e., on the ground
what we've _intuitively perceived_ as the "natural numbers" is _not adequate_ for
us to say they are true or false?
> we will never know that they are true. There can also be statements
> that are true, but which we have no way of ever knowing that they are
> true. For example, I flip a coin, and before I see whether it lands
> heads up or tails up, it is run over by train, smashing it into a
> flat, smooth chip of metal. Now, there is no way of ever knowing
> whether it was heads-up or tails-up. But it is possible that
> "It was heads-up before it was smashed" is true.
>
> Statements can be true even if there is no way to ever know that they
> are true.
But that's _not_ my point! The statements I have in mind are the ones that
can _not_ be assigned true or false, in the first place! Do you see that they
aren't of the same kind of statements you've alluded to?
Barb Knox
<a3f061ed-3838-4be9...@u7g2000yqm.googlegroups.com>,
Marshall <marshal...@gmail.com> wrote:
> On Dec 30, 8:16�pm, Barb Knox <s...@sig.below> wrote:
> > �Marshall <marshall.spi...@gmail.com> wrote:
> >
> > By the nature of the construction of predicate logic, every arithmetic
> > formula must be either true or false in the standard model of the
> > natural numbers.
> >
> > But, we have no satisfactory way to fully characterise that standard
> > model! �We all think we know what the natural numbers are, but Goedel
> > showed that there is no first-order way to define them, and I don't know
> > of *any* purely formal (i.e., syntactic) way to do do.
>
> I was more under the impression that Goedel showed there
> was no complete finite theory of them, rather than no
> way to define them. Are you saying those are equivalent?
Yes, in this context. Since we are finite beings we need to use finite
systems.
> >�(The usual ways
> > to define them are not fully syntactic, but rely on "the full semantics"
> > of 2nd-order logic, or "a standard model" of set theory, both of which
> > are more complicated than just relying on "the Standard Model" of
> > arithmetic in the first place.)
>
> Here's a possible definition:
>
> nat := 0 | succ nat
>
> x + 0 = x
> x + succ y = succ x+y
>
> x * 0 = 0
> x * succ y = x + (x * y)
>
> Is there some way this definition is not fully syntactic?
> It uses no quantifying over predicates, so it can't be
> using second order logic.
> It certainly seems to me that the above is fully syntactic,
> and is a complete definition of basic arithmetic. Are
> there statements that are true of this definition that
> can't be captured by any finite theory? Sure there
> are, but that has nothing to do with whether it's
> a proper syntactic definition. To say it's not a syntactic
> definition, you have to point out something about
> it that's not syntactic, or not correct as a model
> of the naturals.
This is the usual first-order initial-algebra definition, and with the
addition of "succ x = succ y -> x=y" and an induction schema gives
first-order Peano Arithmetic. First-order logic is indeed formal (i.e.,
syntactic) in that all inferencing activities consist of finite
operations on finite strings. But, via Goedel and others, the Peano
axioms do NOT fully characterise the natural numbers N. N is indeed a
model (the Standard Model) which satisfies these axioms, but there are
also *non-standard models* which satisfy these axioms -- these models
contain infinite elements in addition to the usual naturals.
You can get some of the flavour of non-standard models by considering
the following non-standard model for just succ, where every element has
a unique successor and predecessor:
0, 1, 2, ... ..., w-2, w-1, w, w+1, w+2, ...
So, we can readily produce purely formal systems that are satisfied by
N, but all of them (as far as I know) are also satisfied by other,
non-standard, models. Try as we might, those pesky infinite
non-standard integers keep cropping up. That is the sense in which I
mean that we apparently can not formally fully characterise N.
(Note that we similarly cannot formally define "finite", so the dodge of
saying something like "the naturals are defined by the Peano axioms plus
the restriction that everything is finite" can not be expressed purely
formally.)
> > > If it's actually the case (that every statement of basic arithmetic
> > > is either true or false) then it's not a shortcoming to say so.
> > > On the contrary, that would be a virtue.
> >
> > Speaking philosophically (since I'm posting from sci.philoisophy.tech),
> > entities which in some sense exist but are thoroughly inaccessible seem
> > to be of little value. �This applies to the truth values of any
> > statements which can never be known to be true or false.
>
> While I have sympathy for that position, I don't think it's
> tenable in the long run. Or anyway, it's not tenable to go
> from "of little value" to suggesting that we should, say,
> not attend to the real numbers because of the existence
> of uncomputable numbers,
I am not an expert in that field, but I believe that almost all of real
analysis can be reconstructed using just computable numbers, e.g. the
work of Bishop.
> or suggest that statements
> that are undecidable one way or the other are somehow
> neither true nor false. What they are is undecidable.
They are true or false in any *particular* model. Since we apparently
cannot formally pin down arithmetic to have just one particular model
(the Standard one) then there will always be some arithmetic statements,
the undecidable ones, which are true in some models and false in others.
Thus it is unreasonable to say that an undecidable statement is simply
"true" or "false" -- we need to specify a particular model, almost
always the Standard one, which we can not fully characterise formally.
This doesn't prevent doing interesting number theory, but it is at least
somewhat bothersome from a foundational perspective.
Marshall
wrote:
Certainly steps 4 - 9 constitute an RAA proof with
the assumption being K(p & ~K(p)).
However what I was referring to was specifically
how they get from step 7 to step 8 within that
RAA proof. Your response does not seem to
address that particular issue.
Are your comfortable with how step 8 is
obtained from step 7 via Rule C as described
on this page?
http://plato.stanford.edu/entries/fitch-paradox/
It's entirely possible that I misunderstand
Jan Hidder's point, or rule C, or something
else entirely, however I would like to at
least feel that we were discussing the same
step in the proof.
Marshall
Marshall
> Marshall <marshall.spi...@gmail.com> wrote:
> > On Dec 30, 8:16 pm, Barb Knox <s...@sig.below> wrote:
> > > Marshall <marshall.spi...@gmail.com> wrote:
>
> > > By the nature of the construction of predicate logic, every arithmetic
> > > formula must be either true or false in the standard model of the
> > > natural numbers.
>
> > > But, we have no satisfactory way to fully characterise that standard
> > > model! We all think we know what the natural numbers are, but Goedel
> > > showed that there is no first-order way to define them, and I don't know
> > > of *any* purely formal (i.e., syntactic) way to do do.
>
> > I was more under the impression that Goedel showed there
> > was no complete finite theory of them, rather than no
> > way to define them. Are you saying those are equivalent?
>
> Yes, in this context. Since we are finite beings we need to use finite
> systems.
I have no disagreement with the point about finiteness, but I
don't see how that point leads to saying that a theory is
the same thing as a definition. That is rather tantamount to
saying that theories are all there are, and that's just not
true. There are things such as computational models,
for examples. It seems entirely appropriate to me to
use a computational model as the definition of something,
which is why I gave a computational model of the naturals
as a definition.
Perhaps worse, if it's not possible to have a definition of
anything, then I don't see how you can have any
theories, either. Theory of what? If you have no
definition, I don't see how you can even claim to
have an object under discussion.
Small points:
First of all, I claim "succ x = succ y -> x=y" is necessarily
the case via the definition of =.
Secondly, I claim we don't need to explicitly add any
induction schema, because induction on the naturals
in this case is merely a special case of structural
induction, which is itself merely a special case of
case analysis on the constructors for nat, and case
analysis is always available, as it were.
These are perhaps just quibbles.
> First-order logic is indeed formal (i.e.,
> syntactic) in that all inferencing activities consist of finite
> operations on finite strings. But, via Goedel and others, the Peano
> axioms do NOT fully characterise the natural numbers N. N is indeed a
> model (the Standard Model) which satisfies these axioms, but there are
> also *non-standard models* which satisfy these axioms -- these models
> contain infinite elements in addition to the usual naturals.
>
> You can get some of the flavour of non-standard models by considering
> the following non-standard model for just succ, where every element has
> a unique successor and predecessor:
>
> 0, 1, 2, ... ..., w-2, w-1, w, w+1, w+2, ...
>
> So, we can readily produce purely formal systems that are satisfied by
> N, but all of them (as far as I know) are also satisfied by other,
> non-standard, models. Try as we might, those pesky infinite
> non-standard integers keep cropping up. That is the sense in which I
> mean that we apparently can not formally fully characterise N.
I can see how your above set could be a model for PA, but
I don't see how it's supposed to be something that conforms
to the definition I gave.
For one thing, addition on the naturals is supposed to be total.
What is the result of "2 + w" under my definition of +? It does
not terminate, because you have introduced elements with
infinite descending deconstruction. That my addition operator
is total over (nat, nat) is provable; if there is some value
for which it is not total that value must therefor not
belong to nat.
For another thing, my definition doesn't have any "w" in
it, so you don't get to insert them in to the process.
We are supposed to be being syntactical here; recall
that you wanted to keep out second order logic and
set theory, so no "w".
Perhaps most importantly, I defined "nat" as those
things that are constructed via one of the two
specified constructors. Your w-elements are not
so constructed, so they cannot meet the definition
I gave.
I have noticed in the past that logicians and set
theorists don't necessarily buy the idea that
the universe consists only of those objects that
can be constructed using explicitly defined
construction rules. I am rather inclined to say
"tough," but perhaps I'll get better results if
I just say that's fine, but anything that isn't so
constructed isn't a natural, by definition.
> (Note that we similarly cannot formally define "finite", so the dodge of
> saying something like "the naturals are defined by the Peano axioms plus
> the restriction that everything is finite" can not be expressed purely
> formally.)
It seems to me that syntax is necessarily finite, but again
this is perhaps just a quibble.
> > > > If it's actually the case (that every statement of basic arithmetic
> > > > is either true or false) then it's not a shortcoming to say so.
> > > > On the contrary, that would be a virtue.
>
> > > Speaking philosophically (since I'm posting from sci.philoisophy.tech),
> > > entities which in some sense exist but are thoroughly inaccessible seem
> > > to be of little value. This applies to the truth values of any
> > > statements which can never be known to be true or false.
>
> > While I have sympathy for that position, I don't think it's
> > tenable in the long run. Or anyway, it's not tenable to go
> > from "of little value" to suggesting that we should, say,
> > not attend to the real numbers because of the existence
> > of uncomputable numbers,
>
> I am not an expert in that field, but I believe that almost all of real
> analysis can be reconstructed using just computable numbers, e.g. the
> work of Bishop.
I'd accept "almost all" but note that "almost all" isn't the
same as "all". For example, the order relation on computable
numbers is not itself computable, sadly. Also isn't it the
case that the least-upper-bound property is lost if we
limit ourselves to computables?
Regardless, the bigger issue, it seems to me, is
that any such system is going be be distinctly more
complex than the reals, and that complexity has a
nontrivial cost.
> > or suggest that statements
> > that are undecidable one way or the other are somehow
> > neither true nor false. What they are is undecidable.
>
> They are true or false in any *particular* model. Since we apparently
> cannot formally pin down arithmetic to have just one particular model
> (the Standard one) then there will always be some arithmetic statements,
> the undecidable ones, which are true in some models and false in others.
Even if we can pin it down, we still have statements that we don't
know if they are true or false. It might require an infinite amount
of computation to decide. Or just more than we will ever have.
> Thus it is unreasonable to say that an undecidable statement is simply
> "true" or "false" -- we need to specify a particular model, almost
> always the Standard one, which we can not fully characterise formally.
Sure, but whatever those statements do evaluate to, we can
narrow it down to one of two possibilities, even if we can't narrow
it any further.
> This doesn't prevent doing interesting number theory, but it is at least
> somewhat bothersome from a foundational perspective.
I agree that it is bothersome!
Marshall
Nam Nguyen
Agree. The question - and the heart of my argument - is whether or not there
exists a formula F such that it's impossible to know/assert a truth value
in the collection K of _all_ arithmetic models: K = {the standard one, the
non-standard ones}? I've argued that there exist such statements.
> Thus it is unreasonable to say that an undecidable statement is simply
> "true" or "false" -- we need to specify a particular model, almost
> always the Standard one, which we can not fully characterise formally.
>
> This doesn't prevent doing interesting number theory, but it is at least
> somewhat bothersome from a foundational perspective.
Arguably, FOL isn't just for number theories and so there's always a possibility
the existences of such formulas might shed some light about FOL systems that
we've largely ignored: e.g. systems that have infinite number of logical symbols,
some of which might represent isomorphic - but different - operations.
Marshall
> Marshall wrote:
> > On Dec 30, 8:16 pm, Barb Knox <s...@sig.below> wrote:
> >> Marshall <marshall.spi...@gmail.com> wrote:
>
> >> By the nature of the construction of predicate logic, every arithmetic
> >> formula must be either true or false in the standard model of the
> >> natural numbers.
>
> >> But, we have no satisfactory way to fully characterise that standard
> >> model! We all think we know what the natural numbers are, but Goedel
> >> showed that there is no first-order way to define them, and I don't know
> >> of *any* purely formal (i.e., syntactic) way to do do.
>
> > I was more under the impression that Goedel showed there
> > was no complete finite theory of them, rather than no
> > way to define them.
>
> Godel didn't show any of the 2 you've mentioned.
"Any effectively generated theory capable of expressing
elementary arithmetic cannot be both consistent and complete.
In particular, for any consistent, effectively generated formal
theory that proves certain basic arithmetic truths, there is an
arithmetical statement that is true, but not provable in the theory."
So there cannot be a complete finite theory of basic arithmetic.
> > Are you saying those are equivalent?
>
> If I'm the one answering this question then "No": defining a model of a formal
> system is not the same as demonstrating anything about a formal system that's
> supposed to be about the model. Naturally.
Well we agree on one thing. That's unusual.
> > It certainly seems to me that the above is fully syntactic,
> > and is a complete definition of basic arithmetic.
>
> That's *not* the canonical knowledge of arithmetic: what happens to the usual
> syntactical symbol '<', in your "complete definition"?
It's easy to extend this with <.
> > Are
> > there statements that are true of this definition that
> > can't be captured by any finite theory? Sure there
> > are, but that has nothing to do with whether it's
> > a proper syntactic definition. To say it's not a syntactic
> > definition, you have to point out something about
> > it that's not syntactic, or not correct as a model
> > of the naturals.
>
> Setting aside the missing "<", what you've defined up there is
> *in no way* conforming with the _FOL definition of a model_ which
> the naturals is supposed to be collectively. For example, what's
> the set of 2-tuples that would correspond to your '+'?
The goal was to provide a syntactic definition of the
naturals, which I did. The goal was not to provide
a FOL model. Nonetheless it's pretty easy to
get there from here. For example:
{((x, y), z) | x+y=z}
> >>> If it's actually the case (that every statement of basic arithmetic
> >>> is either true or false) then it's not a shortcoming to say so.
> >>> On the contrary, that would be a virtue.
> >> Speaking philosophically (since I'm posting from sci.philoisophy.tech),
> >> entities which in some sense exist but are thoroughly inaccessible seem
> >> to be of little value. This applies to the truth values of any
> >> statements which can never be known to be true or false.
>
> > While I have sympathy for that position, I don't think it's
> > tenable in the long run. Or anyway, it's not tenable to go
> > from "of little value" to suggesting that we should, say,
> > not attend to the real numbers because of the existence
> > of uncomputable numbers, or suggest that statements
> > that are undecidable one way or the other are somehow
> > neither true nor false. What they are is undecidable.
>
> First order undecidable formulas are in a different class than those
> that aren't model-able, aren't truth assigned-able.
>
> I asked you before:
>
> "(1) There are infinite counter examples of GC.
>
> Tell me what you'd even suspect as a road-map to assign true or
> false to (1)?"
You keep assuming that the mere fact that a sentence is
undecidable means that it has some definite truth value
that is not one of {true, false}. Apparently you just take
this as a given. I, however, regard it as a false statement.
> Now if you let (1') be defined as:
>
> (1') df= (1) /\ A1 /\ A2 /\ ... A9
>
> where A1 - A9 are Q's axioms (a la Shoenfield). Tell us, Marshall, what models or
> what kinds of models that you think you could assign 'true' or 'false' to
> (1')? If you really can't - which I don't think you can - then don't you at
> least think of the possibility that there are arithmetic statements that can't
> be true or false?
I suppose anything is possible, in some vague, New-Age sort of
way. I suppose if someone were to supply some convincing
argument as to why there must be some third possibility,
I would at least consider it.
However, I have yet to hear any convincing argument
in favor of there being a third possibility. The mere fact
of a decision being hard, even infinitely hard, does not
suggest to me the existence of some third truth value
for a sentence to have.
> Why is it that a statement has to be true or false while _there's no way_ to
> assign a truth value to it any way? Other than we might have grown up accustomed
> to it, what kind of reasoning is that?
>
> Ok I might sound a bit rhetorical here. But can you technically answer my question
> about (1')?
It seems to me that the definitions of the various things we
are talking about necessitate that a statement is either
true or false. The definition does not admit to the existence
of any third possibility. That some statements are undecidable
does not alter the definition of the terms the statements
were made with; the definitions remain as they were.
Thus every statement must have one of the two truth
values, by definition.
Now, if you want to make some new system to evaluate
statements in, that could certainly be defined with more
than the usual two possibilities. But that wouldn't be the
usual basic arithmetic; it'd be something new.
Although I don't consider reasoning by analogy to the
real world to be a great technique, it is at least suggestive
that there are real-world statements that we can
narrow down to few possibilities but cannot narrow
down to one. For example, Mr. McCullough's coin-and-
railroad story. We could even further say we were
close enough to see the coin landed definitely on
one side, but we weren't close enough to say
which side it was.
Marshall
Marshall
> Barb Knox wrote:
>
> > They are true or false in any *particular* model. Since we apparently
> > cannot formally pin down arithmetic to have just one particular model
> > (the Standard one) then there will always be some arithmetic statements,
> > the undecidable ones, which are true in some models and false in others.
>
> Agree. The question - and the heart of my argument - is whether or not there
> exists a formula F such that it's impossible to know/assert a truth value
> in the collection K of _all_ arithmetic models: K = {the standard one, the
> non-standard ones}? I've argued that there exist such statements.
Why would the existence of such statements imply that there
are truth values other than true or false?
Marshall
Nam Nguyen
You seemed to have confused between the FOL definition of models of formal
systems in general and constructing a _specific_ model _candidate_. In defining
the naturals, say, from computational model ... or whatever, you're just
defining what the naturals be. It's still your onerous to prove/demonstrate
this definition of the naturals would meet the definition of a model for,
say Q, PA, .... So far, have you or any human beings successfully demonstrated
so, without being circular? Of course not.
Marshall
Showing that the axioms of PA are true in my definition is
straightforward, using only structural induction, which in the
case of my two-constructor definition is simply case
analysis of the two cases.
Try it; it's fun!
Marshall
Nam Nguyen
Because a) FOL truth is no longer absolute: it has to be relativized to some
models; and yet b) what one constructs and _label_ as a model might indeed
be impossible to be technically verified as a model. How could a statement be
true or false if in the first place it can't be true-able or false-able?
I think I've asked/raised this question a few times but have yet to hear
a response to it!
Marshall
There is simply no issue here to respond to. Everything you've
said here is either false or else it's the same as the conclusion
you're trying to establish.
Marshall
Nam Nguyen
I'm not assuming anything in asking you the question, Marshall.
If a simple question that you, I, or anyone could either know
or don't know the answer.
If I'm to answer the question I'd say I don't know of any possible
road-map. If you you think (1) is false, as you seem to have so,
present your road-map, reasons based on the _accepted definitions_
of FOL models etc...to back it up
Don't just evade the question and hope that people would understand
your argument!
Nam Nguyen
Great "refute" you seem to have had here! Among "everything" I've said here
are a) and b). Why do you think they're false? Or you just said so out of the
habit of saying things with no back-up reasons?
Btw, usually "conclusion" is "the same" thing as what one would be "trying to
establish". You seemed to be surprise of that. Why?
Nam Nguyen
It might be straightforward to you and you might call it "Cheney induction"
instead of "structural induction" but it's irrelevant and the question is
the same: how could you demonstrate that your definition would meet the FOL
standard definition of model of a formal system? Did you already make that
presentation in the thread and I simply missed it?
> which in the
> case of my two-constructor definition is simply case
> analysis of the two cases.
>
> Try it; it's fun!
I'm sure there are a lot of fun things in life but here the interesting thing
would be demonstrating your definitions meet the FOL definition of models
of formal systems. You haven't tried it; so what you've claimed here isn't
interesting!
>
>
> Marshall
Marshall
I have no opinion on whether (1) is true or false. I don't believe
that question to be relevant to the question of whether statements
in arithmetic are either definitely true or definitely false.
Suppose I tell you I have a natural number in mind, but it's
impossible for you to know which natural number it is.
However we all know that this natural number can be
encoded as a binary string. Let me ask you a question
about this number: does its representation as a binary
string contain any characters in it besides "0" and "1"?
You don't need to know which number it is to answer
this question. Likewise, you don't need to know the
truth or falsity of (1) to know that its truth-value is
limited to being one of those two.
Marshall
Marshall
What sort of thing would you accept as an answer? What
difficulties do you foresee?
If you are convinced it is impossible and that nothing will
satisfy you, I'd rather not waste my time. On the other
hand if you have a specific idea as to what a correct
answer would look like, I might be able to satisfy you.
Marshall
Gene Wirchenko
wrote:
>Marshall wrote:
[snip]
>> There is simply no issue here to respond to. Everything you've
>> said here is either false or else it's the same as the conclusion
>> you're trying to establish.
>
>Great "refute" you seem to have had here! Among "everything" I've said here
>are a) and b). Why do you think they're false? Or you just said so out of the
>habit of saying things with no back-up reasons?
>
>Btw, usually "conclusion" is "the same" thing as what one would be "trying to
>establish". You seemed to be surprise of that. Why?
I am impressed with the speed that you showed yourself a fool
worthy of killfiling.
Sincerely,
Gene Wirchenko
Nam Nguyen
The simple thing that everyone including you would expect and accept:
conforming with the standard definition of a model of a formal system.
For instance given the language L(e) and the formal system T = {Ax[x=e]};
let's U be the singleton of the empty set U = {{}} and the set M of ordered
pairs be defined/constructed as:
M = {('A',U), ('e',(e,e))}
One doesn't call -or not call- the constructed M a model of T until one verifies
it does or doesn't conform with the FOL definition of model, right? An in this case
it turns out M meets the definition and therefore Nam or Marshal could call it
a model of M, but not before the verification. Naturally.
Can you verify that your definition of the naturals meet the definition of
formal system model, with say Q is the underlying system at hand, as I did
verify M w.r.t to T above? [It's just a pure simple technical question!]
> What difficulties do you foresee?
Ok. this is a much better and more technical question one could entertain.
In a nutshell, one of difficulties that formula such as (1) or (1') presents is
that there's no way you could define any model of Q such that a certain expected
set of 2-tuples (i.e. _relation_) can be verified to exist. And if you can't,
you can't tell whether or not you have would conform to the overall definition of a
model of the underlying formal system (say Q in this case).
In details, if (1) is true then there would exist an infinite sequence of primes
p1, p2, p3, ...., each of which is the maximum prime less than the corresponding
counter example of GC. Which means there's a relation "depicted" as:
p1 < p2 < p3 < .... pn < ...
or, using the definition, there's this relation R:
R = {(p1,p2), (p2,p3), ....}
The problem is then there's not yet a formal or intuitive way that we could
determine R to be empty or not - and there's always the possibility you can never
be able to ascertain one way or another.
But R is part of what you could define as a model of Q (and the naturals would be such
a model). And if you couldn't ascertain the existence of part of the model (naturals
or non-standard), how could you know what you have is in fact a model of the formal
system?
If you understand this difficulty then to say there's a formula we can't assign a truth
value in this "model" is equivalent in meta level to saying there's no way to verify
this is in fact a model of the system. In a nutshell.
>
> If you are convinced it is impossible and that nothing will
> satisfy you, I'd rather not waste my time. On the other
> hand if you have a specific idea as to what a correct
> answer would look like, I might be able to satisfy you.
I did come up with the requirement that the R above being empty or not should
be known: that's the requirement of FOL model definition. If you don't know that,
you can't never know if certain formulas would be true or false simply because
what you believe as a model fails to be verified as a model.
Nam Nguyen
I meant "I didn't come up..."
Nam Nguyen
This is a public forum and hence fwiw I don't have interest or concern about someone
is being killfiled by anybody or not. All I'm doing in here is listing to people's
rationale to see what is what in mathematical reasoning.
Regards,
Nam Nguyen
>
> Sincerely,
>
> Gene Wirchenko
Daryl McCullough
>However what I was referring to was specifically
>how they get from step 7 to step 8 within that
>RAA proof. Your response does not seem to
>address that particular issue.
That's exactly the step that I was talking about.
Steps (4), (5) and (6) and (7) constitute a proof
of ~K(p ∧ ~Kp). Therefore, we have
|- ~K(p ∧ ~Kp)
By C, if you have |- f, then you have |- [] f.
Letting f = ~K(p ∧ ~Kp), it follows that
|- [] ~K(p ∧ ~Kp)
which is step (8).
>Are your comfortable with how step 8 is
>obtained from step 7 via Rule C as described
>on this page?
>http://plato.stanford.edu/entries/fitch-paradox/
Yes, that's exactly what they are doing. They
didn't use the |- symbol in step 7, but it is
clear that (7) is the conclusion of a proof.
Daryl McCullough
>
>In article
><a3f061ed-3838-4be9...@u7g2000yqm.googlegroups.com>,
> Marshall <marshal...@gmail.com> wrote:
>> I was more under the impression that Goedel showed there
>> was no complete finite theory of them, rather than no
>> way to define them. Are you saying those are equivalent?
>
>Yes, in this context. Since we are finite beings we need to use finite
>systems.
I don't agree. What Godel's theorem says is that we can't know all
the truths about the natural numbers, but it doesn't imply that there
is any fuzziness in what we mean by natural numbers.
All the nonstandard models of the naturals contain infinite objects.
We're not likely to mistake such an object for an actual natural. As
you say, we are finite beings, so any natural we can write down is
finite.
Nam Nguyen
> Barb Knox says...
>> In article
>> <a3f061ed-3838-4be9...@u7g2000yqm.googlegroups.com>,
>> Marshall <marshal...@gmail.com> wrote:
>
>>> I was more under the impression that Goedel showed there
>>> was no complete finite theory of them, rather than no
>>> way to define them. Are you saying those are equivalent?
>> Yes, in this context. Since we are finite beings we need to use finite
>> systems.
>
> I don't agree. What Godel's theorem says is that we can't know all
> the truths about the natural numbers, but it doesn't imply that there
> is any fuzziness in what we mean by natural numbers.
For what it's worth, in mathematics the truths about the natural numbers is
what we mean we mean by the natural numbers, not what they existentially are!
>
> All the nonstandard models of the naturals contain infinite objects.
> We're not likely to mistake such an object for an actual natural. As
> you say, we are finite beings, so any natural we can write down is
> finite.
But there's no such thing as finite natural numbers. Natural numbers are natural
numbers, infinite or not.
Jan Hidders
> Marshall says...
>
> >However what I was referring to was specifically
> >how they get from step 7 to step 8 within that
> >RAA proof. Your response does not seem to
> >address that particular issue.
>
> That's exactly the step that I was talking about.
> Steps (4), (5) and (6) and (7) constitute a proof
> |- ~K(p ∧ ~Kp)
>
> By C, if you have |- f, then you have |- [] f.
> |- [] ~K(p ∧ ~Kp)
> which is step (8).
>
> >Are your comfortable with how step 8 is
> >obtained from step 7 via Rule C as described
> >on this page?
> >http://plato.stanford.edu/entries/fitch-paradox/
>
> Yes, that's exactly what they are doing. They
> didn't use the |- symbol in step 7, but it is
> clear that (7) is the conclusion of a proof.
Wow. You are right. They correctly conclude in (7) that |- ~K(p ∧
~Kp).
Hmm. I need to think this over. I'm beginning to believe now that the
inference in the paradox is in fact correct.
-- Jan Hidders
Jan Hidders
wrote:
> Okay, I've thought about it a little more, and I have come to
> the conclusion that Fitch's paradox is invalid. Or perhaps the
> statement of the knowability principle is wrong.
>
> Here's the proof of the contradiction:
>
> 1. (Knowability principle) For all p: p -> <> K(p)
>
> where <>Phi means "Phi is possibly true" and K(Phi) means
> "Phi is known".
>
> 2. (Non-omniscience principle) For some p: p & ~K(p)
>
> 3. Letting p0 be the true but unknown proposition, we have
> p0 & ~K(p0)
>
> 4. From 1&3, we have <>K(p0 & ~K(p0))
>
> At this point, let me switch to possible world semantics: <> Phi
> means "Phi is true in some world". So let's switch to the world
> in which K(p0 & ~K(p0)) is true. In that world we have
>
> 5. K(p0 & ~K(p0))
>
> From this it follows:
>
> 6. K(p0) & K(~K(p0))
>
> But only true things are knowable, so from K(~K(p0)) it
> follows that ~K(p0). So we have
>
> 7. K(p0) & ~K(p0)
>
> which is a contradiction.
>
> The mistake becomes clearer if we explicitly introduce
> possible worlds. Let's use w ||- Phi to mean "Phi is true
> in world w" and K_w(Phi) to mean "Phi is known in world
> w". Let's introduce w0 to mean "our world". Then the
> proof becomes the following:
>
> 1. (Knowability principle) for all p: (w0 ||- p) -> exists w, K_w(p)
>
> In other words, if p is true in our world, then there exists another
> world in which p is knowable.
>
> 2. (Non-omniscience principle) for some p: w0 ||- p & ~K_w0(p)
>
> 3. Introducing the constant p0 for this unknown proposition, we
> have: w0 ||- p0 & ~K_w0(p0)
>
> 4. From 1&3, we have exists w, K_w(p0 & ~K_w0(p0))
>
> 5. Letting w' be a name for some world making the existential true,
> we have: K_w'(p0 & ~K_w0(p0))
>
> From this it follows:
>
> 6. K_w'(p0) & K_w'(~K_w0(p0))
>
> Since only true things are knowable, we have:
>
> 7. K_w'(p0) & ~K_w0(p0)
>
> That's no contradiction at all! The proposition p0 is
> known in one world, w', but not in another world, w0.
> It only becomes a contradiction when you erase the
> world suffixes.
True, but you have now fundamentally changed the semantics of the K
operator in the sense that the model theory now looks very different.
You have essentially turned K from a unary operator K(p) to a binary
operator K(w,p).
If you assume the model theory that I presented earlier the inferences
can be verified to be in fact all correct (with apologies for copying
your words):
Let W be the set of all possible worlds, and w0 the element of W that
is our world in W. Since W will be fixed I will omit it in (W, w) ||-
Phi and simply write w ||- Phi.
1. (Knowability principle) for all p : (w0 ||- p) -> exists w in W, w
||- K(p)
2. (Non-omniscience principle) For some p: w0 ||- p & ~K(p)
3. Introducing the constant p0 for this unknown proposition, we have:
w0 ||- p0 & ~K(p0)
4. From 1&3, we have: Exists w in W, w ||- K(p0 & ~K(p0))
5. Letting w' be a name for some world making the existential true, we
have: w' ||- K(p0 & ~K(p0))
From this by principle (A) it follows:
6. w' ||- K(p0) and w' ||- K(~K(p0))
Since only true things are knowable by principle (B), we have:
7. w' ||- K(p0) and w' ||- ~K(p0)
From the semantics of K in the model theory it then follows that:
8. K(p0) in w' and K(p0) not in w'
Which is indeed a contradiction.
-- Jan Hidders
Marshall
> Marshall wrote:
>
> Can you verify that your definition of the naturals meet the definition of
> formal system model, with say Q is the underlying system at hand, as I did
> verify M w.r.t to T above? [It's just a pure simple technical question!]
I expect so. I haven't gone through the exercise at length, but
the whole process seems straightforward enough. I have done
certain individual proofs, but not all of them.
> > What difficulties do you foresee?
>
> Ok. this is a much better and more technical question one could entertain.
>
> In a nutshell, one of difficulties that formula such as (1) or (1') presents is
> that there's no way you could define any model of Q such that a certain expected
> set of 2-tuples (i.e. _relation_) can be verified to exist. And if you can't,
> you can't tell whether or not you have would conform to the overall definition of a
> model of the underlying formal system (say Q in this case).
If you don't admit the existence of any possible technique of
showing such a thing, it wouldn't be a good use of my time
to try to convince you otherwise.
Note at least that yours is a minority opinion, here; it's certainly
possible to show the necessary relations exist, and have
the desired properties, though such ordinary methods as
induction.
Marshall
Daryl McCullough
>> From this it follows:
>>
>> 6. K_w'(p0) & K_w'(~K_w0(p0))
>>
>> Since only true things are knowable, we have:
>>
>> 7. K_w'(p0) & ~K_w0(p0)
>>
>> That's no contradiction at all! The proposition p0 is
>> known in one world, w', but not in another world, w0.
>> It only becomes a contradiction when you erase the
>> world suffixes.
>
>True, but you have now fundamentally changed the semantics of the K
>operator in the sense that the model theory now looks very different.
>You have essentially turned K from a unary operator K(p) to a binary
>operator K(w,p).
That's not a change of the *semantics*. That's a change of the
*syntax*. My claim is that in the possible worlds semantics,
every predicate (and operator) that can vary from world to world
implicitly is a function of the world. That complexity can usually
be avoided because implicitly we assume that everything is talking
the same world. But when you nest <> and K, it is no longer possible
to make that assumption. Not without restrictions on what can be
said. My point is that the knowability principle doesn't make
any sense without explicit mention of possible worlds.
It might make sense if we restrict the principle to propositions
p that don't involve the knowability operator. But if we restrict
it that way, we can't carry out Fitch's proof.
Jesse F. Hughes
> On 1 jan, 05:26, stevendaryl3...@yahoo.com (Daryl McCullough) wrote:
>> Marshall says...
>>
>> >Are your comfortable with how step 8 is
>> >obtained from step 7 via Rule C as described
>> >on this page?
>> >http://plato.stanford.edu/entries/fitch-paradox/
>>
>> Yes, that's exactly what they are doing. They
>> didn't use the |- symbol in step 7, but it is
>> clear that (7) is the conclusion of a proof.
>
> Wow. You are right. They correctly conclude in (7) that |- ~K(p & ~Kp).
>
> Hmm. I need to think this over. I'm beginning to believe now that the
> inference in the paradox is in fact correct.
But of course it's correct!
Fitch's paradox is perfectly non-controversial, as a matter of purely
formal reasoning. It's well-known and well studied by logicians. It
would be truly remarkable if you found an error in a famous formal
proof of under a dozen lines.
--
"The papers are currently at journals. [When published,] make no
mistake, there will be no place on this planet where you can hide.
Remember, I'm not talking about something vague here. I'm talking
about publication in journals." James S. Harris. Wow. Journals.
Jesse F. Hughes
> That's not a change of the *semantics*. That's a change of the
> *syntax*. My claim is that in the possible worlds semantics,
> every predicate (and operator) that can vary from world to world
> implicitly is a function of the world. That complexity can usually
> be avoided because implicitly we assume that everything is talking
> the same world. But when you nest <> and K, it is no longer possible
> to make that assumption. Not without restrictions on what can be
> said. My point is that the knowability principle doesn't make
> any sense without explicit mention of possible worlds.
>
> It might make sense if we restrict the principle to propositions
> p that don't involve the knowability operator. But if we restrict
> it that way, we can't carry out Fitch's proof.
I haven't worked through the semantic details (at least not recently),
but the proof clearly "works" and the intuition behind the proof seems
plausible enough.
Suppose that p is true, but I don't know it. Then p & ~Kp is true.
But surely, I could not know p & ~Kp. That is, I couldn't know "p is
true, but I don't know that p is true."
After all, if I know that conjunction, then I know that p is true, so
how could I know that I don't know that p is true?
The argument seems perfectly clear to me, both formally and
informally.
--
Jesse F. Hughes
"To all Leaders of the World, buy or rent the movie 'The Day
After'[...] I assure you will have a new perspective on WMDs."
-- practical advice from online petitions
Jan Hidders
Explicit in the formulas? So you reallly do want to change the syntax?
If not, I'm a bit puzzled as to how you want to change the semantics.
It would help if you could provide a model theory to explain how you
want to change the semantics. Right now the model theory I gave
already does allow the operator K to be different in possible worlds.
So how would your semantics differ from that?
-- Jan Hidders
Daniel Pitts
> stevend...@yahoo.com (Daryl McCullough) writes:
>
>> That's not a change of the *semantics*. That's a change of the
>> *syntax*. My claim is that in the possible worlds semantics,
>> every predicate (and operator) that can vary from world to world
>> implicitly is a function of the world. That complexity can usually
>> be avoided because implicitly we assume that everything is talking
>> the same world. But when you nest <> and K, it is no longer possible
>> to make that assumption. Not without restrictions on what can be
>> said. My point is that the knowability principle doesn't make
>> any sense without explicit mention of possible worlds.
>>
>> It might make sense if we restrict the principle to propositions
>> p that don't involve the knowability operator. But if we restrict
>> it that way, we can't carry out Fitch's proof.
>
> I haven't worked through the semantic details (at least not recently),
> but the proof clearly "works" and the intuition behind the proof seems
> plausible enough.
>
> Suppose that p is true, but I don't know it. Then p & ~Kp is true.
> But surely, I could not know p & ~Kp. That is, I couldn't know "p is
> true, but I don't know that p is true."
>
> After all, if I know that conjunction, then I know that p is true, so
> how could I know that I don't know that p is true?
>
> The argument seems perfectly clear to me, both formally and
> informally.
~Kp)" would also be true. There are a whole islands of truths that
can't be known to be true, but are indeed true. This is basically
G�del's theorem.
Fitch's proof (at least by your description) is using the proof as its
own premise. p & ~Kp can be true without knowing it, therefore you
still don't know p is true.
--
Daniel Pitts' Tech Blog: <http://virtualinfinity.net/wordpress/>
Daryl McCullough
>Suppose that p is true, but I don't know it. Then p & ~Kp is true.
>But surely, I could not know p & ~Kp. That is, I couldn't know "p is
>true, but I don't know that p is true."
>
>After all, if I know that conjunction, then I know that p is true, so
>how could I know that I don't know that p is true?
>
>The argument seems perfectly clear to me, both formally and
>informally.
I agree. My point is not about the proof, it's about the
"knowability principle" that if something is true, then
it is possible that it is knowable. That's not a reasonable
thing to assume unless we either restrict what sort of propositions
we are talking about, or be more explicit about *who* knows what.
I don't have any problem with the proof of Fitch's paradox. It's
a valid proof, but I take it as evidence for rejecting the knowability
principle.
Daryl McCullough
>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.
>If not, I'm a bit puzzled as to how you want to change the semantics.
>It would help if you could provide a model theory to explain how you
>want to change the semantics. Right now the model theory I gave
>already does allow the operator K to be different in possible worlds.
>So how would your semantics differ from that?
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.
Jan Hidders
> stevendaryl3...@yahoo.com (Daryl McCullough) writes:
> > That's not a change of the *semantics*. That's a change of the
> > *syntax*. My claim is that in the possible worlds semantics,
> > every predicate (and operator) that can vary from world to world
> > implicitly is a function of the world. That complexity can usually
> > be avoided because implicitly we assume that everything is talking
> > the same world. But when you nest <> and K, it is no longer possible
> > to make that assumption. Not without restrictions on what can be
> > said. My point is that the knowability principle doesn't make
> > any sense without explicit mention of possible worlds.
>
> > It might make sense if we restrict the principle to propositions
> > p that don't involve the knowability operator. But if we restrict
> > it that way, we can't carry out Fitch's proof.
>
> I haven't worked through the semantic details (at least not recently),
> but the proof clearly "works" and the intuition behind the proof seems
> plausible enough.
>
> Suppose that p is true, but I don't know it. Then p & ~Kp is true.
> But surely, I could not know p & ~Kp. That is, I couldn't know "p is
> true, but I don't know that p is true."
>
> After all, if I know that conjunction, then I know that p is true, so
> how could I know that I don't know that p is true?
>
> The argument seems perfectly clear to me, both formally and
> informally.
Yes, it does. Thanks. Very nicely formulated.
It did strike me that you formulated K as "I know that P". For some
reason it made me realize that it was formulated on the Stanford page
as "Somebody at some time knows that P". Under the latter
interpretation it seems now indeed a bit strange to me to require that
all facts, and specifically those of the form ~Kp, are possibly known.
I can imagine there are facts p for which we can never establish
definitively that they will not be known to somebody at some time,
except after waiting until we run out of time or persons, and by then
there will be nobody left to know this. So ~Kp might very well be both
true and unknowable.
-- Jan Hidders
Jan Hidders
> 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
syntax?
> >If not, I'm a bit puzzled as to how you want to change the semantics.
> >It would help if you could provide a model theory to explain how you
> >want to change the semantics. Right now the model theory I gave
> >already does allow the operator K to be different in possible worlds.
> >So how would your semantics differ from that?
>
> 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. The given model theory still seems to contain the paradox,
so you will want to change it. Can you show how?
-- Jan Hidders
Daryl McCullough
>
>On 2 jan, 00:14, stevendaryl3...@yahoo.com (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
>syntax?
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.
vldm10
> W = the type of possible worlds
> A = the type of atomic propositions
> P = the type of all propositions
I am not sure that propositions are types???
Let me give you the following example:
This sentence is false.
--
Vladimir Odrljin
Jan Hidders
Ok. I think I get what you want to do.
But I'm afraid I don't think that will work. The reason is that in
your logic you can still express the same things that could be
expressed in the old logic. Take for example the following proposition
in the old model theory:
(1) K(p & ~K(p))
You can still express this in your logic. You can do this by using a
predicate CW(w) that expresses that w is (equivalent to) the current
world. You can express this as follows:
(2) CW(w) =def= For all p, ( t(w,p) <-> p )
With that you can write (1) in your logic as:
(3) Forall w : W, ( CW(w) -> k(w, (p & ~k(w, p))) )
This can be done for all for all formulas in the old logic and so it
seems to me that you will still have the same paradox but written down
differently.
-- Jan Hidders
Daryl McCullough
>But I'm afraid I don't think that will work. The reason is that in
>your logic you can still express the same things that could be
>expressed in the old logic. Take for example the following proposition
>in the old model theory:
>
>(1) K(p & ~K(p))
>
>You can still express this in your logic.
Yes, but with the correct axiomatization of knowability
predicate, the corresponding proposition will not be true.
>You can do this by using a predicate CW(w) that expresses
>that w is (equivalent to) the current world. You can express
>this as follows:
>
>(2) CW(w) =def= For all p, ( t(w,p) <-> p )
>
>With that you can write (1) in your logic as:
>
>(3) Forall w : W, ( CW(w) -> k(w, (p & ~k(w, p))) )
>
>This can be done for all for all formulas in the old logic and so it
>seems to me that you will still have the same paradox but written down
>differently.
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
vldm10 says...
>
>On Jan 2, 4:14=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough) wrote:
>
>> W = the type of possible worlds
>> A = the type of atomic propositions
>> P = the type of all propositions
>
>
>I am not sure that propositions are types???
>Let me give you the following example:
>
>This sentence is false.
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).
Jan Hidders
> Jan Hidders says...
>
> >But I'm afraid I don't think that will work. The reason is that in
> >your logic you can still express the same things that could be
> >expressed in the old logic. Take for example the following proposition
> >in the old model theory:
>
> >(1) K(p & ~K(p))
>
> >You can still express this in your logic.
>
> Yes, but with the correct axiomatization of knowability
> predicate, the corresponding proposition will not be true.
>
> >You can do this by using a predicate CW(w) that expresses
> >that w is (equivalent to) the current world. You can express
> >this as follows:
>
> >(2) CW(w) =def= For all p, ( t(w,p) <-> p )
>
> >With that you can write (1) in your logic as:
>
> >(3) Forall w : W, ( CW(w) -> k(w, (p & ~k(w, p))) )
>
> >This can be done for all for all formulas in the old logic and so it
> >seems to me that you will still have the same paradox but written down
> >differently.
>
> 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 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
Daryl McCullough
>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)
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.
>If your logic is complete it will also have the
>equivalents of all the used axioms and principles,
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.
vldm10
wrote:
> In article <46afa0f9-e70d-4d21-bf67-7f49cd16b...@21g2000yqj.googlegroups.com>,
> vldm10 says...
>
>
>
> >On Jan 2, 4:14=A0pm, stevendaryl3...@yahoo.com (Daryl McCullough) wrote:
>
> >> W = the type of possible worlds
> >> A = the type of atomic propositions
> >> P = the type of all propositions
>
> >I am not sure that propositions are types???
> >Let me give you the following example:
>
> >This sentence is false.
>
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 )
> 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).
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?
>
> --
> Daryl McCullough
> Ithaca, NY
Vladimir Odeljin
Jan Hidders
> 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. 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.
> 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.
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
Daryl McCullough
>
>On 3 jan, 14:09, stevendaryl3...@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.
Jan Hidders
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
Daryl McCullough
>
>On 3 jan, 18:32, stevendaryl3...@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.
Jan Hidders
> Jan Hidders says...
>
>
>
>
>
>
>
> >On 3 jan, 18:32, stevendaryl3...@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
Daryl McCullough
>> >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)
Tegiri Nenashi
differentiating the concepts of "World" and "Model"?
Jan Hidders
> Excuse me, but I have a basic question. What is the motivation for
> differentiating the concepts of "World" and "Model"?
The term model is usually used for the complete structure for which we
define the truth value of a formula. In conventional logic this is
usually a model of the particular world we assume we are in. However,
in modal logic this includes the complete set of possible worlds plus
the particular world we assume we are in. Both are needed since for
basic propositions we need to inspect the actual world and the modal
operators refer also to the other possible worlds.
-- Jan Hidders
Daryl McCullough
>Excuse me, but I have a basic question. What is the motivation for
>differentiating the concepts of "World" and "Model"?
You could think of each possible world as a different model of a theory. That
works. (Although there may need to be certain constraints on what models of a
theory are under consideration). But the philosophical discussion of what's
possible, and what's necessary, and alternative possible worlds predates modern
model theory.
One thing that is different about modal logics is that ability to refer to
multiple possible worlds (any time you say that something is possible, you are
implicitly quantifying over possible worlds). It's not usual in model theory to
allow quantification over models in the object language (although such
quantification may take place in the metalanguage). When you consider
propositions involving modal operators, a single "possible world" is not a model
for such propositions. It's the entire structure of all possible worlds that is
being referred to by statements such as: "It is necessarily the case that X".
There is a discussion of the various uses of possible worlds here:
http://www9.georgetown.edu/faculty/ap85/papers/PhilThesis.html
but there is no mention of the fact that a possible world is a model of a
theory.
Vadim Tropashko
> Excuse me, but I have a basic question. What is the motivation for
> differentiating the concepts of "World" and "Model"?
Model (aka structure) is an ordered triple <domain (aka universe),
signature, and interpretation function>. Now, assuming "universe =
world" we have "world != model". QED.