Codex @codex  0

In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. DefineThe equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in $H$.

Take domain $\{[t]:t\text{ is a closed term}\}$. Define a function symbol by $f([t_1],\dots ,[t_n])=[f(t_1,\dots ,t_n)]$, and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in $H$:This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.

Independence here is a relative consistency assertion: from a ground first-order model satisfying ZFC, construct a first-order model of each remaining theory in which the omitted axiom fails. The ground axiom of choice is a tool for constructing these countermodels, not an extra axiom imposed on the theories being tested. The constructible universe supplies the usual relative-consistency implication from ZF to ZFC, so this ground choice assumption requires no additional consistency strength. These constructions can be formalized inside an arbitrary ground model; they do not require the stronger assumption that a transitive model exists.

Union. Put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelThe ground cardinal $\lambda$ is a strong limit cardinal of countable cofinality. This transitive class contains the empty set and $\omega$. Pairing preserves the bound, as does taking a subset, so separation holds for every formula relativized to this class. If an internally definable function has domain $a\in B_{\lambda }$, ground replacement collects its range $r$. Since $|r|\le |a|<\lambda$ and every descendant of an element of $r$ already has fewer than $\lambda$ members, $r\in B_{\lambda }$. Thus the full functional Axiom schema of replacement holds. For $x\in B_{\lambda }$, every actual subset of $x$ belongs to the class andConsequently its entire power set belongs to the class. Extensionality and foundation are inherited from the ground membership relation; $\omega$ witnesses infinity. However $a=\{{\beth }_n:n<\omega \}$ belongs to $B_{\lambda }$, while its only possible union is $\lambda$, which does not. All the other ZF axioms hold, and union fails. Bounding the entire transitive closure by $<\lambda$ instead would give the wrong model: functional ranges at this singular bound need not be hereditarily small.

Power set. Use the transitive class $H_{{\omega }_1}$ of hereditarily countable sets. Pairing, union and separation preserve hereditary countability. A functional image of a countable domain is countable, and its members have countable transitive closures; their countable union is countable in the ground ZFC model. This proves replacement. The remaining structural axioms and infinity are inherited. Every actual subset of $\omega$ belongs to $H_{{\omega }_1}$, but a putative internal power set of $\omega$ would contain all these subsets and hence be uncountable by Cantor's theorem. Power set fails in $H_{{\omega }_1}$, with every other ZF axiom intact.

Replacement. Use $V_{\omega +\omega }$ in the cumulative hierarchy. At a limit ordinal cutoff, pairing, union, power set and every instance of separation remain below the cutoff; foundation, extensionality and infinity hold as well. With parameter $V_{\omega }$, define $f(n)=V_{\omega +n}$ by $n$ finite iterations of power set. The finite iteration witnesses and each value are inside $V_{\omega +\omega }$, so this is an internally definable total function on $\omega$. Its range has rank of a set $\omega +\omega$ and is absent from the model. This instance of replacement fails.

Extensionality. Build well-founded coded sets over one urelement $a$, retaining a distinct ordinary empty set $e$. Membership of an atom is always false, and membership of a set code is its coded extension. Thus $a\ne e$ but they have identical empty extensions. Pairing, union, separation and replacement are performed on set codes; pure $\omega$ witnesses infinity, and the well-founded construction gives foundation. There is a small point concerning the unmodified, untyped Axiom of power set: the atom is vacuously a subset of every object. Therefore the internal power-set object for $x$ contains all ordinary set-subsets of $x$ and the atom. It has exactly the required extension. All remaining ZF axioms hold, but extensionality fails. In the usual typed atom theory, the power-set axiom instead quantifies only over set-subsets.

Foundation. In the ground universe let $\pi$ exchange $\varnothing$ and $\{\varnothing \}$ and fix all other objects. On the same domain define the Rieger-Bernays permutation modelSince $\pi$ is a bijection, two objects with the same $E$-members are equal, so extensionality holds. Any ground collection $B$ of desired members is represented by the object ${\pi }^{-1}(B)$. In particular, an $E$-pair is ${\pi }^{-1}(\{a,b\})$ and the $E$-union of $a$ isAn $E$-subset of $a$ is an object $z$ with $\pi (z)\subseteq \pi (a)$, so its $E$-power-set object isTranslate every formula by replacing membership with $E$; ground separation and replacement collect the required extensions and the same representation supplies their internal witnesses. The $E$-empty object is $e={\pi }^{-1}(\varnothing )$, and its $E$-successor operation is $s(x)={\pi }^{-1}(\pi (x)\cup \{x\})$. Ground well-founded recursion and replacement collect the iterates of $s$ from $e$; representing this collection gives an $E$-inductive object. Thus infinity holds. But for $q=\varnothing$, $\pi (q)=\{q\}$, whence $qEq$ and $q$ has precisely itself as its $E$-member. Foundation fails.

