KELLERB@VTCC1.BITNET (Ben Keller) (12/16/89)
I am trying to comprehend the connections between proof theory and the semantics for constructive logic (and how computation fits in here as well). I have been unable to find a clear discussion of these topics. From what I have been able to find on semantics, two forms include classical models with domains of constructive objects (so objects have to be constructed), and the Kripke semantics which can be represented as a poset of classical models (where the ordering represents the relationship between "possible states of knowledge"). The connections to proof are implicit: we must be able to construct (prove the existence of) an object before it can be included in the domain of discourse. Is there any formal statement of the connection between these or any other forms of constructive models and proof theory? Ben Keller Dept of Computer Science Va Tech Blacksburg, Va 24061-0106 kellerb@vtcc1.cc.vt.edu