Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!ucbvax!VTCC1.BITNET!KELLERB
From: KELLERB@VTCC1.BITNET (Ben Keller)
Newsgroups: comp.theory
Subject: proof theory, semantics of constructive logic, and computation
Message-ID: <C-249.THEORYNT@ibm.com>
Date: 15 Dec 89 20:10:03 GMT
Sender: daemon@ucbvax.BERKELEY.EDU
Reply-To: Ben Keller <KELLERB%VTCC1.BITNET@VM1.NoDak.EDU>
Lines: 21


        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