Re: [Hol-info] Free variable natural language translation..

[Tony J. <ton...@co...>]

Well, compare this example with.

- val stmt4 = try mk_thm([],``?a_female_person.(Is_female:'a->bool) 
a_female_person``);
 > val stmt4 =  [] |- ?a_female_person. Is_female a_female_person : thm

- val stmt5 = try ASSUME ``(Is_female:'a->bool) a_female_person``;
 > val stmt5 =  [Is_female a_female_person] |- Is_female a_female_person 
: thm

- val stmt6 = try EXISTS  (``?a_female_person.(Is_female:'a->bool) 
a_female_person``,  ``a_female_person:'a``) stmt5;
>  val stmt6 =
     [Is_female a_female_person]   |- ?a_female_person. Is_female 
a_female_person : thm

- val stmt7 = try CHOOSE (``a_female_person:'a``,stmt4) stmt6;
 > val stmt7 =  [] |- ?a_female_person. Is_female a_female_person : thm


With this one

- val stmt4 = try mk_thm([],``?some_person.(Is_female:'a->bool) some_person``);
> val stmt4 =  [] |- ?some_person. Is_female some_person : thm

- val stmt5 = try ASSUME ``(Is_female:'a->bool) Sarah``;
> val stmt5 =  [Is_female Sarah] |- Is_female Sarah : thm

- val stmt6 = try EXISTS  (``?some_person.(Is_female:'a->bool) some_person``,``Sarah:'a``) stmt5;
> val stmt6 =  [Is_female Sarah] |- ?some_person. Is_female some_person : thm

- val stmt7 = try CHOOSE (``Sarah:'a``,stmt4) stmt6;
> val stmt7 =  [] |- ?some_person. Is_female some_person : thm


My question is "Which one is using the semantics of free variables 
correctly?".

Because in the former, the free variable is "some person who has the 
property of being a female."  But in the latter, the free variable is "a 
specific person who has the name Sarah (and say she has the SSN of 
999-99-9999, so we can consider her a unique individual)."  My thinking 
is that the first example is the correct one, but I want to be sure.


Thanks,

Tony



Rob Arthan wrote:

>On Friday 30 Sep 2005 1:32 am, Tony Johnson wrote:
>  
>
>>My question is whether or not the following is semantically correct..
>>
>>show_assums := true;
>>- val stmt4 = try mk_thm([],``?some_person.(Is_female:'a->bool)
>>some_person``);
>>
>> > val stmt4 =  [] |- ?some_person. Is_female some_person : thm
>>
>>- val stmt5 = try ASSUME ``(Is_female:'a->bool) Sarah``;
>>
>> > val stmt5 =  [Is_female Sarah] |- Is_female Sarah : thm
>>
>>- val stmt6 = try EXISTS  (``?some_person.(Is_female:'a->bool)
>>some_person``,``Sarah:'a``) stmt5;
>>
>> > val stmt6 =  [Is_female Sarah] |- ?some_person. Is_female some_person
>>:
>>: thm
>>
>>- val stmt7 = try CHOOSE (``Sarah:'a``,stmt4) stmt6;
>>
>> > val stmt7 =  [] |- ?some_person. Is_female some_person : thm
>>
>>Is the above kosher?
>>    
>>
>
>If you mean "is it valid?", then yes. The CHOOSE inference (= existential 
>elimination) just goes round in circles if the antecedents have the form |- 
>!x.p x and p v |- !x.p x.
>
>  
>
>> Or am I misunderstanding the meaning of free
>>variables...
>>    
>>
>
>Without knowing what you think might be wrong about the example, I can't say.
>
>Regards,
>
>Rob.
>
>  
>