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  2723 reads

Browse archivesActive forum topics 
Recent comments
17 hours 13 min ago
19 hours 22 min ago
1 day 2 hours ago
1 day 7 hours ago
1 day 7 hours ago
1 day 9 hours ago
1 day 16 hours ago
1 day 18 hours ago
1 day 21 hours ago
1 day 21 hours ago