TITLE: Typo in the calculus of constructions paper?
QUESTION [10 upvotes]: In the classic the calculus of constructions paper there is a rule that states

(page 7 of the pdf, page 101 of the original document)
This rule would mean that any context is reducible to a member of that context.  This seems like it shouldn't be correct, as it would entail
1 ≅ Nat
3 ≅ Nat
1 ≅ 3

if Nat is a context.
I think the best interpretation is that the lower delta was meant to be an M.  Especially considering the rules given on the next page.
So is this simply a typo, or some subtle logical rule that I don't understand?

REPLY [11 votes]: You are correct, there is an error in that paper, and the rule should indeed read:
$$\frac{\Gamma\vdash M:\Delta}{\Gamma\vdash M\cong M} $$
the use of jugements of this style for equality (sometimes called "typed equality") originates already in Martin-Löf, I think (see here for example). It's often replaced with an untyped operational definition in modern treatments, where there is no jugement of the form $\Gamma\vdash N\cong M$, and conversion is defined on raw terms.
Somewhat counter-intuitively, proving that the system with typed conversion is equivalent to the one without types is very difficult, and was settled in 2010 by Siles and Herbelin.


TITLE: Does forcing generally go one way?
QUESTION [7 upvotes]: Question Is there any forcing free proof for hard independence results?  talks about the use of forcing for independence results such as: $Con(ZFC)\longrightarrow Con (ZFC+\neg CH) $.  For that case (and its companions $V=L$ and $AC$)  constructibility is used for the other half of the independence: $Con(ZFC)\longrightarrow Con (ZFC+ CH) $.
Is this typical?  Do later independence results still tend to use forcing one way, and $V=L$ the other?  Are there independence results where forcing is used in both directions?
Are there statements $S$ where forcing is used for both $Con(ZF+S)$ and $Con(ZF+\neg S)$?
Question Is every class that does not add sets necessarily added by forcing?  mentions use of forcing over a model of $NBG$ to add a universal choice function.  But I do not know for whether you would also use forcing to eliminate that version of global choice in that context.

REPLY [14 votes]: There is a wide variety of statements $S$ for which forcing can be used to prove the (relative) consistency of both $S$ and $\lnot S$ with $\mathsf{ZFC}$.
For example, Cohen developed forcing to prove the consistency of $\lnot\mathsf{CH}$, but we can also prove $\mathsf{CH}$ consistent this way: We can add to the universe a well-ordering of the reals of type $\omega_1$ without adding any reals. This, by the way, shows that any projective statement provable from $\mathsf{CH}$ is provable without it.
There are some restrictions: $V=L$ cannot be forced. This is because $L$ is forcing invariant (we can also say generically absoute): If $W$ is a forcing extension of $V$, then $L$ in the sense of $W$ is the same as $L$ in the sense of $V$. This is true of larger core models, and is one of their key features. It allows us to prove results about the universe by arguing about forcing extensions, and is particularly useful when proving consistency strength lower bounds (and in the development of the general theory of core models).
Similarly, if $\alpha$ is a countable ordinal, then we cannot use forcing to make $\alpha$ uncountable (the idea being that if we already see a surjection from $\omega$ onto $\alpha$, adding more sets is not going to make this go away).
Other examples of statements $S$ that can be forced either way are: $2^{\aleph_1}=\aleph_{17}$, $\mathfrak b=\omega_1<\mathfrak c$, any algebraic homomorphism between Banach algebras is continuous, etc. The list can go on forever. If we assume the presence of large cardinals in the universe, then even more examples can be given.
Joel Hamkins and his collaborators (notably, Benedikt Loewe) have worked on this, making explicit interesting connections with modal logic (think of $\diamondsuit\phi$ as "it is forceable that $\phi$" and of $\square\phi$ as "$\phi$ holds in all extensions"). See here for a starting point.

