[Haskell-cafe] A model theory question

Patrick Browne patrick.browne at dit.ie
Mon Sep 27 03:25:24 EDT 2010

Alexander Solla wrote:
>  On 09/26/2010 01:32 PM, Patrick Browne wrote:
> Bigger how?  Under logical implication and its computational analogue? 
> That is to say, do you want the model to be more SPECIFIC, describing a
> smaller class of objects more richly (i.e, with "more" logical
> implications to be made) or do you want the model to be more GENERAL,
> and contain the less specific submodels?  This is how "forcing" works.

My idea of bigger is based on the import modes and parameterized modules
of the Maude/CafeOBJ languages, where smaller theories are used to
construct larger theories (and/or objects). In these languages I guess
theories (loose specifications or interfaces) correspond to your
*logical implication* and objects (or tight specification) correspond to
*computation* at the ordinary programming level. The axioms of the
theories must hold at the programming level.

What does the term *forcing* mean?



This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie

More information about the Haskell-Cafe mailing list