0

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?

1 Answer 1

1

You are indeed right: what you probably want is to axiomatize the atomic boolean algebra structure on e, i.e. assume that there are various constants such as bot : e, a relation le_e : e -> -> Prop. But if you want to reason internally in Coq, you might also want to axiomatize the atomic boolean algebra structure, for instance assume an axiom bot_is_bot : forall x : e, le_e bot x, and similarly for all other properties of the structure you want to look at. That way, a model of your theory has to be an atomic boolean algebra, because it has to interpret all the axioms, which exactly correspond to having this structure.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.