Put one object into each box first. The remaining $n-k$ objects can be distributed without restrictions, so stars and bars givesEquivalently, the substitution $u_i=x_i-1$ gives a bijection between positive integer solutions of ${\sum }_i{x}_i=n$ and nonnegative integer solutions of ${\sum }_i{u}_i=n-k$.

Let $x_i$ be the number of objects in box $i$. The arrangements correspond exactly to nonnegative integer solutions of $x_1+\cdots +x_k=n$. By stars and bars, place $n$ stars and $k-1$ separating bars in a row. The number of stars between consecutive bars records the occupancy of each distinguishable box, with adjacent bars allowing an empty box. Choosing the bar positions gives

First suppose the sets are finite, with cardinalities $a=|A|\ge 2$ and $b=|B|\ge 2$. The power set and Cartesian product counting rules giveSince $ab-a-b=(a-1)(b-1)-1\ge 0$, the desired inequality follows.

The power-set product cardinality inequality also has an injection proof that does not assume finiteness. Choose distinct $a_0,a_1\in A$ and distinct $b_0,b_1\in B$. For $S\subseteq A$ and $T\subseteq B$, define the subset of $A\times B$These three encoding regions are disjoint. The row with second coordinate $b_0$ recovers $S$; the column with first coordinate $a_0$ and second coordinate different from $b_0$ recovers $T\setminus \{b_0\}$; the extra position $(a_1,b_1)$ records whether $b_0\in T$. Thus $\Phi$ is injective, proving for arbitrary setsEncoding by $S\times T$ alone would fail: all pairs with either factor empty would have the same output.

For every set $S$, the definition of a power set givesEquality by identical membership therefore provesThe essential observation is that being a subset of a set intersection means being a subset of both factors.

The commutativity and associativity of set intersection giveEquivalently, part (ii) reduces both sides to removal of the same set union $B\cup C=C\cup B$.

Use set difference, associativity of set intersection, and De Morgan's laws:

Take every complement of a set relative to $\mathcal{U}$. By set difference, De Morgan's laws, and distribution of set intersection over set union,Here the middle term is the empty set, since a set and its complement of a set are disjoint.

With the convention $\mathbb{N}=\{0,1,2,\dots \}$, the even inputs $2j$ map to $j$ for $j\ge 0$, while the odd inputs $2j+1$ map to $-(j+1)$ for $j\ge 0$. These two images of a function are disjoint and together equal $\mathbb{Z}$. Within either class there are no repeated outputs. More explicitly the inverse function isConsequently $f$ is both injective and surjective, hence a bijection. If instead $\mathbb{N}=\{1,2,\dots \}$, the input zero is absent: $f$ remains injective but its image of a function is $\mathbb{Z}\setminus \{0\}$, so it is not onto. The printed paper does not specify this convention; the zero-based convention gives the apparent intended bijection.

If $0\le x<y$, then $\sqrt{x}<\sqrt{y}$ and $x<y$, so $\sqrt{x}+x<\sqrt{y}+y$. Thus the function is strictly increasing on its domain and is injective. Its values are nonnegative, so it is not surjective onto $\mathbb{R}$:If ${\mathbb{R}}_{+}$ means $(0,\infty )$ its image of a function is $(0,\infty )$; if it includes zero its image of a function is $[0,\infty )$. Indeed, for any $u>0$, set $t=(\sqrt{1+4u}-1)/2>0$ and $x=t^2$; then $\sqrt{x}+x=t+t^2=u$. This convention does not change the classification.

Since $x^2+1\ge 2|x|$, the image of a function is contained in $[-1/2,1/2]$. Both endpoints occur, at $x=-1$ and $x=1$. By continuity and the intermediate value theorem applied on $[-1,1]$, every intermediate value occurs too. HenceIt is not surjective onto $\mathbb{R}$ because, for example, $1$ is not attained. It is not injective because $f(2)=f(1/2)=2/5$ although $2\ne 1/2$.

Choose $v$ fresh. Here double-negation elimination is necessary to turn the negation of a possible counterexample into the positive statement:The remaining context at line 7 contains no free $v$. The universal quantifier introduction rule therefore gives

Choose an eigenvariable $v$ fresh for the premise. Use the existential quantifier introduction rule to contradict the premise under a temporary assumption $R(v)$:At line 6 the assumption $R(v)$ has been discharged and the sole remaining premise has no free $v$, satisfying the eigenvariable condition. Thus

A variable $v$ is fresh for the surrounding context $\Gamma$ when it does not occur free in any undischarged assumption in $\Gamma$. Choose it also distinct from bound variables that would cause variable capture in the intended substitution. The universal quantifier introduction rule isIts justification is that the logical derivation of $\varphi (v)$ used no special information about $v$, so it establishes the property of an arbitrary object. Semantically, changing the assignment of $v$ preserves the truth of $\Gamma$; therefore $\varphi (v)$ holds for every possible assigned object. Without the eigenvariable condition, the assumption $R(v)$ could incorrectly be generalized to $\forall xR(x)$ in an interpretation where only one of two objects satisfies $R$.

Use proof by contradiction, expanding the final classical step explicitly into negation introduction followed by double-negation elimination. First the assumption $\neg (\neg P\vee \neg Q)$ forces $P$: otherwise $\neg P$ immediately gives the prohibited logical disjunction. It similarly forces $Q$. The formal natural deduction derivation isHenceThis direction of De Morgan's laws uses the classical rule supplied on the source rule sheet; it has not been silently treated as an available inference rule.

In proof by contradiction, assume the negation of the desired conclusion and derive logical falsity; discharge that assumption and infer the desired conclusion. Its sequent rule isThis is a rule of classical propositional logic. It follows from the paper's negation introduction rule, which first yields $\neg \neg \varphi$, and double-negation elimination, which yields $\varphi$. This is stronger than merely deriving $\neg \varphi$ by showing that $\varphi$ leads to logical falsity.

Use negation introduction separately for each component, introducing the forbidden logical disjunction in each subproof:Both temporary assumptions have been discharged before the final conjunction introduction, so

Extract both negations, assume the logical disjunction, and use disjunction elimination to derive logical falsity in either case:The two case subproofs are siblings, not nested within one another. Therefore

Use conjunction elimination to extract the three inputs, then apply the implication elimination rule three times:The implication introduction rule closes the only subproof, giving

Read chained logical implications as right-associative. Use the following natural deduction derivation; indentation bars mark nested subproofs and the last column records rules and discharged line ranges:Each application of the implication introduction rule discharges only its matching temporary assumption. Thus

A common-context sequent version of the disjunction elimination rule isThe second and third premises record exactly the two boxed subproofs of the natural deduction presentation. Their additional case assumptions do not occur in the conclusion: that is assumption discharge. The surrounding context $\Gamma$ remains throughout. A formulation with different surrounding contexts is equivalent after retaining their union by weakening.