The higher cardinality interpretation of `qubit`
Jen had the idea of effective cardinality being built into the logic of qubit. This got me thinking.
From one perspective, the propositional arguments of a proof might be thought of as having some kind of "singular frequency". Each singular frequency identifies an argument. When forming expressions, one is creating new signals which might have multiple frequencies.
E.g.
a, b:
and(a, b)
The truth table is:
a b and(a, b)
0 0 0
0 1 0
1 0 0
1 1 1
When repeating the truth table infinitely, one can see how a and b are repeating versus and(a, b). Their relations are similar to how a continuous signal might be decomposed into sine waves using the Fourier transform.
When using qubit, the argument a to qubit(a) might be interpreted as a projection from a finite cardinality to a higher cardinality:
qubit : ℕ -> 2^ℕ
With other words, 2^ℕ might be thought of as the set of random propositions. This is an interesting perspective on the continuum hypothesis, because it provides an interpretation of 2^ℕ without assuming it is continuous or not.
This idea also maps very well into stuff like The Mathematics of Infinite-Things-Space. Here, higher cardinalities being "forced into" the discrete structure of natural numbers might be thought of as a way of constructing a continuum.
I am not sure whether qubit^2 : 2^ℕ -> 2^(2^ℕ) or qubit^2 : 2^ℕ -> 2^ℕ.
This might be interpreted as a refinement type.