The common amplitude $a>0$ is uniquely determined by any entry's absolute value. After choosing it, each entry independently has sign $+1$ or $-1$. Thus the correspondenceis a bijection from $(0,\infty )\times \{-1,1{\}}^{\mathbb{N}}$ onto the set. The positive reals have cardinal $\mathfrak{c}$, and binary sign sequences have cardinal $2^{{\aleph }_0}=\mathfrak{c}$. HenceHere “independently” refers to unconstrained deterministic choices of coordinates, not probabilistic independence; no probability distribution is being specified.

Every finitely supported sequence vanishes from some index onward, since a finite subset of the natural numbers has a greatest element. Thus the set is a union over $n<\omega$ of sequences determined by their first $n$ real entries, with zeros afterwards. Each nontrivial piece has cardinal ${\mathfrak{c}}^n=\mathfrak{c}$, so the union has cardinal at most ${\aleph }_0\cdot \mathfrak{c}=\mathfrak{c}$.

Conversely $r\mapsto (r,0,0,\dots )$ is an injection from $\mathbb{R}$. Cantor-Schröder-Bernstein therefore givesNo choice of an arbitrary infinite support is involved; it is the finite support that makes a countable union of finite-dimensional parameter spaces enough.

The notation ${}^{\mathbb{R}}\mathbb{R}$ means all functions from the real numbers to themselves, with no continuity restriction. Its cardinal isThe exponent law follows by viewing a function to a function set as one function on a Cartesian product. Cantor's theorem gives $2^{\mathfrak{c}}>\mathfrak{c}$, so this is strictly larger than the other continuum-sized examples here. Characteristic functions of subsets of $\mathbb{R}$ already supply the lower bound $2^{\mathfrak{c}}$.

For an infinite cardinal $\kappa$, multiplication by a nonzero countable cardinal does not change it. Since $|\mathbb{R}|=\mathfrak{c}\ge {\aleph }_0$,There is also an immediate lower bound from $r\mapsto (r,0)$; the standard product identity supplies the matching upper bound. The discreteness of the second coordinate does not create a new cardinal beyond the continuum.

The Cantor-Schröder-Bernstein theorem states that injections $f:A\to B$ and $g:B\to A$ imply the existence of a bijection $A\to B$. Here is a direct proof, avoiding any appeal to a fixed-point theorem. Let $A_0=A\setminus g(B)$, $A_{n+1}=g(f(A_n))$, and $C={\bigcup }_{n<\omega }{A}_n$. DefineThe second case is defined because $A\setminus C\subseteq g(B)$. On $C$, $f$ is a bijection onto $f(C)$. For $b\in B$, injectivity of $g$ and the construction of $C$ give $g(b)\in C$ if and only if $b\in f(C)$: $g(b)$ cannot be in $A_0$, so membership in $C$ means membership in some $g(f(A_n))$. Hence $g^{-1}$ bijects $A\setminus C$ onto $B\setminus f(C)$. The two pieces have disjoint domains and images and together cover $A,B$, proving $h$ bijective. This proof itself uses no choice.

Write $\mathfrak{c}=|\mathbb{R}|=2^{{\aleph }_0}$. We use the standard infinite-cardinal identities $\kappa \cdot {\aleph }_0=\kappa$, ${\kappa }^n=\kappa$ for positive finite $n$ and infinite $\kappa$, and $({\kappa }^{\lambda }{)}^{\mu }={\kappa }^{\lambda \cdot \mu }$, under the permitted axiom of choice. The map $z\mapsto (\mathrm{Re}z,\mathrm{Im}z)$ bijects $\mathbb{C}$ with ${\mathbb{R}}^2$. Therefore

For a countable fixed point of a normal ordinal function, first show that $\Phi$ maps every countable ordinal to a countable ordinal. Use transfinite induction below ${\omega }_1$. The zero case is assumed, and the successor case is the stated preservation property. If $\lambda$ is a countable limit, normality gives $\Phi (\lambda )={\bigcup }_{\alpha <\lambda }\Phi (\alpha )$, a countable union of countable sets, hence countable. This countable-union step is where axiom of countable choice is used; the assumed axiom of choice supplies it.

