User loginNavigation 
Dedekind, Cantor, Conway, & Hewitt (w/ some Chomsky)Here, I will attempt to cool down controversy on LtU over Hewitt's construction of Real by explaining it in more familiar terms. I think this will help to shed some light on Direct Logic and begin to hint why it is interesting in a PLT context. I will borrow conceptually from John H. Conway who wrote, in "On numbers and games":
Hewitt can be read as constructing Real by specifying a set of 3way partitions of the dyadic fractions between 0 and 1. Every Real in [0..1] corresponds to three sets: {L  M  R} The sets are ordered so that no member of L is greater than or equal to any member of M or R, no member of M is greater than or equal to any member of R. Zero: 0 ≡ {{}  {}  Dyad} where Dyad is the set of all dyadic fractions between 0 and 1 One: 1 ≡ {Dyad  {}  {}} Hopefully the dyadic fractions are themselves members of Real and we can memorialize that fact in a manner similar to Dedekind: ∀d ∈ Dyad, {d_{l}  { d }  d_{r} } ∈ ℝ where d_{l} ≡ { x ∈ Dyad  x < d } and d_{r} ≡ { x ∈ Dyad  x > d } Note: the Real {d_{l}  { d }  d_{r} } is called d. The rationals in general correspond to regular languages as follows: Let Rat be the set of of sets of finite strings of 0 and 1 such that: ∀r in Rat, r is a regular language r is well ordered by a prefix relation ∀s in r, s is finite length and ends with 1 r_{l} ≡ { d ∈ Dyad  ∃x ∈ r, x > d } r_{m} ≡ { d ∈ r  ∀x ∈ r, x <= d } r_{r} ≡ { d ∈ Dyad  ∃x ∈ r, x < d } Note: the Real { r_{l}, r_{m}, r_{r} } is called r } As you can see, the subset of Real given by Rat is the set of all rational fractions between 0 and 1. The rationals are given by certain regular languages over the alphabet {0,1}. Similarly, the constructible reals are given by certain recursivvely enumerable languages. Let Tructable be the set of all recursively enumerable sets of finite strings of 0s and 1s, each string ending with a 1, such that each member of Tructable is well ordered by a prefix relation. By analogous construction to the rationals: ∀ t ∈ Tructable, { t_{l}, t_{m}, t_{r} } is in Real All rationals (dyadic and otherwise) are Tructable. Finally, we consider a set of languages of finite strings for which the generator functions are nondeterministic. Let Fracs be the set of all sets of finite strings of 0s and 1s, each string ending with a 1, such that each member of Fracs is well ordered by a prefix relation. By analogous construction, ∀ f ∈ Fracs, { f_{l}, f_{m}, f_{r} } is in Real Note that if a member f of Fracs has a maximal element, then f is also a dyadic rational. Note that if a member f is a regular language over {0,1}, then it is a rational. Note that if a member of f is a recursively enumerable set, then it is a tructable real. There are other possibilities. By a diagonalization argument, we know that Fracs contains members f which are not recursively enumerable. Those f are the unconstructible reals. Let's suppose that the real world contains fair randomness. For example, there is a coin flip or some other kind of measurement we can repeat that will produce random outcomes. Neither heads or tails will be permanently starved. A sequence of coinflips on a given worldline will eventually produce both a 0 and a 1. Furthermore, on some worldlines, the sequence of coin flips is not described by any recursively enumerable function (at least assuming that there is no upper bound on the number of times we get to flip the coin). The number of possible worldlines on which coin flips might be recorded is uncountable and, indeed, corresponds nicely to the members of Fracs. In other words, a machine can enumerate the members of any f in Fracs, from shortest to longest. Such a machine, on a particular worldline, is pretty much what Hewitt means by an "Actor address". By Thomas Lord at 20150622 20:53  LtU Forum  previous forum topic  next forum topic  other blogs  2452 reads

Browse archivesActive forum topics 
Recent comments
1 hour 47 min ago
3 hours 5 min ago
3 hours 50 min ago
4 hours 14 min ago
4 hours 24 min ago
5 hours 23 min ago
5 hours 44 min ago
6 hours 55 min ago
15 hours 29 min ago
16 hours 1 min ago