Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 3rd 2016
   • (edited Nov 3rd 2016)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI was looking at Zeno Vendler's subtle account of the differences between every, each, all and any, and it seemed to me that one difference pointed to something like one might expect from turning the two conjunctions of linear logic into universal quantifiers: * I can afford each dish. * I can afford all dishes. I see someone else wondered this at Math Stackexchange, [Why don't the quantifiers split in linear logic?](http://math.stackexchange.com/questions/1788978/why-dont-the-quantifiers-split-in-linear-logic) There's also a difference of who chooses in existential cases: * You can have an/some apple. * You can have any apple. [Wikipedia on [linear logic](https://en.wikipedia.org/wiki/Linear_logic): Additive disjunction ($A \oplus B$) represents alternative occurrence of resources, the choice of which the machine controls.] Does this ring any bells?

   I was looking at Zeno Vendler’s subtle account of the differences between every, each, all and any, and it seemed to me that one difference pointed to something like one might expect from turning the two conjunctions of linear logic into universal quantifiers:

   • I can afford each dish.
   • I can afford all dishes.

   I see someone else wondered this at Math Stackexchange, Why don’t the quantifiers split in linear logic?

   There’s also a difference of who chooses in existential cases:

   • You can have an/some apple.
   • You can have any apple.

   [Wikipedia on linear logic: Additive disjunction ($A \oplus B$) represents alternative occurrence of resources, the choice of which the machine controls.]

   Does this ring any bells?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI think one problem is that the usual rules for multiplicative connectives, if extended to quantifiers regarded as infinitary conjunctions and disjunctions, would necessitate infinite contexts and probably infinite proofs too. That is, if I know that "all" real numbers $x$ satisfy $P(x)$ in a multiplicative sense, then the only way to use that in a proof would be to use $P(x)$ for *all* real numbers $x$, which would require an infinite amount of work since there are infinitely many real numbers. Infinitary logic of this sort is I think theoretically possible, but people don't study it a lot, because it's not something we can actually write on paper explicitly or implement in a computer. Semantically, we don't usually encounter monoidal categories in which you can tensor together infinitely many things. A different sort of "multiplicative quantifier" appears in [[bunched implication]], where the domains of quantification are treated multiplicatively as well (rather than simply indexing an infinitary multiplicative connective). Semantically this seems to correspond to hyperdoctrines of a sort over a semicartesian monoidal category, so that the multiplicative quantifiers can be adjoints to pullback along the projection morphisms of the tensor product.

   I think one problem is that the usual rules for multiplicative connectives, if extended to quantifiers regarded as infinitary conjunctions and disjunctions, would necessitate infinite contexts and probably infinite proofs too. That is, if I know that “all” real numbers $x$ satisfy $P(x)$ in a multiplicative sense, then the only way to use that in a proof would be to use $P(x)$ for all real numbers $x$, which would require an infinite amount of work since there are infinitely many real numbers. Infinitary logic of this sort is I think theoretically possible, but people don’t study it a lot, because it’s not something we can actually write on paper explicitly or implement in a computer. Semantically, we don’t usually encounter monoidal categories in which you can tensor together infinitely many things.

   A different sort of “multiplicative quantifier” appears in bunched implication, where the domains of quantification are treated multiplicatively as well (rather than simply indexing an infinitary multiplicative connective). Semantically this seems to correspond to hyperdoctrines of a sort over a semicartesian monoidal category, so that the multiplicative quantifiers can be adjoints to pullback along the projection morphisms of the tensor product.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeNov 4th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI see, thanks.

   I see, thanks.

4. • CommentRowNumber4.
   • CommentAuthorKeithEPeterson
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: KeithEPeterson
   Format: MarkdownItexBut what about the Finite Set case?

   But what about the Finite Set case?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIn that case you can just write $P(1) \otimes \cdots \otimes P(n)$.

   In that case you can just write $P(1) \otimes \cdots \otimes P(n)$.

6. • CommentRowNumber6.
   • CommentAuthorKeithEPeterson
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: KeithEPeterson
   Format: MarkdownItexSo then for $I \in FinSet$, we have $\forall_{\otimes} := \bigotimes_{i\in I}P_i$, which seems to be a reasonable thing to say. Also, couldn't I use an ultrafilter on infinite $I$ as well and then be able to deal with some infinite cases?

   So then for $I \in FinSet$, we have $\forall_{\otimes} := \bigotimes_{i\in I}P_i$, which seems to be a reasonable thing to say.

   Also, couldn’t I use an ultrafilter on infinite $I$ as well and then be able to deal with some infinite cases?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't understand, what would you do with an ultrafilter?

   I don’t understand, what would you do with an ultrafilter?

8. • CommentRowNumber8.
   • CommentAuthorKeithEPeterson
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: KeithEPeterson
   Format: MarkdownItexMy idea is to use ultrafilters the same they are used in non-standard analysis to work with infinities aka "non-finite hyperreals". Perhaps I should make an explicit construction...

   My idea is to use ultrafilters the same they are used in non-standard analysis to work with infinities aka “non-finite hyperreals”.

   Perhaps I should make an explicit construction…

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 10th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI've never heard of "nonstandard logic" before -- that would be neat if it gives something interesting.

   I’ve never heard of “nonstandard logic” before – that would be neat if it gives something interesting.

10. • CommentRowNumber10.
    • CommentAuthorKeithEPeterson
    • CommentTimeDec 11th 2016
    • PermaLink
    Author: KeithEPeterson
    Format: MarkdownItexIn fact, why not view Infinitary (Boolean) Logic as an instance of non-standard analysis? Why couldn't this diagram commute? $\begin{matrix} \mathbb{R} & \overset{(-)\mapsto {}^*(-)}{\rightarrow} & {}^{*}\mathbb{R}\\ \downarrow & & \downarrow\\ \mathbb{B} & \overset{(-)\mapsto {}^*(-)}{\rightarrow} & {}^{*}\mathbb{B} \end{matrix}$

    In fact, why not view Infinitary (Boolean) Logic as an instance of non-standard analysis? Why couldn’t this diagram commute?

    $\begin{matrix} \mathbb{R} & \overset{(-)\mapsto {}^*(-)}{\rightarrow} & {}^{*}\mathbb{R}\\ \downarrow & & \downarrow\\ \mathbb{B} & \overset{(-)\mapsto {}^*(-)}{\rightarrow} & {}^{*}\mathbb{B} \end{matrix}$

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 11th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThere are, of course, lots of subtle issues when using "hyperfinite" hyperreal numbers to say things about "actually" infinite sets. So this is an interesting speculation, but I think would take a lot of work to make precise.

    There are, of course, lots of subtle issues when using “hyperfinite” hyperreal numbers to say things about “actually” infinite sets. So this is an interesting speculation, but I think would take a lot of work to make precise.