Now set ${\alpha }_0=0$, ${\alpha }_{n+1}=\Phi ({\alpha }_n)$. The preceding result makes every term countable, and the domination proved earlier makes the sequence nondecreasing. If it ever stabilizes, it already gives the required fixed point. Otherwise $\alpha ={\sup }_{n<\omega }{\alpha }_n$ is a countable nonzero limit, using axiom of countable choice again for countability of the union. Its defining sequence is cofinal, so monotonicity and continuity giveApply this to $\Phi (\alpha )={\omega }^{\alpha }$. This is normal, begins at $1$, and ${\omega }^{\alpha +1}={\omega }^{\alpha }\cdot \omega$ is countable whenever ${\omega }^{\alpha }$ is countable. Thus a countable $ϵ$ satisfies $\boxed{ϵ={\omega }^{ϵ}}$. Starting at zero gives the familiar tower sequence $0,1,\omega ,{\omega }^{\omega },\dots$, whose supremum is ${ϵ}_0$. The finite recursion, ordinal identities and fixed-point continuity do not require choice; the uses of choice above concern countable unions of countable ordinals.

For fixed $\beta$, the recursion defining $\beta +\alpha$ makes it continuous in $\alpha$ at every nonzero limit, and $(\beta +\alpha )+1>\beta +\alpha$. Thus $\alpha \mapsto \beta +\alpha$ is normal, including when $\beta =0$.

For $\beta >0$, take $\lambda =\beta \cdot \omega$. If $\alpha <\lambda$, choose a natural number $n$ with $\alpha <\beta n$; then $\alpha +\beta \le \beta (n+1)<\lambda$. Since $\alpha +\beta \ge \alpha$, their supremum as $\alpha \uparrow \lambda$ is $\lambda$. But $\lambda +\beta >\lambda$, soHence right addition by a nonzero fixed ordinal fails continuity and is not normal.

Normality and argument order in ordinal arithmetic also give the multiplication statements: $\alpha \mapsto \beta \cdot \alpha$ is normal for $\beta >0$, while $\alpha \mapsto \alpha \cdot \beta$ is normal exactly when $\beta =1$. At $\beta =0$ it is constant. For fixed $\beta >1$, let $\kappa ={\omega }^{\beta \cdot \omega }$. Cantor normal form shows that $\xi \beta <\kappa$ whenever $\xi <\kappa$: leading exponents below $\beta \omega$ remain below it after adding the leading exponent of $\beta$. Thus ${\sup }_{\xi <\kappa }\xi \beta =\kappa$, but $\kappa \beta >\kappa$, again violating continuity. Left-fixed multiplication is strictly increasing and continuous by its recursion.

For exponentiation, $\alpha \mapsto {\beta }^{\alpha }$ is normal for $\beta \ge 2$; bases zero and one are exceptions. The reverse map $\alpha \mapsto {\alpha }^{\beta }$ is normal exactly when $\beta =1$. Exponent zero gives the constant one. For $\beta >1$, use the same $\kappa$ and put $\lambda ={\omega }^{\kappa }$. For each $\alpha <\lambda$ choose $0<\zeta <\kappa$ with $\alpha \le {\omega }^{\zeta }$. Then ${\alpha }^{\beta }\le {\omega }^{\zeta \beta }<\lambda$, while ${\alpha }^{\beta }\ge \alpha$ for positive $\alpha$. Consequently its left supremum is $\lambda$, but ${\lambda }^{\beta }={\omega }^{\kappa \beta }>\lambda$. The bound by ${\omega }^{\zeta }$ also handles finite bases, where an unqualified leading-exponent multiplication formula would need care. All these are ordinal facts and use no choice.

The ordinal operations are defined by transfinite recursion in the right argument. Addition satisfies $\alpha +0=\alpha$, $\alpha +(\beta +1)=(\alpha +\beta )+1$, and $\alpha +\lambda ={\sup }_{\beta <\lambda }(\alpha +\beta )$ at a nonzero limit. Multiplication satisfies $\alpha \cdot 0=0$, $\alpha \cdot (\beta +1)=\alpha \cdot \beta +\alpha$, and $\alpha \cdot \lambda ={\sup }_{\beta <\lambda }\alpha \cdot \beta$. Exponentiation satisfies ${\alpha }^0=1$, ${\alpha }^{\beta +1}={\alpha }^{\beta }\cdot \alpha$, and ${\alpha }^{\lambda }={\sup }_{\beta <\lambda }{\alpha }^{\beta }$ at nonzero limits. These are ordinal operations, not commutative cardinal arithmetic.

