[ProofPower] type variables in subgoal package

[Roger Bishop Jones]

On Thursday 23 September 2004  5:03 pm, Roger Bishop Jones wrote:

> The reason why the logic does not allow instantiation
> of the conclusion without instantiation of the assumptions
> is because it is not sound. If you could you would be
> able to derive a contradiction by starting with
> asm_rule of "there is exactly one object of type 'a"
> then instantiate 'a in the conclusion to BOOL and prove
> that the conclusion is False, then discard the

I should have said "discharge" here.

> assumption and instantiate 'a to "one"
> and prove that the hypothesis is true, yielding
> a proof of T => F, which is false, from which all
> else follows.

Roger Jones