[proofplan] The inclusion $C \subseteq (C^\perp)^\perp$ follows directly from the definition of the dual: every element of $C$ is orthogonal to every element of $C^\perp$, and hence lies in $(C^\perp)^\perp$. The reverse inclusion is a dimension count: two applications of the [Dimension Formula for a Linear Code and its Dual](/theorems/1690) give $\dim((C^\perp)^\perp) = \dim(C)$. A subspace contained in another subspace of the same finite dimension must equal it, so $C = (C^\perp)^\perp$. The parity-check interpretation follows because $(C^\perp)^\perp = \{x \in \mathbb{F}_2^n : x \cdot y = 0 \text{ for all } y \in C^\perp\}$ is exactly the null space of a matrix whose rows form a basis of $C^\perp$. [/proofplan] [step:Show that $C \subseteq (C^\perp)^\perp$ by unfolding the definitions] By definition, the dual of any subset $S \subseteq \mathbb{F}_2^n$ with respect to the standard bilinear form $x \cdot y := \sum_{i=1}^n x_i y_i$ is \begin{align*} S^\perp := \{x \in \mathbb{F}_2^n : x \cdot s = 0 \text{ for all } s \in S\}. \end{align*} Fix $c \in C$. For every $y \in C^\perp$, the definition of $C^\perp$ gives $y \cdot c = 0$. Since the form is symmetric, $c \cdot y = y \cdot c = 0$ for all $y \in C^\perp$. By definition of $(C^\perp)^\perp$ applied with the subset $C^\perp$, this says $c \in (C^\perp)^\perp$. Hence \begin{align*} C \subseteq (C^\perp)^\perp. \end{align*} [guided] This inclusion is the "tautological" one: every $c \in C$ is orthogonal to everything orthogonal to $C$. In symbols, starting from the defining property of $C^\perp$ — that $y \cdot c = 0$ for all $y \in C^\perp, c \in C$ — we use the symmetry $y \cdot c = c \cdot y$ to rewrite it as $c \cdot y = 0$ for all $y \in C^\perp$, which is precisely the defining property of $(C^\perp)^\perp$ for the element $c$. No dimension count is needed here. The nontrivial content of the theorem is that this inclusion is an equality, which requires showing that $(C^\perp)^\perp$ is not strictly larger than $C$ — this is where finite-dimensionality enters in the next step. [/guided] [/step] [step:Compute $\dim((C^\perp)^\perp)$ using the dimension formula twice] By the [Dimension Formula for a Linear Code and its Dual](/theorems/1690) applied to the linear code $C$, \begin{align*} \dim_{\mathbb{F}_2}(C^\perp) = n - \dim_{\mathbb{F}_2}(C). \end{align*} The same theorem applied to the linear code $C^\perp$ (which is indeed a linear subspace of $\mathbb{F}_2^n$, since $S^\perp$ is always linear: $(x + x') \cdot s = x \cdot s + x' \cdot s$ and scalar multiples similarly) gives \begin{align*} \dim_{\mathbb{F}_2}((C^\perp)^\perp) = n - \dim_{\mathbb{F}_2}(C^\perp) = n - (n - \dim_{\mathbb{F}_2}(C)) = \dim_{\mathbb{F}_2}(C). \end{align*} [guided] To apply the [Dimension Formula](/theorems/1690) to $C^\perp$, we need $C^\perp$ to be a linear code — i.e., a linear subspace of $\mathbb{F}_2^n$. This is automatic: $S^\perp$ for any subset $S$ is always a linear subspace, because the orthogonality conditions $x \cdot s = 0$ are linear in $x$. Specifically, if $x_1, x_2 \in S^\perp$ and $\lambda \in \mathbb{F}_2$, then $(\lambda x_1 + x_2) \cdot s = \lambda(x_1 \cdot s) + (x_2 \cdot s) = 0$ for every $s \in S$. Hence the dimension formula applies, and we chain two applications: $\dim(C^\perp) = n - \dim(C)$, then $\dim((C^\perp)^\perp) = n - \dim(C^\perp) = \dim(C)$. The cancellation is exact. [/guided] [/step] [step:Conclude $C = (C^\perp)^\perp$ by equality of dimensions] By Step 1, $C$ is a linear subspace of $(C^\perp)^\perp$. By Step 2, $\dim(C) = \dim((C^\perp)^\perp) < \infty$ (both dimensions are at most $n$). A finite-dimensional vector space contains no proper subspace of the same dimension: if $V \subseteq W$ are subspaces of a finite-dimensional space with $\dim V = \dim W$, then any basis of $V$ has the right cardinality to be a basis of $W$ and is already linearly independent in $W$, so it spans $W$ and $V = W$. Applying this with $V = C$ and $W = (C^\perp)^\perp$, \begin{align*} C = (C^\perp)^\perp. \end{align*} [/step] [step:Deduce that every linear code is a parity-check code] Let $h_1, \ldots, h_{n-k} \in \mathbb{F}_2^n$ be a basis of $C^\perp$, and assemble these as the rows of a matrix \begin{align*} H := \begin{pmatrix} h_1 \\ \vdots \\ h_{n-k} \end{pmatrix} \in \mathbb{F}_2^{(n-k) \times n}. \end{align*} For any $x \in \mathbb{F}_2^n$, the $i$-th component of $Hx$ is $h_i \cdot x$. Therefore $Hx = 0$ if and only if $h_i \cdot x = 0$ for all $i$, which (because $h_1, \ldots, h_{n-k}$ span $C^\perp$ and orthogonality is linear) holds if and only if $x \cdot y = 0$ for all $y \in C^\perp$, i.e.\ $x \in (C^\perp)^\perp$. By Step 3, $(C^\perp)^\perp = C$, so \begin{align*} C = \{x \in \mathbb{F}_2^n : Hx = 0\} = \ker(H), \end{align*} exhibiting $C$ as the null space of the matrix $H$, which is the defining property of a parity-check code with parity-check matrix $H$. [guided] The parity-check interpretation is a direct corollary of the double-dual identity. Reading definitions: a parity-check code is one defined as $\{x : Hx = 0\}$ for some matrix $H$. The space $(C^\perp)^\perp$ is, by construction, the set of vectors orthogonal to every element of $C^\perp$, which — writing down a basis of $C^\perp$ as the rows of a matrix $H$ — is exactly $\ker(H)$. The double-dual identity $(C^\perp)^\perp = C$ therefore says $C = \ker(H)$ with $H$ being any matrix whose rows form a basis of $C^\perp$. The rows of $H$ give $n - k$ linearly independent parity-check equations, one for each basis element of $C^\perp$. [/guided] [/step]