On Thursday, February 28, 2019 at 10:54:28 AM UTC-6, Bruno Marchal wrote: > > > On 27 Feb 2019, at 19:18, Philip Thrift <cloud...@gmail.com <javascript:>> > wrote: > > > > On Wednesday, February 27, 2019 at 11:25:06 AM UTC-6, Bruno Marchal wrote: >> >> >> On 26 Feb 2019, at 19:41, Philip Thrift <cloud...@gmail.com> wrote: >> >> >> >> There is another approach vs. the JD Hamkins / set theory & mathematical >> logic (math dept.) approach. the one of Martin Escardo / type & programming >> language theory (computer science dept.). >> >> Martin Escardo >> http://www.cs.bham.ac.uk/~mhe/ >> >> *higher-type computation = * >> >> *sets that can be exhaustively searched by an algorithm, in the sense of >> Turing, in finite time, as those that are topologically compact* >> >> >> ? >> >> If it is an algorithm in the sense of Turing, and if the search is >> required to be finite, then the set is finite. >> > > > > In any case, there is programming he has written > > M.H. Escardo. *Infinite sets that admit fast exhaustive search*. > > > In that sense, there is no problem. The universal dovetailer exhaust all > computations with all oracles in that sense. > > > > > In LICS'2007, IEEE, pages 443-452, Poland, Wroclaw, July. > > pdf <https://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf> (paper), hs > <https://www.cs.bham.ac.uk/~mhe/papers/exhaustive.hs> (companion Haskell > program extracted from the paper > > from https://www.cs.bham.ac.uk/~mhe/papers/ > > > One could say: *There is nothing outside the code.* > > (The program stands on its own.) > > > > > Programs can’t do that when becoming inputs to universal programs. You > can’t escape truth so easily, even if you can’t define it. All Gödel-Löbian > machines know that. There is definitely something outside the code, if > there is a code. And that is the many universal codes which gives the > behaviour and the experience to the person attached to their infinitely > many codes in arithmetic. But the laws of physics must be derived from > this, and by using the self-reference logics of Gödel-Löb-Solovay (G*), we > get the qualia as supplementary gifts, in the form of immediate “volume” > type of truth that we cannot prove, nor define, yet indubitably known. > > Bruno >

We have only scratched the surface of the subject of *Semantic*s (of code) in PLT. *PLT: A path to enlightenment in Programming Language Theory* https://steshaw.org/plt/ - pt -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.