4 ms·

You make a lot of strong claims, and express them with supreme confidence, but without providing much in the way of evidence. Some of what you say is complete

You make a lot of strong claims, and express them with supreme confidence, but without providing much in the way of evidence. Some of what you say is complete nonsense (e.g. "All mathematical optimization falls outside of classical logic", or "[Marx and Engels] are essentially talking about linear logic"). I can talk about this for hours. I recommend talking less about linear logic, and spending more time doing the maths, so that you actually understand LL, which is a precondition to making reasonable judgements about the pros and cons of LL.

adamnemecek 8y ago
What do you want evidence for? And like what form of evidence do you accept? > All mathematical optimization falls outside of classical logic" How so? > I recommend talking less about linear logic, and spending more time doing the maths, so that you actually understand LL, Cool, I don't remember asking for your suggestions.
- YorkshireSeason 8y ago
  How so? How about you show how even one of the well-known techniques for mathematical optimisation (see e.g. [1] for an overview) are not expressible in the currently accepted foundations of mathematics (such as ZF, PA, MLTT, HOTT), or at least point to peer-reviewed papers in credible mathematical publications that give evidence that "[a]ll mathematical optimization falls outside of classical logic". Or even weaker, point to Girard's written works where he claims that "[a]ll mathematical optimization falls outside of classical logic". "Extraordinary claims require extraordinary evidence." [1] https://en.wikipedia.org/wiki/Mathematical_optimization https://en.wikipedia.org/wiki/Mathematical_optimization
  - adamnemecek 8y ago
    I'm trying to have an informal discussion about things that aren't established science. Linear logic is from 1989. How many people do you think are familiar with it? HOTT states nothing about optimization. None of the foundations of mathematics really tackle optimization. I have a claim that you may or may not accept. There is such a thing as linear types (they are similar to Rust types). There's this language called ATS which is basically OCaml with C like performance. The performance gain is thanks to linear types, the compiler can statically reason about performance and statically optimize code. This isn't unrelated to mathematical optimization. Linear types let you to trully distinguish between values and references. Your standard for proof is too high and there's only one particular type of proof that you accept unquestioningly. I'm still not convinced that you've looked into this for long enough to really see how they are related. Before we continue, tell me something about linear logic, or like how you understand it. Maybe helping you understand linear logic would be more productive than repeatedly invoking a couple of memes. It's quite naive that our current understanding of math is really "all there is". > "Extraordinary claims require extraordinary evidence." I'm allowed to make whatever claims I want. You are allowed to disagree.
    - YorkshireSeason 8y ago
      trying to have an informal discussion That's fine, but you express yourself in a way that sounds like you have a deep understanding of LL, and its relationship to other subjects such as programming languages and economic games. You have gotten a lot of pushback here for this reason, I'm just expressing myself more bluntly than other. Sorry, but you don't currently have this knowledge, and that might be misleading to others. I recommend to take this criticism constructively, and deepen your knowledge of logic (linear or otherwise), and there is only one way of doing this, which is to go beyond intuition and informality, and "do the math". How many people do you think are familiar with it? A lot on HN. Including myself, having written several papers on the subject, and discussed LL on numerous occasions with the world's leading researchers in the area, including Girard himself and several of his students. HOTT states nothing about optimization. None of the foundations of mathematics really tackle optimization. This is a complete misunderstanding of the foundations of mathematics. ZF(C) doesn't mention the natural and real numbers either. You can construct the rational and the real numbers in all foundations of mathematics (and this is typically done in undergraduate maths see e.g. [1] where I learned the construction from). Notions of minimun/maximum as well as related concepts can be expressed, too. This means that all mathematical optimisation as conventionally understood is trivially expressible in e.g. ZFC. There is such a thing as linear types I know, I coauthored some of the early papers on linear types. Linear types let you to trully distinguish between values and references. No, linear types let you distinguish between values that are guaranteed to be used exactly once, and values that may not be used exactly once. Note that Rust (at least last time I looked -- the language evolves fast) has more like affine rather than linear types (guaranteeing use at most once). that our current understanding of math is really "all there is". Nobody says this, indeed this is an immediate consequence of Goedel's incompleteness results. [1] Yiannis Moschovakis, Notes on Set Theory (https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Mathematics/dp/038728723X https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Math...)
      - adamnemecek 8y ago
        Can you post your papers on linear logic? > Notions of minimun/maximum as well as related concepts can be expressed, too. Exactly. There are two types of minimum and maximum, something that isn't expressible in any of the current foundations of mathematics. There is your minimum and maximum, and my minimum maximum. This is exactly what linear logic is about.

