Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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”?
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.
For each set $x$, ${|x|} \lt {|2^x|}$.
For $x$ a set, ${|x|} \lt {|2^x|}$.
For each $x$ a set, ${|x|} \lt {|2^x|}$.
For set $x$, ${|x|} \lt {|2^x|}$.
(which are both bad grammar).
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.
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.
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$.
1 to 6 of 6