Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorColin Tan
   • CommentTimeDec 29th 2013
   • PermaLink
   Author: Colin Tan
   Format: MarkdownItexThroughout the Lab, a term x of type X is introduced with the phrase "for x a X". Is the word "for" a contraction of the universal quantifier "for each"? In the [context](http://ncatlab.org/nlab/show/context) of weak logics that do not understand universal quantification, we put the sentence "x : X" before the turnstile, which amounts to "x : X" being an assumption. In this sense, should the manner of introducing a term x of type X be written "if x is a X"?

   Throughout the Lab, a term x of type X is introduced with the phrase “for x a X”. Is the word “for” a contraction of the universal quantifier “for each”? In the context of weak logics that do not understand universal quantification, we put the sentence “x : X” before the turnstile, which amounts to “x : X” being an assumption.

   In this sense, should the manner of introducing a term x of type X be written “if x is a X”?

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeDec 29th 2013
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe ‘for’ here is the same ‘for’ as in ‘for each’, but it\'s not that ‘for’ is a contraction of ‘for each’; the grammar is different. I will use a concrete example. You can say either : For each set $x$, ${|x|} \lt {|2^x|}$. or : For $x$ a set, ${|x|} \lt {|2^x|}$. (which both mean the same), but you can\'t say : For each $x$ a set, ${|x|} \lt {|2^x|}$. or : For set $x$, ${|x|} \lt {|2^x|}$. (which are both bad grammar).

   The ‘for’ here is the same ‘for’ as in ‘for each’, but it's not that ‘for’ is a contraction of ‘for each’; the grammar is different.

   I will use a concrete example. You can say either

   For each set $x$, ${|x|} \lt {|2^x|}$.

   or

   For $x$ a set, ${|x|} \lt {|2^x|}$.

   (which both mean the same), but you can't say

   For each $x$ a set, ${|x|} \lt {|2^x|}$.

   or

   For set $x$, ${|x|} \lt {|2^x|}$.

   (which are both bad grammar).

3. • CommentRowNumber3.
   • CommentAuthorColin Tan
   • CommentTimeDec 29th 2013
   • PermaLink
   Author: Colin Tan
   Format: TextWhat does "for" mean?

   What does "for" mean?
4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeDec 30th 2013
   • (edited Dec 30th 2013)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexIndividual words like "for" are hard to define when divorced from context, but I think "for each set $x$" could be equivalently replaced by "given any set $x$", and "for $x$ a set" by "given a set $x$". Incidentally, with regard to the last question of #1, I think the phrase "if $x$ is an $X$" is also a more or less okay substitute, but the sense is a little different from what one is familiar with from set theory. In traditional set theory, given any two sets $x$ and $X$, we can always form the proposition "$x$ is an $X$" (meaning actually $x \in X$) and ask whether it holds; it's as if the the expressions $x$ and $X$ have an independent existence. But in type theory, a term $x$ is automatically attached to a type $X$, i.e., as soon as a term $x$ is introduced, we declare its type $X$ -- that's a rule of the type theory game. So I find it personally more helpful to say "given a term $x$ of type $X$" rather than "if $x$ is a term of type $X$", because the latter expression carries a subtle suggestion that there is some choice in the matter. Another way to say it is that "if $x$ isn't a term of type $X$" is just something that never comes up legally in the type-theoretic game.

   Individual words like “for” are hard to define when divorced from context, but I think “for each set $x$” could be equivalently replaced by “given any set $x$”, and “for $x$ a set” by “given a set $x$”.

   Incidentally, with regard to the last question of #1, I think the phrase “if $x$ is an $X$” is also a more or less okay substitute, but the sense is a little different from what one is familiar with from set theory. In traditional set theory, given any two sets $x$ and $X$, we can always form the proposition “$x$ is an $X$” (meaning actually $x \in X$) and ask whether it holds; it’s as if the the expressions $x$ and $X$ have an independent existence. But in type theory, a term $x$ is automatically attached to a type $X$, i.e., as soon as a term $x$ is introduced, we declare its type $X$ – that’s a rule of the type theory game. So I find it personally more helpful to say “given a term $x$ of type $X$” rather than “if $x$ is a term of type $X$”, because the latter expression carries a subtle suggestion that there is some choice in the matter. Another way to say it is that “if $x$ isn’t a term of type $X$” is just something that never comes up legally in the type-theoretic game.

5. • CommentRowNumber5.
   • CommentAuthorColin Tan
   • CommentTimeDec 30th 2013
   • PermaLink
   Author: Colin Tan
   Format: MarkdownItexI prefer the type-theoretic approach. Still, I am trying to understand the logical meaning of the words "for" or "given" when used in the context "for x a set" or "given a set x". Or similarly, the word "let" in the context "let x be a set". From my understanding, such phrases are used to announce the assumption of the antecedent in a conditional statement. In terms of Toby's example "for each set x, the cardinality of x is strictly smaller than the cardinality of its powerset", I would begin writing a proof with the annoucement "Suppose x is a set." And make my argument. Then close with "Thus the cardinality of x is strictly smaller than the cardinality of its power set." And formally conclude with "Hence, for each set x, the cardinality of x is strictly smaller than the cardinality of its powerset." I learnt to use "suppose ... thus" as paratheses from Edward Nelson's book Predicative Arithmetic. Suppose that we are working in the [context](http://ncatlab.org/nlab/show/context) of a weak logic that does not accomodate for universal quantification. This compels Toby's example to be enunciated as "if x is a set, then the cardinality of x is strictly smaller than the cardinality of its powerset." Or, to maintain the atomic nature of "x is a set", write "The cardinality of a set is strictly smaller than the cardinality of its powerset", thus avoiding the declaration of a term.

   I prefer the type-theoretic approach. Still, I am trying to understand the logical meaning of the words “for” or “given” when used in the context “for x a set” or “given a set x”. Or similarly, the word “let” in the context “let x be a set”.

   From my understanding, such phrases are used to announce the assumption of the antecedent in a conditional statement. In terms of Toby’s example “for each set x, the cardinality of x is strictly smaller than the cardinality of its powerset”, I would begin writing a proof with the annoucement “Suppose x is a set.” And make my argument. Then close with “Thus the cardinality of x is strictly smaller than the cardinality of its power set.” And formally conclude with “Hence, for each set x, the cardinality of x is strictly smaller than the cardinality of its powerset.”

   I learnt to use “suppose … thus” as paratheses from Edward Nelson’s book Predicative Arithmetic.

   Suppose that we are working in the context of a weak logic that does not accomodate for universal quantification. This compels Toby’s example to be enunciated as “if x is a set, then the cardinality of x is strictly smaller than the cardinality of its powerset.” Or, to maintain the atomic nature of “x is a set”, write “The cardinality of a set is strictly smaller than the cardinality of its powerset”, thus avoiding the declaration of a term.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeDec 31st 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> Suppose that we are working in the context of a weak logic that does not accomodate for universal quantification. This compels Toby’s example to be enunciated as “if x is a set, then the cardinality of x is strictly smaller than the cardinality of its powerset.” I disagree -- I'm with Todd that "if" is better reserved for the hypothesis of an implication. In the absence of $\forall$, we basically just leave off the initial $\forall$-elimination step and the final $\forall$-introduction step of such a proof, since they correspond to going back and forth between $(x:A) \vdash P(x)$ and $\vdash \forall (x:A) P(x)$. It's not unreasonable to regard "Suppose x is a set" and "Hence, for each set $x$, ..." as natural-language stand-ins for $\forall E$ and $\forall I$, so you could then just leave those off and call it good. However, I think natural language is not well-suited to making fine distinctions such as between $(x:A) \vdash P(x)$ and $\vdash \forall (x:A) P(x)$, so I would not personally bother about it -- I would use language the same as if there were universal quantification, and just be careful to only use it in valid ways, having made sure at the beginning the reader understands the absence of $\forall$.

   Suppose that we are working in the context of a weak logic that does not accomodate for universal quantification. This compels Toby’s example to be enunciated as “if x is a set, then the cardinality of x is strictly smaller than the cardinality of its powerset.”

   I disagree – I’m with Todd that “if” is better reserved for the hypothesis of an implication.

   In the absence of $\forall$, we basically just leave off the initial $\forall$-elimination step and the final $\forall$-introduction step of such a proof, since they correspond to going back and forth between $(x:A) \vdash P(x)$ and $\vdash \forall (x:A) P(x)$. It’s not unreasonable to regard “Suppose x is a set” and “Hence, for each set $x$, …” as natural-language stand-ins for $\forall E$ and $\forall I$, so you could then just leave those off and call it good. However, I think natural language is not well-suited to making fine distinctions such as between $(x:A) \vdash P(x)$ and $\vdash \forall (x:A) P(x)$, so I would not personally bother about it – I would use language the same as if there were universal quantification, and just be careful to only use it in valid ways, having made sure at the beginning the reader understands the absence of $\forall$.