Now, an interesting fact about forcing is how ubiquitous it is. This distinguishes it from other techniques. Woodin's $\Omega$-conjecture can be informally described as stating that any $\Pi_2$ statement we can verify consistent (with large cardinals) in fact can be forced (over arbitrary models with large cardinals). (This is an informal description. A more technical presentation would perhaps obscure the point here. See this survey by Bagaria, Castells, and Larson, for details.)
One of the reasons why the $\Omega$-conjecture is of interest is that it holds in all known "$L$-like" models. It is also forcing absolute, so its consistency cannot be verified by forcing (unless we already know it is true). Another reason is that there are a few examples of $\Pi_2$ statements we do not know how to force over arbitrary models, though we can prove consistent with appropriate large cardinals (by forcing over special ground models). One is: "There is a $\mathbf{\Sigma}^2_1$-well-ordering of the reals, and the continuum is a real-valued measurable cardinal", see here.
In his book The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal, Hugh suggests a few statements of large cardinal character (stronger than "there is a limit $\lambda$ and a nontrivial $j:V_\lambda\to V_\lambda$") that appear to be fragile, meaning that it is not clear that they are preserved by small forcing. Whether these statements can be proved consistent with $\mathsf{CH}$ or with $\lnot\mathsf{CH}$ does not seem to be a matter of forcing. Something different would be needed here.

REPLY [8 votes]: There are plenty of results where one uses forcing to make both parts of the independence. Even the case of CH can be done this way, since Solovay proved shortly after forcing was invented that one can force CH as well as $\neg$CH. Thus, CH is an example of what Benedikt Löwe and I call a switch, a statement $\varphi$ such that $\varphi$ and $\neg\varphi$ are each forceable over any forcing extension, so that you can turn it on and off again at will. A button, in contrast, is a statement that you can force in such a way that it remains true in all further extensions. These concepts were important in our work on The modal logic of forcing.
Meanwhile, there are several examples where the only known proofs use forcing on both sides, particularly in the context of very large cardinals. For example:

The existence of a supercompact cardinal $\kappa$ is relatively consistent with $2^\kappa=\kappa^+$ and with $2^\kappa\gt\kappa^+$. Both sides of these proofs use forcing.
Similar consistency results of the very largest large cardinals with CH and GCH and their negations are only known by forcing.
Many other consistency results concerning the very largest large cardinals are only known by forcing, because there is no inner model theory analogue of $L$ for those cardinals.


TITLE: Minimum Edge Density given a particular condition
QUESTION [2 upvotes]: Consider a graph with $n$ vertices such that if one takes any 4 vertices there are at most 4 edges among these 4 vertices (Notice that there are 6 "possible" edges among these 4 vertices). What is the maximum possible edge density for such a graph as a function of $n$ and what is the limit as $n$ goes to infinity?
Using a probabilistic argument one can show that as $n$ goes to infinity that the edge density can be at most $\frac{2}{3}+\epsilon$, yet finding such a construction seems extremely tricky.

REPLY [2 votes]: It is well-known, but I do not know where did it appear for the first time.
The answer is $f(2k)=k^2$ for $n=2k$ and $f(2k+1)=k(k+1)$ for $n=2k+1$. Examples are bipartite graphs $K_{k,k}$ and $K_{k,k+1}$. The proof of upper estimate goes by induction. Base $n=4$ is clear. Assume that $n\geqslant 5$ and graph on $n-1$ vertices may have at most $f(n-1)$ edges. Assume that some graph $G$ on $n$ vertices has at least $f(n)+1$ edges. Remove some edges so that exactly $f(n)+1$ edges remain. Each vertex $v$ has degree at least $f(n)-f(n-1)+1$, else $G\setminus v$ has more than $f(n-1)$ edges. Thus total number of edges is not less than $n(f(n)-f(n-1)+1)/2>f(n)+1$ (check this for two cases). The contradiction.


TITLE: Help to evaluate $\int\ t^2 \sin\beta t\, dt$
QUESTION [0 upvotes]: $\int\ t^2 \sin\beta t\, dt$
How do I treat
$\sin\beta t$
?

REPLY [0 votes]: Is for integration by parts $\int u dv=uv -\int v du$ applied 2 times: First, let $u=t^2$ and $dv=\sin \beta t dt$; then $du=2t dt$ and $v=-\frac{1}{\beta}\cos \beta t$, so
$$\int t^2\sin \beta t \,dt = -\frac{1}{\beta}t^2\cos \beta t+\int \frac{1}{\beta}\cos \beta t\, 2t dt=-\frac{t^2}{\beta}\cos \beta t+\frac{2}{\beta}\int t\cos \beta t\, dt.$$
Now, let $u=t$ and $dv=\cos \beta t\, dt$. Then we find $du=dt$ and $v=\frac{1}{\beta}\sin \beta t$ and so
$$\int t^2\sin \beta t \,dt =-\frac{t^2}{\beta}\cos \beta t+\frac{2}{\beta}\left[\frac{t}{\beta}\sin \beta t-\int \frac{1}{\beta}\sin \beta t\, dt \right] =$$
$$=-\frac{t^2}{\beta}\cos \beta t+\frac{2t}{\beta^2}\sin \beta t -\frac{2}{\beta^2}\int \sin \beta t \, dt=$$
$$=-\frac{t^2}{\beta}\cos \beta t+\frac{2t}{\beta^2}\sin \beta t -\frac{2}{\beta^2}\left( -\frac{1}{\beta}\cos \beta t +c\right) =$$
$$=-\frac{t^2}{\beta}\cos \beta t+\frac{2t}{\beta^2}\sin \beta t +\frac{2}{\beta^3} \cos \beta t +c. $$


