In CoqId I have entered Variables s p e t f: Type.
I now want the set of elements which interpret terms of type e
to have the structure of a Complete Atomic Boolean algebra. Of course, for this to be the case we need there to be a bottom element BOT and a top element TOP amongst the set of elements which interpret terms of type e
. That is, the set of elements which interpret terms of type e
must form a Boolean algebra where every subset of it must have a join (a supremum), and where for any element of this Boolean algebra which is not BOT, there is an element c which is not BOT and which is such that it is not the case that there is an element d which is not BOT and such that c is below d in the ordering of the Boolean algebra.
I realise these are semantic conditions on the interpretation of terms, with c,d BOT and TOP being the model-theoretic interpretation of terms of type e
.
My question is then what I need to do in CoqId in order to make sure that the terms of type e
behave in such a way that the set of elements which are model-theoretic interpretations them form a Complete, Atomic Boolean algebra. I suppose I will need a term denoting BOT and a term denoting TOP, an ordering relation amongst terms of type e
, an operator which forms the sum of an arbitrary subset of terms of type e
and a negation operator on terms of type e
.
If any of you have any ideas, I would be very interested.
I feel that the answer to this question is that I needn't worry about this in CoqId, since these are model-theoretic conditions on the interpretation of types. Rather, all I need are terms in Coq which represent sum, the top element, the bottom element and negation on type e
, and then it is left to model theory to bother about the interpretations of these terms being a complete, Atomic Boolean algebra. Is that right?