Re: Alice knows everything that's true, in ABLP logic

On Sat, 2009-12-19 at 23:28 -0600, Dan Connolly wrote:
> concerning:
> 
> [[(See Lampson et al's authorization calculus for an explanation of
> "speaks for".) The client may therefore conclude that Alice says Alice
> lives next door to Bill. But Alice wouldn't say this, since Alice does
> not know this to be true.
> ]]
>  -- http://www.w3.org/2001/tag/awwsw/http-semantics-report-20091204.html
> 
> One of the axioms in ABLP logic is:
> 
>   s \implies { A says s }.
> 
> So if it's true that Alice lives next door to bill, then
> Alice ABLP:says it. Perhaps I'm confusing an informal
> notion of truth with "logically necessary" or "provable"
> or something, but I don't think so.


Oops; I was confused; thanks, Pat, for the help...
Now that I actually look at the text, I see that it's
only in the case where s is a propositional-logic tautology:

  Axioms. The basic axioms are those for normal modal logics [14]:
  — if s is an instance of a propositional-logic tautology then |- s
  — if s and (s ⊃ s ) then s ;
  ...

http://homepages.inf.ed.ac.uk/gdp/publications/Calculus_for_Access_Control.pdf


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/
gpg D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E

Received on Monday, 21 December 2009 01:04:49 UTC