FOM: organizing; Boolean rings; signature

[Till Mossakowski]

Vaughan Pratt wrote:
>From: Till Mossakowski <till at Informatik.Uni-Bremen.DE>
>>Lawvere theories and monads are indeed more complex than standard signatures.
>
>Certainly anyone who's worked with standard signatures long enough finds
>them not at all complex ("what else could you possibly use instead?").
>
>But those who've worked with Lawvere theories for a comparable length of
>time are likely to disagree with you, even if they've spent the same
>amount of time with signatures.
>
>Merely saying that something is a category seems automatically to make
>it seem a more complex notion, regardless of whether it actually is
>complex or not.

I have worked with both Lawvere theories and standard algebraic signatures.
OK, I agree. Lawvere theories are indeed not more *complex* than 
ordinary algebraic signatures. But they are more *abstract*.
Sometimes, this abstractness is desirable, because almost all
interesting properties can be formulated at the abstract level,
and the concrete level of signatures makes distinctions that
are not relevant.
But often you still need traditional algebraic signatures.
Namely, if you want to give some *presentation*, do proofs
with that presentation, or want to do an implementation.

That's why I suggested not to replace signatures with Lawvere theories,
but view them complementary, as the "signed theories" do.
There are many signed theories, having the same underlying
Lawvere theory as Boolean algebra, but different algebraic
signatures. Both the sameness of the Lawvere theory matters,
as well as the possibility to have different signatures inducing it.
For example, in circuit theory, you can choose different sets of basic
circuits, corresponding to different signatures, but all being
functionally complete wrt. Boolean algebra, i.e. inducing the
same Lawvere theory.


Till Mossakowski