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 <javascript:>> 
> wrote:
>
>
>
> On Tuesday, February 26, 2019 at 5:07:38 AM UTC-6, Bruno Marchal wrote:
>>
>>
>> On 25 Feb 2019, at 20:35, Philip Thrift <cloud...@gmail.com> wrote:
>>
>> via
>> https://twitter.com/JDHamkins/status/1100090709527408640
>>
>> Joel David Hamkins   @JDHamkins
>>
>> *Must there be numbers we cannot describe or define? Definability in 
>> mathematics and the Math Tea argument*
>> Pure Mathematics Research Seminar at the University of East Anglia in 
>> Norwich on Monday, 25 February, 2019.
>>
>>
>> Abstract:
>>
>> *An old argument, heard perhaps at a good math tea, proceeds: “there must 
>> be some real numbers that we can neither describe nor define, since there 
>> are uncountably many real numbers, but only countably many definitions.*
>>
>>
>>
>> But that argument is rather weak, as the notion of cardinality is a 
>> relative notion, depending of the model (not the theory) that we might use. 
>> There are countable models of Cantor’s theory of set and the transfinite 
>> (cf the paradox of Skolem). If you agree o identify a real number with a 
>> total computable function (from N to N), as Turing did originally, then you 
>> can prove the existence of specific non definable real number, in any rich 
>> enough extension of any essentially undecidable theory.
>>
>> It is very simple, any theory reich enough to define a universal 
>> machine/number, is automatically essentially undecidable. It is a generator 
>> of infinitely many surprises for *any* machines and super-marching, etc. We 
>> know now that we know basically nothing, with such “rich” theories. 
>> Elementary arithmetic is already essentially undecidable.
>>
>> You can change the logic, and will get quite different view on the real 
>> numbers. In brouwer’s intuitionistic logic, and in the effective topos 
>> (which generalises Kleene’s realisability notion, and is based on the 
>> category of partial combinatory algebra): we have that all real number are 
>> computable, and all functions are continuous. I am not sure if we get that 
>> all real numbers will be definable, though. They might be not-not-definable 
>> ...
>>
>>
>>
>> *” Does it withstand scrutiny? In this talk, I will discuss the 
>> phenomenon of pointwise definable structures in mathematics, structures in 
>> which every object has a property that only it exhibits. A mathematical 
>> structure is Leibnizian, in contrast, if any pair of distinct objects in it 
>> exhibit different properties. *
>>
>>
>> x ≠ y ->. Ax ≠ Ay, that is Ax = Ay ->. x = y. That is the axiom of 
>> extensionality (in Combinators, lama calculus, set theories).
>>
>> I have used it in the elimination of variables in the combinations. It is 
>> a god’s gift, as it leads to simple efficacious combinators. It is, with 
>> the combinators, equivalent to [x](Ax) = A, when A has no free occurence of 
>> x. Not to be confuse with ([x]A)x = A (which is always true, and just 
>> defines what elimination of x means). 
>>
>>
>>
>> *Is there a Leibnizian structure with no definable elements? *
>>
>>
>> Yes. The classical reals, or the classical set of total computable 
>> functions.
>>
>>
>>
>> *Must indiscernible elements in a mathematical structure be automorphic 
>> images of one another? *
>>
>>
>> No. If we cannot discern them, we cannot build a morphism between them. I 
>> would say.
>>
>>
>> *We shall discuss many elementary yet interesting examples, eventually 
>> working up to the proof that every countable model of set theory has a 
>> pointwise definable extension, in which every mathematical object is 
>> definable.*
>>
>>
>> http://jdh.hamkins.org/must-there-be-number-we-cannot-define-norwich-february-2019/
>>
>> Lecture notes:
>>
>> http://jdh.hamkins.org/wp-content/uploads/2019/02/Must-every-number-be-definable_-Norwich-Feb-2019.pdf
>>
>>
>> I will take a look, but that does not make much sense, unless the logic 
>> is weakemed in some way. In some intuitionist set theory with choice, it 
>> might make sense.
>>
>> Bruno
>>
>>
>>
>>
> 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 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.)





 

>
>
>
>
>
>
> *constructive mathematics, which I see as a generalization, rather than as 
> a restriction, of classical mathematics. *
>
>
> Hmm…. That is highly debatable, and usually, when made rigorously, it is 
> akin to a form of solipsism. 
>
> When a theory has less axioms, it has more models. So generalisation and 
> particularisation are permuted when we go from theory to model and vice 
> versa. But in arithmetic and analysis, things are more complicated. In the 
> Kleene realisability semantic for Intuitionist logic, (or in the effective 
> topos) we can have theorem which are classically false, for example. 
>
>
>
> *In constructive mathematics, in the way I conceive it, computation is a 
> side-effect, rather than its foundation.*
>
>
> Computation is a side effect of both classical arithmetic and intuitionist 
> arithmetic.
>
> Classicalism and Intuitionism differ only “really” on the real numbers and 
> analysis. With just arithmetic, it is mainly a change of vocabulary. I am 
> aware we can add nuances, but most makes not much sense in any serious 
> computationalist machine theology, were the main axiom has to be highly 
> non-constructive. But then physics get constructive defined, and do the 
> theology of the machine can be tested.
>
>
>
>
> *What distinguishes classical and constructive mathematics is that the 
> latter is better equipped to explicitly indicate the amount of information 
> given by its definitions, theorems and proofs, which is related to topology 
> and domain theory.*
>
>
> OK.
>
>
>
>
> * The correct question is not whether a mathematical theorem is 
> constructive, but instead how much information its formulation (type) and 
> proof (inhabitant of the type) give. A good foundation has a rich supply of 
> types and ways to build their inhabitants so that the available amount of 
> information can be precisely expressed.*
>
>
> Types are for applications. Reality is arguably untyped. With mechanism, 
> we recover intuitionism as the normal phenomenology of the machine, and 
> yes, she cannot live without types, locally, but for the fundamental 
> reality, mechanism requires the abandon of types, or, at the least, a 
> universal type, like the type of a universal machine when added to a typed 
> world.
>
> You allude to the Curry Howard isomorphism, which is very beautiful, but 
> do not extend so nicely to classical logic (as Krivine claims to have 
> succeeded, but I am not convinced). Nor Kleene realisability (despite my 
> very deep appreciation). It is normal, the notion of “other minds” makes no 
> sense in constructive mathematics, or philosophy. Brouwer mocked his 
> students who claim to love his course. He asked them, why do you love that 
> when it shows that you don’t exist … 
>
> Bruno
>
>
>
>
> - 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.

Reply via email to