HN doesn't allow comments with multiple parents, so I needed to choose one to reply to. ihm, please consider this comment also a reply to yours.
The more I talk about constructivism the less I feel it's adequate to label what I'm talking about, even though my approach to mathematics is completely constructive. Please don't treat every word I use as totally definite.
Mathematics is the science of formal reasoning. I call the rules of reasoning, that is the rules of manipulation of statements including their lexicon, syntax and semantic, a logic. I see intuitionistic logic as the most intuitive, universal and fruitful logic, in short: the logic.
To reason, we need something to reason about. Said somethings should be respresentable, so we can communicate about it. Let me call the things we reason about objects. What do we use to represent objects? Symbols, pictures, sounds, smells and many more things we have senses for. We transmit objects as a literal, or as an algorithm ("a turing machine") of how to recreate the object. All turing machines can be encoded with finite bit arrays.
It turns out we are able to make digital computers recreate symbols and pictures and sounds to a fidelity such that we can't notice any difference compared to the original. I see no fundamental difficulty besides physical limitations to recreate other literals. All literals in a computer can be encoded with finite bit arrays.
Finally, I conclude that finite bit arrays are the most general objects we can reason about; they have rich semantics by the possibility to interpret them as turing machines. What we end up with looks a lot like common programming languages.
Based on intuitionistic logic, finite bit arrays, and the ability to interpret them as turing machines, we can follow the canonical construction of the reals. In this world, every object is a finite bit array, plus some annotated interpretation ("a type"), which is just notation for a bigger finite array. There is simply no place for non-countability.
I long for a software that lets me mix logic and usual programming seamlessly, without unnecessary like meta-theories, meta-logic. Coq is near, but the programming is too unnatural.
One can reason about the logic of a Rust programm, discuss it with others, and even the compiler understands some of the meaning, but richer intuitionistic logic statements about the output or behaviour of the code are sadly beyond the compiler.
I'm about to start applying for my graduate studies of mathematics. Do you have any recommendations which university to apply to to research in the area I talked about?
The more I talk about constructivism the less I feel it's adequate to label what I'm talking about, even though my approach to mathematics is completely constructive. Please don't treat every word I use as totally definite.
Mathematics is the science of formal reasoning. I call the rules of reasoning, that is the rules of manipulation of statements including their lexicon, syntax and semantic, a logic. I see intuitionistic logic as the most intuitive, universal and fruitful logic, in short: the logic.
To reason, we need something to reason about. Said somethings should be respresentable, so we can communicate about it. Let me call the things we reason about objects. What do we use to represent objects? Symbols, pictures, sounds, smells and many more things we have senses for. We transmit objects as a literal, or as an algorithm ("a turing machine") of how to recreate the object. All turing machines can be encoded with finite bit arrays.
It turns out we are able to make digital computers recreate symbols and pictures and sounds to a fidelity such that we can't notice any difference compared to the original. I see no fundamental difficulty besides physical limitations to recreate other literals. All literals in a computer can be encoded with finite bit arrays.
Finally, I conclude that finite bit arrays are the most general objects we can reason about; they have rich semantics by the possibility to interpret them as turing machines. What we end up with looks a lot like common programming languages.
Based on intuitionistic logic, finite bit arrays, and the ability to interpret them as turing machines, we can follow the canonical construction of the reals. In this world, every object is a finite bit array, plus some annotated interpretation ("a type"), which is just notation for a bigger finite array. There is simply no place for non-countability.
I long for a software that lets me mix logic and usual programming seamlessly, without unnecessary like meta-theories, meta-logic. Coq is near, but the programming is too unnatural.
One can reason about the logic of a Rust programm, discuss it with others, and even the compiler understands some of the meaning, but richer intuitionistic logic statements about the output or behaviour of the code are sadly beyond the compiler.
I'm about to start applying for my graduate studies of mathematics. Do you have any recommendations which university to apply to to research in the area I talked about?