TITLE: Diagonalization of a quadratic form
QUESTION [1 upvotes]: I have to diagonalize the following quadratic form:
$$
Q(x,y,z,t)=x^2+y^2+2xy+2xz+2xt+2yz
$$
I want to complete the squares, so I observe that the first three terms are the square $(x+y)^2$. Then I sum and subtract the quantities $2x^2$, $2z^2$, $y^2$ and $t^2$. Now, how do I have to continue? Which is the associated matrix?

REPLY [1 votes]: Consume all the terms containing $x$ first ... etc ...
\begin{eqnarray*}
(x+y+z+t)^2-(y+z+t)^2+(y+z)^2-z^2
\end{eqnarray*}
Edit:
\begin{eqnarray*}
\begin{pmatrix}1 & 1 & 1&1 \\0 & 1 & 1&1 \\0 & 1& 1&0 \\0&0&1&0 \\\end{pmatrix}^{T}
\begin{pmatrix}1 & 0 & 0&0 \\0 & -1 & 0&0 \\0 & 0& 1&0 \\0&0&0&-1 \\\end{pmatrix}
\begin{pmatrix}1 & 1 & 1&1 \\0 & 1 & 1&1 \\0 & 1& 1&0 \\0&0&1&0 \\\end{pmatrix}=
\begin{pmatrix}1 & 1 & 1&1 \\1 & 1 & 1&0 \\1 & 1& 0&0 \\1&0&0&0 \\\end{pmatrix}
\end{eqnarray*}


TITLE: Number of subfields of finite field
QUESTION [3 upvotes]: Possible Duplicate:
Subfields of finite fields

Field with $2^{15}$ elements
How many subfields? Including trivial one and the whole thing I guess $15$. Right or not my guess? I think every subfield gives a subspace of dimension dividing $2^{15}$. Hence 15 of them?

REPLY [8 votes]: A finite field $\mathbb{F}_q$ is contained in the finite field $\mathbb{F}_r$ if and only if there exists a prime $p$ and integers $n$ and $m$ such that $q=p^m$, $r=p^n$, and $m|n$. This follows because $\mathbb{F}_r$ is a vector space over $\mathbb{F}_q$, and so will have $q^d$ elements for some $d$; and because finite fields must have order a power of a prime.
In particular, $\mathbb{F}_{2^{15}}$ contains a field with $2^r$ elements if and only if $r|15$.
While every subfield is a subspace, not every subspace is a subfield. For example, the field with four elements can be realized as
$$\{a+b\alpha\mid a,b\in\mathbb{F}_2,\ \alpha^2=\alpha+1\}.$$
Then $\{b\alpha\mid b\in\mathbb{F}_2\}$ is a subspace, but not a subfield.


TITLE: how fast decrease a limit
QUESTION [1 upvotes]: I have this limit,
$$
\lim_{b\rightarrow0}b\log b +(1-cb-b)\log(1-cb-b)-(1-cb)\log(1-cb)
$$
where $c\in\mathbb{R}$ is a constant.
I know this is going to zero, but I want to know how fast it decreases. For instance, when $c=0$ it becomes
$$
\lim_{b\rightarrow0}b\log b+(1-b)\log(1-b)
$$
and here the dominat term is $b\log b$ so it decreases as fast as $b\log b$.
So, the dominant term in the case of the first limit should be bounded by $b\log b$ but how I get it, and what if $c$ is not constant anymore, if $c=\frac{1}{b}$, the limit still would vanish, but how fast in this case?
thanks

REPLY [3 votes]: We have that
$$b\log b +(1-cb-b)\log(1-cb-b)-(1-cb)log(1-cb)=$$
$$=b\log b+(1-cb-b)(-cb-b+o(b))-(1-cb)(-cb+o(b))=$$$$=b\log b-cb-b+cb+o(b)=b\log b-b+o(b)=$$
$$=b\log b + o(b\log b)$$