W3C home > Mailing lists > Public > public-rif-wg@w3.org > May 2010

Re: [FLD] review of Appendix Hebrand Structures

From: Michael Kifer <kifer@cs.stonybrook.edu>
Date: Thu, 6 May 2010 13:17:52 -0400
To: Jos de Bruijn <jos.debruijn@gmail.com>
CC: RIF <public-rif-wg@w3.org>
Message-ID: <20100506131752.34f280f2@kiferdesk>



On Thu, 6 May 2010 09:46:51 +0200
Jos de Bruijn <jos.debruijn@gmail.com> wrote:

> <snip/>
> 
> > 2- In the definition of Herbrand domain, it seems to me that the second
> > and
> > > third bullet are redundant, since they are implied by the first
> >
> > Why? These terms (mentioned in those bullets) are equal according to our
> > semantics. How does it follow that they are equal in Herbrand structures if
> > those bullets are not included?
> >
> 
> They are indeed equal to our semantics, so if t and s are such equal terms,
> then TVal_I(s=t) must be true, so (s,t)\in E, by the first bullet.

ah, ok. Still, I think it is worth reminding, so I made this into a remark
rather than part of the definition.

michael
Received on Thursday, 6 May 2010 17:18:28 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Thursday, 6 May 2010 17:18:28 GMT