3 ms·

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”. (

by 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/
  - AstralStorm 8y ago
    You can convert any terminating formula (including recursive) to a finite logic representation in second order logic with exponential number of terms. This by use of Peano numbering. Proving whether the given (inductive or recursive) formula is actually terminating is the halting problem though. Linear logic is closely related to martingales too.
    - YorkshireSeason 8y ago
      I'm not sure I can follow you here. I have said that you need to express infinitary formulae in a finitary form. What's the connection with martingales?

by Jaxan 8y ago

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/
- AstralStorm 8y ago
  You can convert any terminating formula (including recursive) to a finite logic representation in second order logic with exponential number of terms. This by use of Peano numbering. Proving whether the given (inductive or recursive) formula is actually terminating is the halting problem though. Linear logic is closely related to martingales too.
  - YorkshireSeason 8y ago
    I'm not sure I can follow you here. I have said that you need to express infinitary formulae in a finitary form. What's the connection with martingales?