For a normal function on an ordinal, prove domination by transfinite induction. At zero, $0\le \Phi (0)$ automatically. If $\alpha \le \Phi (\alpha )$, strict increase at successors gives $\alpha +1\le \Phi (\alpha )+1\le \Phi (\alpha +1)$. At a nonzero limit $\lambda$, continuity and the induction hypotheses giveTherefore $\boxed{\alpha \le \Phi (\alpha )\text{ for every ordinal }\alpha }$. No axiom of choice is needed for this ordinal induction.

There are sixteen binary Boolean functions, one for each four-bit truth table. Exactly eight give an adequate basis together with negation.

The eight affine functions are $0,1,p,\neg p,q,\neg q,p\oplus q,\neg (p\oplus q)$. Each is affine over the field with two elements, and composition with other affine functions or negation remains affine. Since conjunction is not affine, none of these eight bases is adequate.

Each remaining truth table has either one true row or three true rows. In the latter case negate its output to obtain a function with one true row. Negate selected inputs to move that row to $(1,1)$: the resulting function is conjunction. Conjunction together with negation expresses every disjunctive normal form, proving adequacy of all remaining eight. They are AND, NAND, OR, NOR, the two directed implications, and the two asymmetric conjunctions $p\wedge \neg q$, $\neg p\wedge q$. The count treats the binary connective by its truth function rather than by arbitrary choices of its printed symbol.

Adequacy here means functional completeness: every Boolean truth function of finitely many positive-arity propositional inputs can be expressed by a formula using the available connectives. It is an expressive-power claim, distinct from the completeness theorem relating derivability and semantic entailment.

Negation and implication define conjunction and disjunction byGiven any truth table, for each input row where its output is true form the minterm containing each input positively or negatively according to that row. The disjunction of these minterms is true on exactly the required rows: a disjunctive normal form. Replacing its conjunctions and disjunctions by the displayed definitions gives a formula using only $\neg ,\to$.

The constantly true and constantly false functions are represented by $p\to p$ and $\neg (p\to p)$, using a dummy input if needed. Thus the empty or full truth table also causes no difficulty. If one insists on genuinely nullary formulas with no variables at all, a separate truth constant is needed; ordinary propositional adequacy allows the constant truth functions to be expressed with irrelevant input variables.

Choose a fresh variable $x_3$. In A7 take the equality antecedent $x_3=x_1$, the atomic formula $\varphi =(x_3=x_2)$, and replace its occurrence of $x_3$ by $x_1$. This gives directly the theoremGeneralize on $x_3$, with no open assumptions. A4 then instantiates that quantifier with the term $f(x_0)$. The substitution is free for $x_3$, since the matrix contains no quantifiers. One modus-ponens step yieldsFinally generalize, in order, on $x_2$, $x_1$, and $x_0$. The result isEvery step is A7, generalization, A4, or modus ponens. Neither completeness, adequacy, nor an unproved appeal to all propositional tautologies is needed. In particular the proof does not silently upgrade the variable-only equality axiom to an arbitrary-term axiom: quantification and instantiation perform that upgrade explicitly.

Fix any structure and any assignment of the three quantified variables, writing their values as $a_0,a_1,a_2$. If either of the nested antecedents is false, the corresponding implication is true. If both are true, then $f^A(a_0)=a_1$ and $f^A(a_0)=a_2$. Actual identity is transitive, so $a_1=a_2$, making the consequent true as well.

Thus the unquantified matrix is true under every assignment in every structure. The universal-quantifier semantic clause then makes its universal closure true in every structure:No assumption that $f$ is injective is used. The argument says that one value cannot equal two distinct elements, not that distinct inputs have distinct outputs.

A first-order structure consists of a nonempty domain $A$, an interpretation $c^A\in A$ of each constant symbol, a total function $f^A:A^n\to A$ for each $n$-ary function symbol, and a relation $R^A\subseteq A^n$ for each $n$-ary predicate symbol. Logical equality is interpreted as actual identity.

An assignment in a first-order structure is a map $s$ from the variables into $A$. It extends recursively to terms: $x^A[s]=s(x)$, $c^A[s]=c^A$, and $f(t_1,\dots ,t_n{)}^A[s]=f^A(t_1^A[s],\dots ,t_n^A[s])$. Atomic truth is determined by membership of the resulting tuple in $R^A$, or equality of the two term values. Negation reverses the truth value, and an implication is false exactly when its antecedent is true and its consequent false.

For a universal quantifier,These clauses define a valuation on every formula by structural recursion. Only free-variable values affect a formula's truth; consequently a sentence has the same truth value under every assignment. This is a semantic assignment of domain elements, not a programming assignment operation.

