[opentheory-users] article format wording about constants

[Rob Arthan]

Ramana, Joe,

> On 15 Jan 2011, at 21:50, Ramana Kumar wrote:
> 
>> On Sat, Jan 15, 2011 at 9:41 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> On Sat, Jan 15, 2011 at 9:13 PM, Joe Hurd <joe at gilith.com> wrote:
>>>> Hi Ramana,
>>>> 
>>> 
...
>>> Applying the type instantiation ('a |-> bool) to both results in
>>> 
>>> |- !(v : bool list) (v' : bool list). P (v : bool list) (v' : bool list)
>>> 
>>> |- P (c : bool list) (c : bool list)
>>> 
>>> where the two constants have been identified, but the two variables
>>> have been kept separate.
> 
> This is not true in HOL4.

...

And then:

On 15 Jan 2011, at 23:17, Joe Hurd wrote:

> Hi Ramana,
> 
> The example I gave make deliberate use of the universal quantifiers to
> illustrate my point about variables being determined by both name and
> type. As you found out, without any binders HOL4 does indeed identify
> the variables, but this can be seen as a 'forced additional
> specialization': it is always sound to identify free variables in a
> theorem but a logical weakening may occur as a result.

Yes: ProofPower's type instantiation rule soundly (although perhaps confusingly) will rename one of the variables in Joe's example.

However, there are cases where renaming bound variables is logically necessary. E.g., the following is a theorem because the term beta-reduces to !y:'a.1 = 1:

|- !y:'a. (\(x:num)(x:'a). x = 1) 1 y

Instantiating 'a to num without renaming would result in a term that beta-reduces to !y:num.y = y and that's false. This has been an unsoundness bug in several implementations of the logic, but I believe they are all fixed now.

Regards,

Rob.