The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Very likely my name for the type is wrong; allow me to clarify.

Void in current parlance is an uninhabited type - I know that. We're
not trying to build the world out of False, I used the wrong name for
something that is new. This void, for lack of a better word, would be
better named vacuity, is a sort of inhabited immutable singleton
consisting with some associated properties. Vacuity exists and should
be a type in our lexicon, similar to the way that void expresses the
uninhabited type but is still a meaningful identifier that corresponds
to something that actually is. Vacuity is still a thing, and it is
distinct from void; it might be also the type that admits no other,
but then I'm thinking of the physics reading that I've been doing and
I'm trying to explain behaviors in physics with a type.

I was thinking that substitution might be something that can be easily
encoded with vacuity, since by preservation of its invariant
definition it forces a sort of exchange of any size, kind or type of
variable.

Suppose you wanted to design, from precise definition of nothingness -
perfect nothingness - countability and computability, dimensions and
so on. It's hard to clarify precisely what this is, because I don't
know if my vacuous space is sufficiently vacuous or precisely well
defined. Is it meaningful to pursue this?

On Fri, Dec 9, 2016 at 1:22 PM, Kenneth Adam Miller
<kennethadammiller AT gmail.com>
 wrote:
> Hello,
>
>
> Lately I've become interested in the idea of a fundamental void while
> reading a lot about quantum mechanics. Basically, my idea is that, if you
> could codify the definition of void down into a few properties, you might
> have something from which to construct dimensions and measure with respect
> to one another. I tried hard to describe the motivation behind this to a
> friend but I got some really smarmy replies. So I wondered if my intuition
> was totally bunk.
>
> The motivation behind this is to explain fundamentally why the commutator
> between two basis vectors must be zero in order to conclude that they are
> orthogonal to one another, and also how the means that quantum decoherence
> can result in instantaneous communication across any distance by
> constructing computation/countability with respect to this and subsequently
> clarify the manifestation of entanglement as an outcropping of this notion.
>
> I tried to explain that I was thinking of void as being this uninstantiated
> and unobservable entity, a kind of epitome of "that which cannot be", and to
> assert that although one cannot interact directly with such a void, you can
> encode other computations and numbers with respect to the original
> fundamental notion of void. So, I tried to say that that was orthogonal by
> definition, but that the lack of intractability or observability would lead
> you to conclude that you could not distinguish any one from another. As a
> consequence of this definition you cannot create anything anew, but can
> references, and can "merge" the encodings around these references. Then I
> wanted to define encoding as being the merge rules that are equal to
> substitution with one or more of these references.
>
>
> I hope this doesn't sound crazy, but I've really been thinking about this a
> lot-void is not false, and I'm not building the world out of false. But I
> can encode false as a contextually interpretable construct around void. I
> wanted to say that, a perfectly constructed definition of void would require
> by construction instantiable orthogonality. So, supposing you wanted to
> build infinity or a dimension; you'd go about it by recursively compounding
> the semantics of operation. So, you'd have plus, multiplication,
> exponentiation, and so on, and you'd have a kind of back reference of the
> same encoding so that, in each step you would extend both the substitution
> and the operation for the step. In addition, what's great about this is that
> it allows orthogonal computations to freely continue without obstruction by
> mere structure, and that it there can be more than one operation in each
> substitution operation.
>
>
> All of this is what I'm putting together by means of intuition and memory of
> what I've read about computability and me just trying to combine it in my
> head, thinking of it visually, sort of. But it's really really difficult to
> nail down what I think is a missing other property and its consequence. Has
> anybody read about a definition of perfect void beneath the quantum level? I
> think it would make an excellent semantic primitive for constructing the
> behaviors of quantum particles as well.
>