adamnemecek 8y ago

What do you want evidence for? And like what form of evidence do you accept? > All mathematical optimization falls outside of classical logic" How so? > I recommend talking less about linear logic, and spending more time doing the maths, so that you actually understand LL, Cool, I don't remember asking for your suggestions.

YorkshireSeason 8y ago
How so? How about you show how even one of the well-known techniques for mathematical optimisation (see e.g. [1] for an overview) are not expressible in the currently accepted foundations of mathematics (such as ZF, PA, MLTT, HOTT), or at least point to peer-reviewed papers in credible mathematical publications that give evidence that "[a]ll mathematical optimization falls outside of classical logic". Or even weaker, point to Girard's written works where he claims that "[a]ll mathematical optimization falls outside of classical logic". "Extraordinary claims require extraordinary evidence." [1] https://en.wikipedia.org/wiki/Mathematical_optimization https://en.wikipedia.org/wiki/Mathematical_optimization
- adamnemecek 8y ago
  I'm trying to have an informal discussion about things that aren't established science. Linear logic is from 1989. How many people do you think are familiar with it? HOTT states nothing about optimization. None of the foundations of mathematics really tackle optimization. I have a claim that you may or may not accept. There is such a thing as linear types (they are similar to Rust types). There's this language called ATS which is basically OCaml with C like performance. The performance gain is thanks to linear types, the compiler can statically reason about performance and statically optimize code. This isn't unrelated to mathematical optimization. Linear types let you to trully distinguish between values and references. Your standard for proof is too high and there's only one particular type of proof that you accept unquestioningly. I'm still not convinced that you've looked into this for long enough to really see how they are related. Before we continue, tell me something about linear logic, or like how you understand it. Maybe helping you understand linear logic would be more productive than repeatedly invoking a couple of memes. It's quite naive that our current understanding of math is really "all there is". > "Extraordinary claims require extraordinary evidence." I'm allowed to make whatever claims I want. You are allowed to disagree.
  - YorkshireSeason 8y ago
    trying to have an informal discussion That's fine, but you express yourself in a way that sounds like you have a deep understanding of LL, and its relationship to other subjects such as programming languages and economic games. You have gotten a lot of pushback here for this reason, I'm just expressing myself more bluntly than other. Sorry, but you don't currently have this knowledge, and that might be misleading to others. I recommend to take this criticism constructively, and deepen your knowledge of logic (linear or otherwise), and there is only one way of doing this, which is to go beyond intuition and informality, and "do the math". How many people do you think are familiar with it? A lot on HN. Including myself, having written several papers on the subject, and discussed LL on numerous occasions with the world's leading researchers in the area, including Girard himself and several of his students. HOTT states nothing about optimization. None of the foundations of mathematics really tackle optimization. This is a complete misunderstanding of the foundations of mathematics. ZF(C) doesn't mention the natural and real numbers either. You can construct the rational and the real numbers in all foundations of mathematics (and this is typically done in undergraduate maths see e.g. [1] where I learned the construction from). Notions of minimun/maximum as well as related concepts can be expressed, too. This means that all mathematical optimisation as conventionally understood is trivially expressible in e.g. ZFC. There is such a thing as linear types I know, I coauthored some of the early papers on linear types. Linear types let you to trully distinguish between values and references. No, linear types let you distinguish between values that are guaranteed to be used exactly once, and values that may not be used exactly once. Note that Rust (at least last time I looked -- the language evolves fast) has more like affine rather than linear types (guaranteeing use at most once). that our current understanding of math is really "all there is". Nobody says this, indeed this is an immediate consequence of Goedel's incompleteness results. [1] Yiannis Moschovakis, Notes on Set Theory (https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Mathematics/dp/038728723X https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Math...)
    - adamnemecek 8y ago
      Can you post your papers on linear logic? > Notions of minimun/maximum as well as related concepts can be expressed, too. Exactly. There are two types of minimum and maximum, something that isn't expressible in any of the current foundations of mathematics. There is your minimum and maximum, and my minimum maximum. This is exactly what linear logic is about.