On 21/03/17 07:43, Ralf Hemmecke wrote:
On 03/21/2017 08:34 AM, Martin Baker wrote:
In ILogic T and _|_ are required as top and bottom of lattice.

In Boolean I guess they should give true and false?

Certainly, because these are the only values in Boolean.

I think its only when logic becomes algebraised (when we have symbols
for logical variables) that we need to make a distinction between
top/bottom and true/false.

Sorry, but I don't understand this. What algebra do you mean so that T()
and true are both values of the domain that are not the same? Not that
if they are not equal then true cannot be at the top of the lattice.

What I'm trying to say is that in, say, intuitionistic logic we have
variables (in the mathematical sense - can range over all values). For
example, proposition("a") here:

(1) -> proposition("a") /\ logicT()

    (1)  a
                                   Type : ILogic
(2) -> proposition("a") /\ logicF()

    (2)  _|_
                                   Type : ILogic

I don't think it would be correct for this to return 'false'.

On 21/03/17 08:05, oldk1331 wrote:
> I meant how to call these two functions?
>
> Besides, ")dis op T" doesn't return this signature, maybe
> 'T' conflict with lisp symbol 'T'?
>
> Also, _|_ can't be called, maybe FriCAS lexer don't recognize it?
>
> If so, change their name to top/bottom is more appropriate.

OK you are just talking about a lexer issue which I can't answer. As a general principle though I think it would be good to use _|_ for input/output wherever possible. Or unicode would be even better. In the above example I think its much clearer that _|_ is a special value 'bottom' could just be a variable name.

Martin B

--
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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.

Reply via email to