Hi John, Cris, Mark, Rob, and Roger,
Before going into the details of John's e-mail on the motivation for HOL Light,
from which I included a larger passage, let me reply to the other comments
concerning the overview at http://dx.doi.org/10./100.111
The following paragraph was added (plus a
Hi Ken,
| John's e-mail on the motivation for HOL Light and his comparison with
| Andrews' systems is highly interesting. I would suggest an article "On the
| Logical Foundations of HOL Light" or similar to make the information
| persistent, as the policy of the mailing list provider may change. F
Andrei,
> On 23 Oct 2016, at 14:31, Andrei Popescu wrote:
>
> Hi Rob,
>
> >> It’s the other way round. Soundness implies that proof-theoretic
> >> conservativity implies model-theoretic conservativity.
>
> Ondra's statement was the correct one.
>
> Let's spell this out, to make sure we are
Hello both,
This may be anecdotal, but I am checkpointing HOL Light with dmtcp 1.2.8
on Ubuntu 16.04.1 and Scientific Linux 6 with no visible problems.
(Haven't managed to make later versions of dmtcp work though.)
Having said that, I would agree a virtual machine is in principle the
better, mo
Andrei,
Here is an "interesting sufficient condition" for model-theoretc
conservativity to entail proof-theoretic conservativity, particularly
relevant to the present discussion:
If in T there is a theorem asserting that an extension is
model-theoretically conservative, in the form required
Hi Rob,
>> It’s the other way round. Soundness implies that proof-theoretic
>> conservativity implies model-theoretic conservativity.
Ondra's statement was the correct one.
Let's spell this out, to make sure we are speaking of the same thing. Say you
have a signature Sigma' extending a signatu
While history of these matters is topical, I thought I might describe
the origin of this facility and the practical rationale for
conservativity at that time.
My memory is not completely reliable, so there might be something here
which I have misremembered but I think the main features will be g
Ondrej,
> On 22 Oct 2016, at 20:07, Ondřej Kunčar wrote:
>
> Hi Rob,
> you are right that we mention only the plain definitions in HOL and not
> the implicit ones, when we compare the definitional mechanism of HOL and
> Isabelle/HOL. (If this what you meant; I assume you didn't mean to say
>