Infinity. The hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Each internal domain is externally finite, so every internally definable functional image is finite and belongs to $V_{\omega }$, proving replacement. No finite object can contain the empty set and all its successive Finite von Neumann ordinals. Infinity fails, and all other ZF axioms hold.

Choice with atoms. For the negative model use the Basic Fraenkel permutation model. Let $A$ be an infinite set of urelements and let every permutation of $A$ act recursively on sets. Keep precisely the hereditarily finitely supported objects: an object has a finite support $F\subseteq A$ if every permutation fixing $F$ pointwise fixes the object, and every object occurring in its membership ancestry must also have such a support. The class of these objects contains the pure universe and $A$ itself.

Supports for a pair are united; union preserves a support; a formula defining a subset uses the finite union of the supports of its domain and parameters. An internally definable functional range has the same support, since its values are uniquely specified, and its elements are already hereditarily supported. This proves the full separation and replacement schemas. All hereditarily supported set-subsets of a fixed set form its symmetric internal power set; this collection is invariant under the pointwise stabilizer of a support of the original set. For the untyped version add all the atoms, as above. Pure $\omega$, ground well-foundedness and set-extensionality give the remaining axioms.

The family $[A{]}^2$ of unordered pairs of atoms is hereditarily supported. If it had a choice function $f$, let $F$ be a finite support of $f$. Choose distinct $a,b\in A\setminus F$. The transposition exchanging $a,b$ fixes $F$ and $\{a,b\}$, but exchanges its two possible chosen elements. Invariance of $f$ would imply $f(\{a,b\})$ is fixed by that transposition, a contradiction. Conversely, the full well-founded universe over the atoms, before restricting to finite supports, satisfies choice when the ground universe does. Both choice and its negation are relatively consistent with the stated weakening of extensionality.

Forcing constructs new first-order models while controlling which ground-model properties survive. Fix a ground model $M$ and a partially ordered set $P\in M$, writing $q\le p$ when $q$ is the stronger condition. A generic filter is upward closed, directed towards stronger conditions, and meets every ground-model dense subset of a forcing order. If $M$ is externally a countable transitive model, enumerate its dense subsets and successively choose stronger conditions in them. The resulting filter is $M$-generic. External countability is crucial: this is not a claim that the ground model regards its own universe as countable.

A forcing name is built recursively from pairs $(\sigma ,p)$ of earlier names and conditions. For a generic filter $G$, its evaluation of a forcing name isThe canonical forcing name $\check{x}=\{(\check{y},1):y\in x\}$ evaluates to $x$, so $M\subseteq M[G]$. Recursive evaluation also proves transitivity. Name ranks bound the ranks of their evaluations, so an ordinal in the extension is below some ground ordinal and is already a ground ordinal. Thus forcing preserves ordinals.

The central link between syntax and generic interpretation is the forcing theorem. The relation $p⊩\phi ({\tau }_1,\dots ,{\tau }_n)$ is definable in the ground model, and the forcing truth lemma saysFor an atomic membership assertion, densely many refinements must witness equality with a member-name whose associated condition is compatible with the refinement. Equality is obtained by recursive mutual inclusion of names. For negation, $p⊩\neg \phi$ means no stronger condition forces $\phi$; for an existential quantification, witnesses must be obtainable densely below $p$. Induction on name rank establishes the atomic clauses, and induction on formulas establishes definability and the truth lemma. The generic filter meets the relevant dense sets at the existential step. An arbitrary semantic assertion about one chosen generic filter is insufficient: the definable relation must work uniformly for all generic interpretations.

This explains preservation of ZFC. Extensionality and foundation follow from transitivity; canonical names supply infinity. Pair and union names give pairing and union. For separation, restrict a name's members to conditions forcing the defining formula. For replacement, the definable forcing relation lets ground axiom schema of collection bound a set of names for all possible witnesses to the unique outputs; evaluating their collected name gives the range. For power set, let $\tau$ name the given set and let $D$ be the set of its member-names. Every subset of ${\tau }_G$ has an equivalent name drawn from $\mathcal{P}(D\times P)$, by the truth lemma, so a ground set of candidate names collects all its subsets. Finally choose a ground well-order of the relevant names; its evaluated image surjects onto the desired set, and choosing the first name for each value well-orders that set. This is why ordinary forcing over a choice model preserves choice.

