Re: [FLD] review of Appendix Hebrand Structures

OK, sounds good to me.

Cheers, Jos

On Thu, May 6, 2010 at 7:17 PM, Michael Kifer <kifer@cs.stonybrook.edu>wrote:

>
>
>
> 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
>



-- 
Jos de Bruijn
 Web:          http://www.debruijn.net/
 LinkedIn:     http://at.linkedin.com/in/josdebruijn