[Haskell-cafe] A model theory question

[Patrick Browne]

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?

See:
http://books.google.ie/books?id=Q0H-n4Wz2ssC&pg=PA41&lpg=PA41&dq=model+expansion+cafeobj&source=bl&ots=_vCFynLmca&sig=07V6machOANGM0FTgPF5pcKRrrE&hl=en&ei=YkSgTPn0OoqOjAfb0tWVDQ&sa=X&oi=book_result&ct=result&resnum=1&ved=0CBgQ6AEwAA#v=onepage&q=model%20expansion%20cafeobj&f=false

Thanks,
Pat

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