4 ms·

> 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

> 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. 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"?

adamnemecek 8y ago
Imma paraphrase Wikipedia. You are right but I find the informal definition to be more illuminating. “Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite”. Now imagine that there’s an opponent who decides the object selection of certain bins. 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).
- aisofteng 8y ago
  I’m having difficulty following your comments about adversarial choice as related to the axiom of choice. What you’re saying doesn’t sound well-defined (in the mathematical sense).
  - adamnemecek 8y ago
    It's actually very well defined (or which part are you confused by). I'm stating these things informally as a formal treatment is right now beyond me and it also doesn't really exist. Look up Chu spaces esp their relationship to linear logic. This paper is pretty informative https://www.semanticscholar.org/paper/Chu-spaces-as-a-semantic-bridge-between-linear-and-Pratt/3bf444cc4a892eccfa4f51064c4b85079acfbcd8 https://www.semanticscholar.org/paper/Chu-spaces-as-a-semant... Fundamentally, think of the minimax algorithm. You have two sides each optimizing for victory.
    - YorkshireSeason 8y ago
      I don't see how Pratt's paper justifies any of your claims.
      - adamnemecek 8y ago
        Can you give me the summary of the paper?
    - AnimalMuppet 8y ago
      "It's actually very well defined" and "a formal treatment... doesn't really exist" seem to me to be contradictory statements.
      - adamnemecek 8y ago
        It's a path that unifies several very formally related. The unification itself isn't fully formalized, you need to look at the symmetries in the well formalized subparts.
- Jaxan 8y ago
  So where is the part about the “best choice”? 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.
  - adamnemecek 8y ago
    Are you familiar with the minimax algorithm? Google for how it’s related to linear logic. For all is a clutch. There exists is much more manageable. However you need both the worst and the best “there exists”.
    - Jaxan 8y ago
      I see. That makes some sense now. Thanks!
  - lmkg 8y ago
    Your formulation doesn't work well if games are allowed to be infinite, because standard propositional logic doesn't handle formulae of infinite length. 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.
    - YorkshireSeason 8y ago
      Neither propositional logic nor first-order logic (FOL) allow formulae of infinite length. 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). [1] https://en.wikipedia.org/wiki/Infinitary_logic https://en.wikipedia.org/wiki/Infinitary_logic [2] https://plato.stanford.edu/entries/logic-infinitary/ https://plato.stanford.edu/entries/logic-infinitary/

adamnemecek 8y ago

Imma paraphrase Wikipedia. You are right but I find the informal definition to be more illuminating. “Informally put, the axiom of choice says that given any collection of bins, each containing at least one object, it is possible to make a selection of exactly one object from each bin, even if the collection is infinite”. Now imagine that there’s an opponent who decides the object selection of certain bins. 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).

aisofteng 8y ago
I’m having difficulty following your comments about adversarial choice as related to the axiom of choice. What you’re saying doesn’t sound well-defined (in the mathematical sense).
- adamnemecek 8y ago
  It's actually very well defined (or which part are you confused by). I'm stating these things informally as a formal treatment is right now beyond me and it also doesn't really exist. Look up Chu spaces esp their relationship to linear logic. This paper is pretty informative https://www.semanticscholar.org/paper/Chu-spaces-as-a-semantic-bridge-between-linear-and-Pratt/3bf444cc4a892eccfa4f51064c4b85079acfbcd8 https://www.semanticscholar.org/paper/Chu-spaces-as-a-semant... Fundamentally, think of the minimax algorithm. You have two sides each optimizing for victory.
  - YorkshireSeason 8y ago
    I don't see how Pratt's paper justifies any of your claims.
    - adamnemecek 8y ago
      Can you give me the summary of the paper?
  - AnimalMuppet 8y ago
    "It's actually very well defined" and "a formal treatment... doesn't really exist" seem to me to be contradictory statements.
    - adamnemecek 8y ago
      It's a path that unifies several very formally related. The unification itself isn't fully formalized, you need to look at the symmetries in the well formalized subparts.
Jaxan 8y ago
So where is the part about the “best choice”? 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.
- adamnemecek 8y ago
  Are you familiar with the minimax algorithm? Google for how it’s related to linear logic. For all is a clutch. There exists is much more manageable. However you need both the worst and the best “there exists”.
  - Jaxan 8y ago
    I see. That makes some sense now. Thanks!
- lmkg 8y ago
  Your formulation doesn't work well if games are allowed to be infinite, because standard propositional logic doesn't handle formulae of infinite length. 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.
  - YorkshireSeason 8y ago
    Neither propositional logic nor first-order logic (FOL) allow formulae of infinite length. 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). [1] https://en.wikipedia.org/wiki/Infinitary_logic https://en.wikipedia.org/wiki/Infinitary_logic [2] https://plato.stanford.edu/entries/logic-infinitary/ https://plato.stanford.edu/entries/logic-infinitary/