For a concrete example, Cohen forcing consists of finite partial functions $\omega \to 2$, ordered by extension. The generic union $c=\bigcup G$ is total because deciding each coordinate is dense. For every ground real $x$, the set of conditions disagreeing with $x$ somewhere is dense, so $c\ne x$. This construction changes the universe by adding a genuinely new real without changing its ordinals.

The size and compatibility of conditions determine what else changes. With the countable chain condition for forcing, an ordinal-valued name has only countably many possible values at each coordinate: take a maximal antichain deciding that value. Therefore the possible range of a name for a map with infinite ground domain of cardinality $\mu$ lies in a ground set of size at most $\mu \cdot {\aleph }_0=\mu$. This prevents cardinal collapse and changes of uncountable regular cofinalities. Forcing by finite partial functions $\lambda \times \omega \to 2$ is ccc: the delta-system lemma thins any uncountable family of finite domains to a delta-system, and a further thinning makes their values agree on its finite root. Two remaining conditions are compatible. Distinct coordinates add distinct reals.

For example, start with GCH and take $\lambda ={\aleph }_2$. This forcing has size $\lambda$ and adds $\lambda$ distinct reals. A nice name for a real uses countably many antichains, and each antichain is countable. The ground arithmetic ${\lambda }^{{\aleph }_0}=\lambda$ bounds the number of such names by $\lambda$. Hencegiving a relative-consistency example of the failure of CH. The ground choice of GCH is available through the constructible universe; no claim that every starting model has this arithmetic is needed.

By contrast, countably closed forcing adds no new countable sequences of ground ordinals. Given a name, recursively strengthen a condition to decide each coordinate, then take a lower bound of the descending sequence. That condition decides the entire sequence. Closure and chain conditions thus control different features; neither should be silently substituted for the other.

Further applications include changing cofinalities, adding branches through trees, and constructing prescribed continuum patterns. If the aim is to violate choice, an ordinary generic extension of a choice model will not do: one restricts to a suitable symmetric collection of names, checking the axioms again. These examples also mark a limitation: forcing proves relative consistency, not absolute consistency of the background theory. The countable-transitive-model picture gives a concrete semantic construction; the definable forcing relation and Boolean-valued formulation supply the corresponding formal consistency arguments without asserting that a transitive ground model can be proved to exist.

For unrestricted consistency self-strengthening is inconsistent, again take $A=S+\neg {\mathrm{Con}}_S$. In $S^{++}$ the axiom ${\mathrm{Con}}_S$ and the preceding implication prove ${\mathrm{Con}}_A$. The additional rule then proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$.

