A Taste of Linear Logic (1993) [pdf]
homepages.inf.ed.ac.uk
homepages.inf.ed.ac.uk
This has some interesting applications in constructive mathematics (https://arxiv.org/abs/1805.07518) and programming (http://homepages.inf.ed.ac.uk/wadler/papers/multiparty/multi...).
I’ve been slowly working on some applied linear logic stuff for my day job the past two years. I definitely think a lot of work has missed out on what happens if you have both implication and par native to your system. You get a really nice kernel for a concurrent functional programming language. With nice resource safety.
Your day job sounds fascinating, would you mind expanding on it a bit?
Basically, it's like classical logic but with two players. From player 1's point of view, player 2's AND has different semantics than his own AND.
It's the logic of state developing over time. In classical logic a statement can only be true since negative eternity and it will be true until eternity.
On the other hand, linear logic deals with statements like "I have a dollar" which can be spent on an ice cream. Therefore, at some point, "I have a dollar" was false, then it became true, and then it became false again.
It's also the logic that captures the difference between a reference and a value which is weirdly important. Unix's "everything is a file" should actually be recast as "everything is a reference".
The Rust borrow checker is based on a subset of linear logic and it's the secret sauce of said compiler. It can reason statically about dynamic systems.
I'll make some claims that I can support with papers if need to be so ask if you want proof. Currently, probability is based on measure theory however linear logic can also be used (Vovk bases probability on game theory which is essentially linear logic).
Generative adversarial networks (which are based on minimax) are based on linear logic as minimax is very linear logical.
I would go as far as to say that mathematics, in addition to axiom of choice also needs an axiom of adversarial choice. Axiom of choice assumes that you can always pick the best possible option, however you need to be able to account for your worst possible options as well. All mathematical optimization falls outside of classical logic.
The funniest thing is that this idea, the duality of things is very old. Dialectics is very firmly rooted in Western philosophy (Aristotle, Kant, Hegel, you know the usual suspects) however no one ever extended it to a formal logic.
Karl Marx (I hate Marx but realize that his ideas might have influenced people so knowing why he was wrong is worth something) also talked about a similar idea (https://en.wikipedia.org/wiki/Dialectical_materialism). In particular Engel's summary is work exploring https://en.wikipedia.org/wiki/Dialectical_materialism#Engels...
They are essentially talking about linear logic, however the third rule is very much wrong, negation of negation is not a part of a logic of two opposites.
It can also be used as the foundation of probability instead of the more traditional measure theory.
I can talk about this for hours.
You may already be aware of this, but that various kinds of temporal logic allows one to capture very complex predicates for the evolution of state machine (much like your person with a dollar).
If you have a familiarity with state machines (here Kripke systems) it might be approachable.
Some useful links:
1. https://www.cs.cmu.edu/~emc/15414-s14/lecture/ModelChecking....
Not sure what you mean here. The axiom of choice just says that the Cartesian product of a set of nonempty sets is nonempty. Can you explain what you mean by "best possible option" and "worst possible options"?
This is a silly example but compare playing chess single player vs multiplayer. In the single player chess, you still have two sides, you are still trying to make your side to win, however you decide all the moves (even for the other party). IRL, a lot of choices are outside of your control. So in some sense, you need to account for your opponent's best moves (which are generally the worst moves for you).
https://www.semanticscholar.org/paper/Chu-spaces-as-a-semant...
Fundamentally, think of the minimax algorithm. You have two sides each optimizing for victory.
Two player games to me are all about quantifiers. If the opponent plays, it means we have to prove a “for all”. (This includes all worst case scenarios obviously.) And own plays are “exist” (just the best option at that time). No axiom of choice involved, just FO logic.
For all is a clutch. There exists is much more manageable. However you need both the worst and the best “there exists”.
There is something called the Axiom of Determinacy which states that all two-player games of perfect information have a winning strategy for one player. This axiom applies to games of any length, including all types of uncountable infinities. The Axioms of Choice and Determinancy are incompatible; if one of them is true, the other can be proven false.
I don't know if this is related to what GP was talking about, but it reminded me.
While there are logics with formulae of infinite length (see [1, 2] for an overview), I would not consider them logics on par with propositional or FOL. Why? Because as a finite human you cannot actually write down infinite formulae! Instead, you use some finite abbreviation mechanism (typically some variant of FOL, extended with set theoretic axioms like ZFC) so you can denote (in a finite way) those infinite formulae. I'd suggest to see infinite formulae as a semantics gadget that is sometimes useful in model-theoretic investigations.
It's not surprising that we encounter questions independent from ZFC (or whatever your preferred foundation of mathematics) when we look at infinite games. It's but an instance of our inability to define infinite sets in an impredicative way (i.e. the usual inductive definition of the natural numbers as the least set closed under successor).
Proving whether the given (inductive or recursive) formula is actually terminating is the halting problem though.
Linear logic is closely related to martingales too.
What's the connection with martingales?
Even a soft, humanities subject like political philosophy, can, unexpectedly, be a topic for mathematical study, e.g. Arrow's theorem.
You're right not to believe in policing disciplinary boundaries.
I think the problem here is more that you haven't demonstrated just how Marx's thought resembles linear logic, so the idea might seem a little crazy, maybe a product of an idée fixe. If it's not something mathematicians would be impressed by (in terms of rigour or depth), and not something Marxists care about (in terms of philosophical implications) it's not going to lead anywhere.
> It's bona fide political philosophy and/or political economy.
It’s above all a description of development of science.
Why not?
Axiom of choice, choosing the right thoughts to have versus to speak.
If you don't understand, you don't want to. It's a perpetual type of terror that often has nothing to do with reality, but you can never be sure.
I'm aware but idk how this is relevant.
> If it's not something mathematicians would be impressed by (in terms of rigour or depth), and not something Marxists care about (in terms of philosophical implications) it's not going to lead anywhere.
I don't care? I'm not trying to impress anyone and I don't care what Marxists care about.
- Richard Demillo, Richard Lipton, and Alan Perlis, 1979
"... So don't rely on social processes for verification"
- David Dill, 1999
Aligned with linear logic, I find it productive to think in the abstract about the dialogues I'm having, in terms of what I would have to say to refute a claim given the opposing claim's form. I have found this oddly more productive at coming up with things to check or validate than asking purely, "what is the truth of the matter?"
I can talk about this for hours.
> 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.
How so?
"Extraordinary claims require extraordinary evidence."
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.
trying to have an informal discussion
How many people do you think are familiar with it?
HOTT states nothing about optimization.
None of the foundations of mathematics
really tackle optimization.
There is such a thing as linear types
Linear types let you to trully distinguish
between values and references.
that our current understanding of math is really
"all there is".
[1] Yiannis Moschovakis, Notes on Set Theory (https://www.amazon.com/Notes-Theory-Undergraduate-Texts-Math...)
> 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.
Can you post your papers
on linear logic?
Show me a peer reviews paper showing this. Extraordinary claims bla bla bla. Do you feel like we have progressed anywhere?
You can fully encode change of state against time with classical logic, it is a fundamental underpinning of solvers for digital synthesis (specifically the extension of SAT solvers to timing analysis).
It's been used, in production, for decades now.
Are you sure this works the way you think it does? I might be wrong but I'm getting a very low signal to noise ratio vibe from your comment.
(Edited for grammatical clarification.)
Edit: I found this comment [1] by you 29 days ago. Would you mind expanding on the "more connections" you mention? Thanks.
The final two are the linear part as they cause the logic to be positional.
The closest CS equivalent are categorial grammars (including combinatorial ones), the difference is that pure linear logic is commutative while these are not in general.
Note also that this paper doesn't seem to be talking about Minimax.
I think Hegels negations are part of breaking things apart from a omnipresent One so it basically means that things get defined as separate entities once they negate other things so 'negation of negation' does not mean that the same thing is negated twice rather it means something new is emerging and something old is disappearing. Maybe you can understand why negation of negation is true in this sense if you consider that the things change in relation to time and space.