tag:blogger.com,1999:blog-11295132.post114495564744195558..comments2015-05-30T22:32:59.468-07:00Comments on A Neighborhood of Infinity: A Modal Logic of Near Certainty?Dan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger13125tag:blogger.com,1999:blog-11295132.post-1145332379695092022006-04-17T20:52:00.000-07:002006-04-17T20:52:00.000-07:00theo,Statements in this logic are considered valid...theo,<BR/><BR/>Statements in this logic are considered valid iff their translation into topological terms is true for <EM>all</EM> topologies. The stuff about topology is pretty solid territory as it's all in <A HREF="http://www.illc.uva.nl/Publications/ResearchReports/PP-2006-08.text.pdf" REL="nofollow">here</A> (though I was unaware of this when I started out). It's quite neat. If I get my theorem prover for this logic working (based on <A HREF="ftp://arp.anu.edu.au/pub/techreports/1995/TR-ARP-15-95.ps.gz" REL="nofollow">this</A>) I'll be able to automatically prove statements about interiors and closures of intersections, unions and complements of sets that are true in all topologies.<BR/><BR/>The interpretation in terms of "almost certainty" is mine so it might not hold up.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1145331161011937292006-04-17T20:32:00.000-07:002006-04-17T20:32:00.000-07:00With sigfpe, I'm not worried about Derek's lottery...With sigfpe, I'm not worried about Derek's lottery-paradox-style concerns. This is because I'm pretty comfortable considering "the number of statements in a book" or "the number of people entering a lottery", let alone "the number of people in the world" to be pretty darn close to infinity.<BR/><BR/>Sigfpe, not having actually worked out anything you said, I'd suggest that probably your topology on worlds should be at least Hausdorff. But I'm still worried about []A corresponding to the closure of A: then I easily have situations where both []A and [](-A).<BR/><BR/>Unless I'm misreading you. Are you using [], etc., to express statements about the size of sets of worlds within a certain semantic, or about all possible ways of assigning meaning (the latter being in analogy with your discussion of traditional prepositional logic)? Because, if the latter, then the discrete topology will always provide a system in which []A is only true if A=X.Theohttp://www.blogger.com/profile/10449695704601441213noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1145314574992550202006-04-17T15:56:00.000-07:002006-04-17T15:56:00.000-07:00Kenny,I'm guessing that you'll want some other con...Kenny,<BR/><BR/><EM>I'm guessing that you'll want some other condition</EM><BR/><BR/>I think "K" [](a->b) -> ([]a->[]b), "4" []a->[][]a and "T" []A->A capture everything I want, with <> (instead of []) interpreted as "almost certainly". I think this might actually be a non-trivial novel way to look at this modal logic. I ought to actually try to come up with a theorem to back this up and clarify what I mean by "almost certain" rather than leaving it fuzzy.<BR/><BR/>I've been busy trying to code up a tableau based theorem prover for this system. I <EM>think</EM> I know exactly what I need to implement it.<BR/><BR/>I agree that the lottery paradox is highly relevant here. But thinking about probabilities again: if P(Ai)>1-ε then for any <EM>finite</EM> indexing set, I can choose ε so that the product of all of the P(Ai) is guaranteed to be as close to 1 as I want. On the other hand, if I were to allow quantifiers then this would become an infinite product and I'd no longer be able make this guarantee. In this case Derek's objection would become valid. (I guess I disagree with Derek, the proviso isn't that we work with finite sets but with finite <EM>propositions</EM>.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1145311235730043852006-04-17T15:00:00.000-07:002006-04-17T15:00:00.000-07:00Some of the points Derek is making are related to ...Some of the points Derek is making are related to the "preface paradox" and "lottery paradox" (I've never really been convinced that they're two different paradoxes). The preface paradox points out the following common situation: an author writes a book, and presumably believes every single assertion in that book to high probability. However, she also knows that virtually every longish book has some errors, so in the preface she announces "this book contains at least one false statement" - and believes this to very high probability as well. In the lottery paradox, we note that given a large enough (fair) lottery, I can say of any ticket with certainty 1-ε that it will not win. And yet I can also say with equal certainty that the conjunction of these assertions is false.<BR/><BR/>I think these paradoxes are often attempts to show that belief (or knowledge) is not closed under conjunction, but it might be used also to show that high probability doesn't imply belief, or something else.<BR/><BR/>That's really interesting that you can convincingly give an account of S4 where the box and diamond are switched, with the diamond meaning near certainty! I'm guessing that you'll want some other condition to guarantee that your diamond is stronger than your box, rather than the other way around as is usual.Kennyhttp://www.blogger.com/profile/12226268498253877151noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144990561899338042006-04-13T21:56:00.000-07:002006-04-13T21:56:00.000-07:00Aha! Got it figured out. This modal logic is basic...Aha! Got it figured out. This modal logic is basically topology in disguise. In fact, the theorems <A HREF="http://planetmath.org/encyclopedia/Interior.html" REL="nofollow">here</A> about the interior of a set translate directly into the things I want to be theorems. Some time I'll write up the details.<BR/><BR/>Noticed a mistake too. I want <>A ->A -> []Asigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144977499980980042006-04-13T18:18:00.000-07:002006-04-13T18:18:00.000-07:00Funny, it seems I've been seeing more references t...Funny, it seems I've been seeing more references to Harryhausen all over. Strange.<BR/><BR/>I think your modal logic would have to work for finite sets. I can say that it's almost certain that some person is not the tallest man in the world, but the probability of that statement being true is 5999999999/6000000000, which is very close to 1, but not the same as the limit as some epsilon goes to zero.<BR/><BR/>Maybe you can differentiate probability laws, to see how a change in the "truthiness" of some parameters will bring the proposition closer to or farther from truth?Derekhttp://www.blogger.com/profile/12934077022923410500noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144964407381158512006-04-13T14:40:00.000-07:002006-04-13T14:40:00.000-07:00neel,I'm kicking myself for not seeing the connect...neel,<BR/><BR/>I'm kicking myself for not seeing the connection with monads, even after wondering briefly about applying Curry-Howard. I'll definitely try reading up on lax logic.<BR/><BR/>I think that what I'm after might be close to Lax logic. In particular I want to 'break symmetry' so that [] isn't <> and []a -> <>a but not the converse.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144963971967561772006-04-13T14:32:00.000-07:002006-04-13T14:32:00.000-07:00Also, I should add that IIRC Curry originally inve...Also, I should add that IIRC Curry originally invented lax logic in 1952, but that he didn't publish because he thought it was weird and unnatural. <BR/><BR/>And it's also worth pointing out that in categorical proof theory, if you take a Cartesian closed category you have a model of the simply typed lambda calculus, and then you can get a model of S4 modal logic if you also have a monad and a comonad over that category. The monad models possibility and the comonad models necessity.Neel Krishnaswamihttp://www.blogger.com/profile/09691828772507600568noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144963902304763212006-04-13T14:31:00.000-07:002006-04-13T14:31:00.000-07:00I have some more justification for the [][][]...[]...I have some more justification for the [][][]...[]p=[]p law.<BR/><BR/>Consider calculus. Sometimes we reason about f(x) and f(y) where x and y are close by considering the derivative of f. For example we know that if f is differentiable, and x is close enough to y, then f(y) is close to f(x)+(y-x)*f'(x). They're not usually equal, but close is good enough for practical purposes. So using derivatives allows us to reason about physical quantities that aren't themselves derivatives, as long as we don't try to push our reasoning too far. (And in fact you could probably derive some theorem that specifies just how far y can wander from x before things break down.)<BR/><BR/>Similarly, in real life we don't know that p is "almost certainly true" in the sense I have defined. But we might know that it's 99.9999% sure. In that case, like in the case of calculus, we can assume [][]...[]p=p as an approximation, and as long as we don't push our reasoning too far we won't get bad results. (And in fact you could probably derive some theorem that says just how close your probability must be to 1 before a given formula, proven using the axioms I suggest, containing a certain number of []'s, becomes invalid.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144963756028167802006-04-13T14:29:00.000-07:002006-04-13T14:29:00.000-07:00You definitely need to look at lax logic. It is a ...You definitely need to look at lax logic. It is a logic with a single modality circle (which I'll write as O), and has the axioms that:<BR/><BR/>A => OA <BR/><BR/>OOA => OA <BR/><BR/>A /\ OB => O(A /\ B)<BR/><BR/>This was originally invented by some people doing hardware verification, who wanted a modality of "truth under some constraints". Your modality of "almost certainly" seems like it should be very similar. <BR/><BR/>Amazingly, this modality turned out to be exactly the same as the monadic type constructor of Moggi's computational lambda calculus. In fact, if you look at the first two axioms as types, you can see them as the two natural transformations that make up a monad. <BR/><BR/>However, this is almost, but not quite, the diamond modality -- the main difference is the third axiom. This axiom (Moggi calls it a monad with a <EM>strength</EM>) does not hold for all monads. <BR/><BR/>Rowan Davies and Frank Pfenning did a proof-theoretic analysis of lax/computational logic, and discovered that you can decompose the circle modality as "possibly necessary". That is: <BR/><BR/>OA == <>[]ANeel Krishnaswamihttp://www.blogger.com/profile/09691828772507600568noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144962519112136292006-04-13T14:08:00.000-07:002006-04-13T14:08:00.000-07:00if []A means "almost certain," what is your defini...<EM>if []A means "almost certain," what is your definition of "almost?" Does a probability greater than 50% constitute "almost?"</EM><BR/><BR/>I'm trying to capture an intuition about a <EM>limiting</EM> probability that approaches one. The limit aspect is the central thing. I don't think this is an invalid thing to do. For example you can compute derivatives by using 'infinitesimals' that are smaller than any real number bigger than zero. This can be successfully formalised and even turned into a practical computational technique. So think of "almost certainly true" as being like a probability of 1-e where e is infinitesimal.<BR/><BR/>And I'm pretty sure <>A isn't []A. It might be if [] meant something like "maybe A" because then there's an obvious symmetry between []A and <>A. But by saying that []A is almost certainty I think I'm breaking that symmetry. In fact, intuitively speaking, if I felt that p had a 50% chance of being true I'd say that <>p was true but that []p wasn't.<BR/><BR/><BR/><EM>If you're dealing with probability, then things like []A ^ []B ^ []C ... etc would tend towards P=zero, with a large number of terms.<BR/></EM><BR/>The limit of a finite sum is just the sum of the limits. Or when dealing with infinitesimals any finite sum of a bunch of them still gives you another infinitesimal. So I think that [][][][]... should just be [].<BR/><BR/>And I just posted something in your blog...sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144959753824316512006-04-13T13:22:00.000-07:002006-04-13T13:22:00.000-07:00So can anyone who is knowledgable about these thin...<I>So can anyone who is knowledgable about these things tell me if what I'm trying to do is sensible? </I><BR/><BR/>Forgot to mention... I have no knowledge of these things!Derekhttp://www.blogger.com/profile/12934077022923410500noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1144958658021584552006-04-13T13:04:00.000-07:002006-04-13T13:04:00.000-07:00(I'll use '[]' for the square operator, for diamo...(I'll use '[]' for the square operator, <> for diamond operator)<BR/><BR/>Misc comments (with brainstormy levels of accuracy).<BR/><BR/>- if []A means "almost certain," what is your definition of "almost?" Does a probability greater than 50% constitute "almost?" <BR/><BR/>That's sort of like a "there exists" statement... does just one exist, or a billion?<BR/><BR/>- does []A imply "Always A"?<BR/><BR/>- Gut feeling: []A is same as <>A. <BR/><BR/>- If you're dealing with probability, then things like []A ^ []B ^ []C ... etc would tend towards P=zero, with a large number of terms.Derekhttp://www.blogger.com/profile/12934077022923410500noreply@blogger.com