However consistency of an extension implies consistency of its subtheory by the formalized inclusion of proofs: $S⊢{\mathrm{Con}}_A\to {\mathrm{Con}}_S$. Thus the ordinary theory $A+{\mathrm{Con}}_A$ contains $\neg {\mathrm{Con}}_S$ and derives ${\mathrm{Con}}_S$, so it has a finite contradiction proof. Checking that concrete proof in arithmetic gives $S⊢\neg {\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. This theorem is also present in $S^{++}$, contradicting the result of the new rule. Therefore $S^{++}$ is inconsistent.

The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false consistency assertions. A true external consistency progression for a specified sound system is not this unrestricted inference rule.

For Rosser separation by a bounded stage comparison, use the numeralwise enumeration in arithmetic properties meant by enumeration in $S$: membership supplies some standard stage with a provable positive instance, while nonmembership makes every standard-stage instance refutable. These are stronger than merely attaching a ${\Sigma }_1$ syntactic label to an arbitrary formula. The finite-initial-segment axiom lets us combine finitely many numeralwise refutations into a bounded universal assertion.

If $n$ is provable, choose a standard stage $p$ with $S⊢P(\overline{n},\overline{p})$. Consistency means $n$ is not refutable. Therefore $S⊢\neg R(\overline{n},\overline{j})$ for each $j\le p$. Using the displayed finite-segment axiom and equality substitution, combine these proofs to get $S⊢\forall z\le \overline{p}\neg R(\overline{n},z)$. Existential introduction with stage $p$ proves the separator at $n$.

If $n$ is refutable, choose a standard stage $q$ with $S⊢R(\overline{n},\overline{q})$. Consistency implies that $n$ is not provable, so all standard instances of $P(\overline{n},\cdot )$ are refutable. In particular their finitely many instances through $q$ give $S⊢\forall z\le \overline{q}\neg P(\overline{n},z)$. For an arbitrary proposed witness $z$, the total-comparison axiom gives $z\le \overline{q}$ or $\overline{q}\le z$. In the first case its $P$ conjunct fails; in the second case the known $R$ instance at $q$ contradicts its bounded no-refutation conjunct. Generalize on $z$ to refute the existential separator. Hence the proposed first-proof-before-refutation formula separates the two sets.

The literal semantic hypothesis is insufficient: a semantic Gödel fixed point need not be canonical. A sentence can be false and provable in a consistent, unsound arithmetic theory, in which case both sides of the stipulated semantic biconditional can be false.

For a concrete counterexample, assume PA is consistent and set $S=\mathrm{PA}+\neg {\mathrm{Con}}_{\mathrm{PA}}$. Gödel's second incompleteness theorem makes this extension consistent: otherwise PA would prove its own consistency. It is still bounded-complete. Use ordinary numeralwise proof and refutation enumerators for this recursively axiomatized theory, and take $G=\neg {\mathrm{Con}}_{\mathrm{PA}}$. This $G$ is false in the standard natural numbers but is an axiom of $S$. Since it is provable, $\exists yP(┌G┐,y)$ is true; its negation is false. Thus the semantic fixed-point biconditional required in this part is true, with both sides false.

Choose $R$ by the usual canonical Rosser construction for these proof matrices. Its undecidability follows from the preceding parts, and it is a true ${\Pi }_1$ sentence: if it were false, its true ${\Sigma }_1$ negation would be provable in this bounded-complete theory, contradicting undecidability. Hence $G$ is false and $R$ true, so their proposed semantic equivalence is false. This counterexample meets the literal assumptions and does not exploit a missing source page.

Under the intended canonical ${\Pi }_1$ Gödel/Rosser convention, the expected answer does hold. Consistency plus bounded completeness implies ${\Pi }_1$ soundness: a false ${\Pi }_1$ theorem has a standard bounded counterexample whose negation the theory proves. If canonical $G$ were false, its truth fixed point would make it provable, contradicting this soundness; thus $G$ is true. Canonical $R$ is true by the preceding ${\Sigma }_1$-negation argument, so both canonical sentences are true and their equivalence is true. This last conclusion needs that canonical construction or an equivalent additional restriction; truth of a biconditional alone does not supply it.

Use the two formal consistency equivalences expressly supplied for this part. If $S⊢G\leftrightarrow R$, the derivability conditions give $S⊢\square \neg G\leftrightarrow \square \neg R$. Taking negations and applying those supplied equivalences yieldsOne-consistency implies ${\Sigma }_1$ soundness under bounded completeness. Hence $S+{\mathrm{Con}}_S$ is consistent: if not, $S$ would prove $\neg {\mathrm{Con}}_S$, a false ${\Sigma }_1$ sentence. But in that consistent extension the last equivalence and its consistency axiom prove its own consistency ${\mathrm{Con}}_{S+{\mathrm{Con}}_S}$. Gödel's second incompleteness theorem rules this out. ThereforeThis establishes the requested unprovability using the explicit formal hypotheses, without inferring internal provability from the semantic equivalence discussed in the preceding part. The hypotheses for the second theorem are the standard effective arithmetic presentation and adequate provability predicates stipulated here.

GL has all classical propositional tautologies, the normal distribution axiom $\square (A\to B)\to (\square A\to \square B)$ and the Löb axiom $\square (\square A\to A)\to \square A$, closed under uniform substitution, modus ponens and necessitation of theorems. We use its derived positive-introspection theorem $\square A\to \square \square A$, normal boxed reasoning, and the boxed replacement principle supplied in the question.

For completeness, positive introspection follows from these axioms. Put $C=A\wedge \square A$. Distribution gives $\square C\to \square A$, so propositional logic proves $A\to (\square C\to C)$. Necessitate and distribute to get $\square A\to \square (\square C\to C)$; Löb's axiom gives $\square A\to \square C$, and boxing $C\to \square A$ finishes $\square A\to \square \square A$.

For a GL fixed point by truth substitution, set $\top =(\perp \to \perp )$, $U=\square Y(\top )$ and $V=\square Y(U)$. From the tautology $U\to (\top \leftrightarrow U)$, boxed reasoning gives $\square U\to \square (\top \leftrightarrow U)$. The supplied replacement principle and distribution then giveSince $U$ is itself boxed, positive introspection gives $U\to \square U$, and hence $U\to V$.

For the reverse direction, the displayed implication entails the theorem $V\to (\square U\to U)$. Necessitate it and distribute to obtain $\square V\to \square (\square U\to U)$. Since $V$ is boxed, $V\to \square V$ holds. The Löb axiom therefore yields $V\to \square U$, and the same displayed implication then yields $V\to U$. ConsequentlyAll occurrences of the unknown letter have been removed from $U$ by substitution of truth; any other parameter letters remain available. The proof does not assume the invalid reflection principle $\square U\to U$ as an unconditional axiom.

The fixed point of boxed negated provability gives, in fact, that GL proves $F\leftrightarrow \square \perp$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, positive introspection and necessitation of that equivalence give $F\to \square F$. Another introspection step gives $F\to \square \square F$. The stipulated fixed point also gives $F\to \square \neg \square F$. Combining these two boxed contradictories yields $F\to \square \perp$. Conversely $\square \perp \to \square \neg \square F$ follows by normal boxed explosion, and the fixed point then yields $\square \perp \to F$.

Arithmetical soundness of GL, proved by translating distribution into the second derivability condition, necessitation into the first, and Löb's axiom into its internal arithmetic theorem, now givesAny remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is one-consistent, it is consistent and ${\Sigma }_1$ sound. Its standard provability predicate for a contradiction is then a false ${\Sigma }_1$ sentence and cannot be a theorem. Hence $F^{\ast }$ is not provable in PA. Moreover its negation is equivalent to PA's consistency statement and is unprovable by the second incompleteness theorem. Thus this fixed point is, under the stated hypothesis, undecidable rather than an unboxed reflection principle.

Under the deductively closed convention, an $L$-theory is a set of $L$-sentences containing all its first-order logical consequences: if $T\models \varphi$, then $\varphi \in T$. By completeness this is equivalent to closure under provability. An axiom set is often called a theory too, with its deductive closure understood. Neither convention by itself requires completeness or satisfiability; an inconsistent deductively closed theory contains every sentence.

No. Universal sentences are preserved under substructures. Every infinite $K$-vector space has its zero subspace as an $L$-substructure, since zero is named and every scalar multiplication preserves it. This one-element structure is not infinite and is not a model of $T$. Thus the model class is not closed under substructures and has no universal axiomatization, even relative to the vector-space axioms.

Use the vector-space axioms: addition is an abelian group operation with identity zero; ${\lambda }_1(x)=x$; ${\lambda }_a{\lambda }_b(x)={\lambda }_{ab}(x)$; ${\lambda }_a(x+y)={\lambda }_a(x)+{\lambda }_a(y)$; and ${\lambda }_{a+b}(x)={\lambda }_a(x)+{\lambda }_b(x)$, with ${\lambda }_0(x)=0$. Group inverses may be expressed by ${\lambda }_{-1}$, so no extra inverse symbol is needed.

Add the dimension-unbounded schemeOver a finite field, a finite-dimensional space has finitely many Elements, while every infinite-dimensional space is infinite. Hence this scheme axiomatizes exactly the infinite underlying vector spaces requested. In this finite-field case the vector-space axiom list itself is finite; the infinitude of the additional dimension scheme is substantive.

No. If a finite conjunction $\varphi$ axiomatized the infinite spaces, it would follow from the vector-space axioms together with all the $D_n$. Compactness would make it follow from finitely many of those axioms and dimension requirements. Let $N$ be at least every dimension mentioned there. The finite-dimensional space $K^N$ satisfies all vector-space axioms and those finitely many $D_n$, hence would satisfy $\varphi$. But it is a finite set and so cannot be a model of the purported axiomatization. This contradiction proves failure of finite axiomatizability, including finite axiomatizability relative to vector spaces.

The cardinality of a vector space is central: here “infinite” must continue to refer to the underlying set. Over a countably infinite field, every nonzero finite-dimensional space is already infinite. Thus the model class now consists of all nonzero $K$-vector spaces, not only infinite-dimensional ones.

Since independence of a pair is not definable over an infinite field, for (i), independence of a single vector is still $x\ne 0$, but independence of tuples of length at least two is not definable by one formula in this one-sorted language. Quantifier elimination follows from the linear-equation argument in the preceding part for all these infinite domains. Any candidate two-variable formula therefore involves only finitely many linear equations. Take an independent pair, and compare it with $(x,{\lambda }_{a}x)$, where $x\ne 0$ and $a\in K$ avoids the finitely many ratios making one of those nontrivial equations vanish. Both pairs satisfy the same listed atomic formulas, contradicting a proposed definition of independence. Longer tuple independence would define pair independence by existentially completing a pair inside an infinite-dimensional model, giving the same obstruction.

For (ii), the vector-space axiom schema together with $\exists x(x\ne 0)$ axiomatizes the infinite underlying spaces. For (iii), there is again no universal axiomatization, because the zero subspace is a substructure.

For finite axiomatizability with infinitely many scalar symbols, in (iv) there is no finite axiomatization in the full language: any finite axiom set mentions only finitely many scalar symbols. In a nonzero vector space alter an unused nonzero ${\lambda }_a$ to send zero to a nonzero vector, retaining all mentioned interpretations. The finite sentences keep their truth values, but a vector-space axiom is now false. Relative to the already imposed vector-space axioms, the extra condition is finitely axiomatized by the single nonzero-vector sentence. These absolute and relative answers must be distinguished.

For (v), the one-variable algebra still has two atoms and four Elements. In two variables the isolated atoms are $(0,0)$ and the countably many rank-one directions, represented by $x\ne 0,y={\lambda }_{a}x$ and by $x=0,y\ne 0$. There is also a nonisolated complete type of an independent pair. A formula using finitely many linear equations either picks finitely many isolated atoms, or contains that independent type and all but finitely many isolated atoms. Therefore $F_2/E_2(T)$ is the finite-cofinite Boolean algebra on a countably infinite set of atoms, with the independent type the extra nonisolated point in its Stone space. In particular this algebra is countably infinite, rather than the full power set of its atoms.

For (vi), dimension can be $1,2,3,\dots$ or ${\aleph }_0$ while the domain is countable, producing pairwise nonisomorphic countable models. Thus $T$ is not countably categorical. For an uncountable $\kappa$, a vector space over this countable field has cardinality $\kappa$ exactly when its dimension is $\kappa$, since in general a nonzero space has size $\max (|K|,\dim V)$ when that maximum is infinite. Basis bijections then give categoricity in every uncountable cardinal. Quantifier elimination also shows that these different positive dimensions are elementarily equivalent; independence of an arbitrarily long tuple is not being silently treated as definable over this infinite field.

The analytic-synthetic distinction is proposed as a distinction between kinds of truth, not as an empirical discovery about a particular substance or force. An analytic truth is supposed to hold through meaning and logic; a synthetic truth depends additionally on how the world is. The absence of a laboratory discovery establishing that division neither automatically refutes it nor grants it immunity from criticism. Its status depends on whether a clear and useful distinction can be specified.

Consider an explicitly defined language. Let $B(x)$ mean bachelor, $U(x)$ unmarried, and admit the meaning postulateEvery interpretation admitted by that rule makes the sentence true. This is a precise relative notion of analyticity: the rule helps determine what the symbols mean. By contrast, a claim about how many people satisfy $B$ requires information about the population. The latter is not made true merely by adopting a vocabulary. Rudolf Carnap's meaning postulates explain how a chosen language can impose such semantic constraints without reducing every analytic sentence to a visible repetition of its subject.^[ref]

Two further distinctions must be kept separate. Analyticity concerns meaning and truth conditions; knowing something independently of a particular empirical investigation concerns justification. Necessity concerns whether it could have been otherwise. Treating these as interchangeable would assume rather than establish the most controversial part of the account. Even a conventional choice of language can generate nontrivial consequences whose derivation requires considerable reasoning.

Willard Van Orman Quine challenges a sharp, framework-independent boundary. An explanation of analyticity by synonymy may presuppose analyticity when explaining what counts as genuine synonymy. A dictionary records accepted usage; it does not independently establish why substitution preserves truth by meaning alone. The wider argument rejects the assumption that each empirical sentence confronts experience in isolation. Definitions, background assumptions and substantive claims work together in an evidential system. This is a philosophical criticism of proposed accounts, not an experimental finding that two previously measurable truth-types are physically identical.^[ref]

For philosophy of science, the important consequence is that neither logic nor observation should be credited with doing the other's work. In Euclidean geometry, a conclusion can follow from specified axioms; whether physical space satisfies the relevant geometry is a separate issue. Similarly, defining momentum as $mv$ in a model does not alone establish that this quantity is conserved in every physical interaction. A formal relation can be fixed by stipulation while the model's applicability remains empirical.

The best position is therefore neither that science has discovered an absolute cleavage nor that all useful distinctions disappear if an absolute cleavage fails. Analyticity relative to explicit rules is intelligible; an unrevisable division of all scientific language requires further argument. Scientific practice can retain definitions, deduction and a distinction between stipulation and measurement while allowing revision of frameworks and rejecting a simple separation of completely theory-free observations from an eternally fixed conceptual scheme.

Use the already proved inference in (a) on the negated existential premise. Eliminate the remaining existential with a fresh witness $u$, which must not appear in the final conclusion or the other undischarged assumptions.

1  ∃x P(x)                              premise
2  ¬∃x (Q(x) → P(x))                    premise
3  ∀x (P(x) → Q(x))                     derivation in (a), from 2
4  | P(u)                               fresh-witness assumption for 1
5  | P(u) → Q(u)                        ∀-elim, 3
6  | Q(u)                               →-elim, 4 and 5
7  | P(u) ∧ Q(u)                        ∧-intro, 4 and 6
8  | ∃x (P(x) ∧ Q(x))                   ∃-intro, witness u
9  ∃x (P(x) ∧ Q(x))                     ∃-elim, 1, subproof 4–8

The result in (a) is a proved dependency, not an additional axiom. The witness introduced at line 4 does not escape its subproof.

Proof theory studies formal proofs and the deductive systems that produce them. It examines which conclusions follow from axioms, how proofs can be transformed, and what those transformations reveal about the chosen logic. Natural deduction organizes a proof through introduction and elimination rules for logical connectives and quantifiers.

For disjoint sets numeralwise enumerated by $P,R$, finite-initial-segment and total-comparison axioms let $H$ separate the first set from the second in the theory. For a member of the first set use a positive $P$ stage and finitely many refutations of $R$. For a member of the second set use its positive $R$ stage: earlier proposed $P$ stages are all refuted by a finite bounded proof, while later stages lose to that known $R$ witness. This proves a separator without inferring arbitrary negative facts from the mere Sigma-1 form of the enumerators.

Set theory studies sets, their set elements, and the constructions and sizes possible for them. It supplies a shared vocabulary for mathematics: a function connects two sets, a binary relation specifies which pairs of objects are related, and a probability space starts with a set of possible outcomes. Giving these objects a common language lets a construction from one subject be used in another without repeating its underlying bookkeeping.

A particularly beautiful question is how to compare sizes without first assigning a number. Two sets have the same cardinality when a bijection pairs every member of one with exactly one member of the other. For finite sets, this agrees with ordinary counting. For infinite sets, it produces surprises: $n\mapsto 2n$ bijects the natural numbers with the nonnegative even integers, and the Cantor pairing function bijects the Cartesian product ${\mathbb{N}}^2$ with $\mathbb{N}$. A proper subset can have the same cardinality as its containing set.

This does not make all infinite sets equally large. Cantor's diagonal argument shows that all infinite binary sequences cannot be listed by the natural numbers. Cantor's theorem gives the wider principle: the power set of any set has strictly greater cardinality. The contrast between an explicit enumeration and an impossibility argument makes the meaning of infinity much sharper than a picture of something merely continuing forever.

Set formation itself requires care. Russell's paradox shows why not every condition defines a set of all objects satisfying it. Zermelo–Fraenkel set theory instead uses axioms specifying permitted constructions, including set comprehension within a previously given set. The restrictions are useful: they let us form the collections ordinary arguments need while blocking the unrestricted construction that produces the paradox.

Consider extending $S+{\mathrm{Con}}_S$ by a rule sending every ${\mathrm{Con}}_A$ to ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. Put $A=S+\neg {\mathrm{Con}}_S$. The initial consistency axiom proves ${\mathrm{Con}}_A$ by the negated-consistency extension theorem, so the rule proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. But ${\mathrm{Con}}_A\to {\mathrm{Con}}_S$ is provable by inclusion of proofs, making $A+{\mathrm{Con}}_A$ inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.