Martin Baker wrote:
>
> Waldek,
>
> I see that you have added default 'T()' and "_|_" in Logic.
>
> It just seems a bit wasteful to hardwire the two notations to be exactly
> the same. Where one seems to be logic terminology and the other seems to
> be lattice terminology:
>
> T == true
> ___|__ == false
>
> especially since, in denotational semantics, we may want them to mean
> different things at the same time:
>
> T
> / \
> / \
> true false
> \ /
> \ /
> _|_
>
>
> I think it is in ILogic (intuitionistic logic) that the clash is
> strongest because, in the above diagram 'T' represents a contradiction,
> in ILogic 'false' often represents a contradiction. So would it make
> more sense to connect the two notations which represent contradiction
> like this:
>
> T == false
> ___|__ == true
>
> If this is the wrong way round then I realise this is my fault as that
> is what I did originally. Its just that I like to draw 'true' at the top
> because it makes /\ and \/ (meet and join) look right in diagrams:
>
> A B
> \ /
> \ /
> (A \/ B)
>
> But perhaps its more important that the notation for contradiction
> should coincide?
AFAICS anything deserving to be called Logic should have 'true' as
top of lattice and 'false' as bottom. You may embed logical values
into bigger latice like in case of denotational semantics, but
this is not _lattice embedding_. To put it differently, with
current definitions 'T' and '_|_' may be used in lattice context
and differ from 'true' and 'false'. We may change the structure
in the future, for example we may decide to separate Logic
from lattices. But currently this is minimal change to
get some consistency.
--
Waldek Hebisch
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
