About Logic - Choice vs. Excluded Middle: A Constructive Paradox


I didn't get much of this!  See nlab on Diaconescu-Goodman–Myhill theorem and Wikipedia's Diaconescu's theorem.

My comment: 
 
11:05 FYI I found this very hard to follow. Actually it has so far been impossible for me to follow! I don't know the context of these statements like "a predicate of booleans is a function from bool (Boole?) to prop" I can guess that it means a well-formed formula with a parameter P, say, which when substituted with any well-formed boolean-valued expression produces a well-formed statement of a proposition, i.e. just another boolean-valued expression? But it could also be interpreted extensionally in set theory and the result would be completely different. So what is the sense in which these things are equivalent? The only way I can see to make this meaningful is to restrict to a language where you speak only of how these translations are made. To talk about sets and types as if they exist independently of this seems like madness. [7:50 maybe the context is Lean?! See Richard Clegg Explaining What's Wrong With Computer Science.]
 
Thorsten knows about all of this, but I guess it's just a bit much to explain. See Aczel, P. (1999). On Relating Type Theories and Set Theories. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_1.

Another comment:
 
Quine's notion of confirmational holism applies here, I think. Strictly speaking it is not true that AC implies LEM because you have to take an axiom SYTEM as a whole: if you don't have the axiom infinity then you are OK. The axiom of choice is fine as Thorsten said. Similarly powerset is provable without infinity. The idea of "looking for a problematic axiom" is nonsensical (unless it's infinity😀). 

See About Logic - Analytic and Synthetic Mathematics for more on axiom systems and equivalences.  Russell's famous utterance: "In Mathematics we don't know what we are talking about nor do we care whether or not what we say about it is true." The second part of that may just be a consequence of the first part!

Subscribe to About Logic. 

Comments

Post a Comment

Popular posts from this blog

How Could One Unify CMU and MIT

Image
I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams . This is about practical computing and the cost and feasibility of software development in general. Here is the problem: We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Sc...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more

HTML in Blog Posts

Just testing stuff: SVG You can click on the blue circle: MathML There is not much you can do with this. See Mathematical Markup Language 1.01 Specification   7.1.5 Mixing and Linking MathML and HTML . It's the big problem  of how you compose languages.   a x 2 + b x + c = 0 You can click on the discriminant: x = − b ± b 2 − 4 ⁢ a ⁢ c 2 ⁢ a 2D Canvas Sound  Beep! WebGPU Next level Parser expression grammar compiler:  https://peggyjs.org/online.html Devine Lu Linvega's unxtal assembler/debugger:  https://wiki.xxi...
Read more