I see now that my sketch proof of "completeness" for Rob
Arthan's proposed new "new_specification" cannot be turned
into a rigorous proof.
When withness are obtained using the choice function, they
may fail the fourth of his specified constraints on the
witnesses. They will do so in just the
On 28 Apr 2012, at 16:17, Roger Bishop Jones wrote:
> On Saturday 28 Apr 2012 13:14, Rob Arthan wrote:
>
>> On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote:
>>> Is the revised new_specification "complete"?
>>> i.e. are there any conservative extensions which cannot
>>> be achieved by it?
>>>
On Sunday 29 Apr 2012 11:11, Rob Arthan wrote:
> > The question I was asking was rather more mundane.
> > Given that we know what it means to say that some
> > proposition P is conservative over a given theory in
> > HOL (in the proof theoretic sense), the question is
> > "is there any proposition
Roger,
On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote:
> Is the revised new_specification "complete"?
> i.e. are there any conservative extensions which cannot be
> achieved by it?
> (an argument for this would strengthen the case)
I would be rather surprised if there were any nice c
On Saturday 28 Apr 2012 13:14, Rob Arthan wrote:
> On 28 Apr 2012, at 09:53, Roger Bishop Jones wrote:
> > Is the revised new_specification "complete"?
> > i.e. are there any conservative extensions which cannot
> > be achieved by it?
> > (an argument for this would strengthen the case)
>
> I wou
Is the revised new_specification "complete"?
i.e. are there any conservative extensions which cannot be
achieved by it?
(an argument for this would strengthen the case)
In the context of the revised new_specification how do we
stand in relation to conservative introduction of type
constr
On 25 Apr 2012, at 14:03, Ramana Kumar wrote:
> Looks like interesting conversations. Congratulations on doing such a great
> job of writing them up! I would be more than happy to fix the relevant
> OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light
> adopt this proposal.
Looks like interesting conversations. Congratulations on doing such a great
job of writing them up! I would be more than happy to fix the relevant
OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light
adopt this proposal.
One small comment: in the description of the revised new_
Conversations with Mark Adams and John Harrison at the Milner Symposium earlier
last week inspired me to think through a new approach to defining constants in
HOL. This generalises what was done in early versions of HOL Light. It
constitutes an adjustment to new_specification that supersedes new