With generalization restricted to variables not free in open assumptions, the deduction theorem statesThe reverse direction follows by thinning and modus ponens. For the forward direction, induct on a derivation, keeping track of its actual assumption contexts. Axioms and assumptions already in $\Gamma$ yield $\alpha \to \chi$ by A1; the distinguished assumption $\alpha$ yields the permitted theorem $\alpha \to \alpha$. If a line $\chi$ is obtained by modus ponens from $\eta$ and $\eta \to \chi$, the induction hypotheses and A2 derive $\alpha \to \chi$.

If a generalization step depends on the discharged assumption, its variable $x$ is not free in $\alpha$ or the other open assumptions. Generalize the induction conclusion $\alpha \to \eta$ to $\forall x(\alpha \to \eta )$ and use A5 to derive $\alpha \to \forall x\eta$. If the subderivation does not depend on $\alpha$, its generalized conclusion can instead be retained as an independent derivation and A1 applied afterwards. Thinning merely enlarges the remaining context and preserves the induction claim. These cases are why assumption dependence, rather than a careless unrestricted universal rule, is essential.

In a presentation allowing generalization freely from hypotheses, the corresponding theorem must instead explicitly require that no variable free in $\alpha$ is generalized in an $\alpha$-dependent line. Without that restriction $P(x)⊢\forall xP(x)$ would incorrectly yield $⊢P(x)\to \forall xP(x)$.

The thinning rule, or weakening, isIt expresses that extra unused assumptions do not destroy a proof. In the context-sensitive predicate-calculus presentation it also allows a theorem first proved with a fresh generalization variable to be used later in a context containing that variable free. Simply replaying the same generalization under the larger context could violate its side condition. For instance a proof of $\forall x(x=x)$ from the empty context may generalize on $x$; it should remain available when an unused assumption $P(x)$ is added, even though that last generalization could not be replayed with $P(x)$ open.

In propositional calculus the axiom schemes and modus ponens have no analogous free-variable restriction. An induction on the original proof simply reuses each axiom, assumption and modus-ponens step under the enlarged assumptions, so weakening is admissible and need not be postulated separately. Context-sensitive Hilbert weakening concerns this proof presentation: systems already tracking only the assumptions on which each line depends can build admissible weakening into their treatment of predicate-calculus generalization as well.

Capture-safe equality replacement gives the corrected scheme:where ${\varphi }^{\prime }$ replaces selected free occurrences of $x_i$ by $x_j$, without capture. One may equivalently use full capture-avoiding substitution, after renaming conflicting binders. Replacing bound occurrences as though they were free is not permitted.

Here is a syntactic proof. Write $e$ for $x_i=x_j$. First derive symmetry under $e$: A6 and A4 give $x_i=x_i$, and A7 applied to the first position in that atomic equality gives $e\to (x_i=x_i\to x_j=x_i)$. Modus ponens and the deduction theorem give $⊢e\to x_j=x_i$. Atomic replacement in the forward direction is A7 itself; in the reverse direction apply A7 with $i,j$ exchanged and use this symmetry. Thus under $e$, an atomic formula and its designated replacement imply each other.

Induct on the formation of $\varphi$, proving both directions simultaneously. For negation, the reverse implication for the immediate subformula gives the forward implication of its negations by contraposition, and vice versa. For $\theta \to \eta$, the two induction equivalences combine propositionally to $(\theta \to \eta )\leftrightarrow ({\theta }^{\prime }\to {\eta }^{\prime })$. This uses only the propositional tautologies allowed in this part.

For $\varphi =\forall z\theta$, first take $z$ distinct from $x_i,x_j$. From assumptions $e$ and $\forall z\theta$, A4 gives $\theta$, the induction hypothesis gives ${\theta }^{\prime }$, and generalization gives $\forall z{\theta }^{\prime }$: $z$ is free in neither open assumption. Discharge the two assumptions to obtain $e\to (\forall z\theta \to \forall z{\theta }^{\prime })$. The reverse direction is identical. If the binder is $x_i$, no free occurrence of that variable lies beneath it and the replacement there is empty. If it is $x_j$, capture avoidance likewise forbids a changed free $x_i$ below that binder unless the binder is first renamed to a fresh variable. Bound-variable renaming is derived from A4 followed by admissible generalization and A5, with the same freshness restriction. This completes the structural induction and proves the scheme for arbitrary formulas.