[ProofPower] type variables in subgoal package

[Roger Bishop Jones]

On Thursday 23 September 2004  4:57 pm, Philip Clayton wrote:
> Roger Bishop Jones wrote:
> >In relation to your comments to Steve about losing
> >the assumptions on things you strip into the assumptions,
> >this is not correct.
>
> I didn't mean losing in that sense.  If you put the theorem |-
> A into the assumptions of the subgoal B ?|- C you get the
> subgoal A, B ?|- C --- exactly the same as if the theorem B |-
> A had been added to the assumptions of B ?|- C. Clearly |- A
> is a stronger theorem than  B |- A but adding either to the
> subgoal B ?|- C has the same effect.  In that sense, some
> information has been lost.  (In particular, the subgoal
> package did not record the fact the |- A is independent of all
> other assumptions, whereas B |- A is not.)

Sorry if I misread you Phil.

I'm afraid I'm still not convinced that there is a material
loss of information which is relevant to the problem under
discussion.

Exactly the same thing would have happened if you had
stripped |- B => A into the assumptions if B was already
an assumption, i.e. you would end up with assumptions A and B.
That's the way the stripping facilities are set up, but we
wouldn't have done it that way if there were any material
loss of information. 

You are right, some information is lost, but none which
is likely to have helped with the proof.
(one can't be sure, sometimes one does find that one
wants for some reason to inhibit stripping).

Thinking about theorems as differing in strength is
likely to be misleading.  You can think about conjectures
as differing in strength, since if |= A => B but |/= B => A
A might be said to be stronger than B.
But if |- A and |- B then |- A <=> B (and of course |= A <=> B)
so all theorems have in that sense, the same strength,
and in particular |- A implies |- A <=> (B => A).

The real root of the problem (if one wants to look
further than the restriction on type instantation)
might be said to be the failure of
the deduction theorem when type instantation
takes place, i.e. we have 

	|- A
	====
	|- A'

where A' is a type instance of A, but can't get
from there to:

	A |- A'
or	|- A => A'

because under the semantics it ain't always so. 

So there are things which you can do by inference
which you can't capture in a theorem, and this
means there are some facts (e.g. polymorphic
ones) which are more powerful (in some sense)
as separate theorems than as assumptions.
(Something similar also happens with free variables.
You can instantiate a free variable in the conclusion
of a theorem, if it isn't free in an assumption,
but if you add the theorem to your assumptions
you won't then be able to specialise it).

Roger Jones