The axiom of dependent choice is a weak version of the axiom of choice, still stronger than the axiom of countable choice. Its multiple (equivalent) formulations, include the following.
4. ⇒ ACℕ : from any sequence E of nonempty sets,
let R = (En×En+1)n∈ℕ.
ACE ⇒ 1. : if f∈EE satisfies
∀x∈E, xRf(x) then
u = (fn(a))n∈ℕ fits.
A generalized formulation of DC uses an R⊂(∐n∈ℕEn)×E, to modify 1. by the more sophisticated condition ∀n∈ℕ, (uk)k<n R un. It can be deduced from 5. like with the above proof of 5. ⇒ 1.
Proof. Assuming DC, let K ≠ ∅ the set of countable subsets of E, and
R = {(A,B)∈K2 | A ⊂ B ∧ LA ∩ Dom E ⊂ E⋆B}
Dom R = K because, applying countable choice to the countable set LA ∩ Dom E,∃f : LA ∩ Dom E → E, Gr f ⊂ E ∴ (A, A∪ Im f)∈R
Hence by DC 2.∃A ∈ Kℕ, ∀n∈ℕ, An ⊂ An+1 ∧ LAn ∩ Dom E ⊂ E⋆An+1
Taking then F = ⋃n∈ℕ An,∀(s,u)∈LF, ∃n∈ℕ, Im u ⊂ An
LF ∩ Dom E = ⋃n∈ℕ LAn ∩ Dom E
⊂ E⋆⋃n∈ℕ An+1 = E⋆F
In particular if E is an L-algebra then F is a countable subalgebra of E (namely the minimal subalgebra of E if following the construction starting with ∅).
The downward Löwenheim–Skolem Theorem, says that under the axiom of choice, any infinite system E
with countable language, has elementary subsystems (3.4.) with any infinite cardinalities
from |ℕ| to |E|.
We did not work enough with infinite cardialities to reach that generality, but from the above, we get
the existence of a countable elementary subsystem F, as an equivalent formulation of DC.
Indeed a formula in prenex form with parameters in F and true in E, will stay true
in F just if the truth of all its existential quantifiers is preserved;
and this can be written LF ∩ Dom E ⊂ E⋆F after converting
existential quantifiers into operation symbols added to L.
Reference : paper
by Asaf Karagila - message and paper
by Christian Espindola.
Let us define a diagram D over a given category C, as the data of
∀i,j∈I, ∀f∈Kij, f∘ψi = ψj
The cones to D form a co-action of C, namely the sub-co-action of the product of the C(Xi), given by the intersection of equalizers Eq(f∘πi, πj) for all i,j∈I and f∈Kij. Then a co-egg of this co-action is called a limit of D. It is in the same way an intersection of equalizers inside a product in C, if these concepts are well-defined there.From the results of 3.9 and 3.10, for any morphism b in C, any limit of a diagram made of b-modules is also a b-module.
The condition remains unchanged when replacing D by the small category it generates, i.e. with I as set of objects, and the sets Kij, once completed with the composites of their elements and the identity elements, become its sets of arrows. For this reason, without loss of generality, a diagram can be assumed to be a small category. At least, let us qualify a diagram as stable if it is stable by composition.
The condition for ψ to be a cone from N to a stable diagram D, can be rephrased saying the extended diagram D' = D ∪ ψ, namely with I' = I∪{N} ≠ I and K'Nj = {ψj}, remains stable; then N is an initial object of the resulting small category (after adding identity elements).
If D is already a small category with an initial object 0∈I then X0 naturally serves as a limit of D.
A projective limit is the limit of a special kind of diagram, called a projective system. It is a nonempty diagram such that:
∀i,j∈I, i ≤ j ⇔ Kji ≠ ∅ ⇒ Kji = {fij} ⊂ Mor(Xj,Xi)
If J ⊂ I is such that ∀i∈I, ∃j∈J, i ≤ j then the natural projection from cones over I to cones over J, is bijective. It thus forms an isomorphism in C between projective limits. Examples :
In the category of sets, over any fixed directed set (I,≤), there is equivalence between
Yi = ⋂i≤j Im fij ⊂ Xi
which is non-empty, otherwise Xk would be empty for an upper bound k of a tuple j∈IXi such that∀x∈Xi, i≤jx ∧ x∉ Im fijx
To check that ∀i,j∈I, i≤j ⇒ fij[Yj] = Yi, the proof of Yi ⊂ fij[Yj] is easy, while that of fij[Yj] ⊂ Yi uses directedness.2. ⇒ 1. : assuming all fij surjective, for any i∈I and x∈Xi, let
∀j∈I, Yj = ⋃{fjk[fik•(x)] |k∈I ∧ i≤k ∧ j≤k}
It is easy to see that∀j∈I,
Yj ≠ ∅
∀j,l∈I, j≤l ⇒ fjl[Yl] ⊂ Yj
Yi = {x}.
Another, less obvious option for 2. ⇒ 1. is
∀j∈I, Yj = {y∈Xj|∀k∈I, (k≤i ∧ k≤j) ⇒ fki(x) = fkj(y)}
Still, Yj ≠ ∅ because
∃m∈I, ∃z∈Xm, i≤m ∧ j≤m
∧ fim(z) = x
∀k∈I,
(k≤i ∧ k≤j) ⇒ fki(x) = fkm(z) =
fkj(fjm(z))
∀y∈Yl, ∀k∈I, (k≤i ∧ k≤j) ⇒ fki(x) = fkl(y) = fkj(fjl(y))
Still another way involves first taking the projective limit of the fij•(x) over ≤⃗(i).The generalization of 1. to infinite sets is a version of the axiom of choice, hard to deduce except when assuming that I is countable, in which case it is easily equivalent to dependent choice (DC 5.).
2. can be seen as a generalized form of the completeness theorem of propositional logic, also known as the compactness theorem, which we quickly deduced and used in the countable case without the axiom of choice, near the end of our proof of the completeness theorem. To extend the completeness theorem to theories with uncountable language, involves at that step the (roughly) full version of 2. (using the axiom of choice except in special cases). The other needed change is, we need term algebras for uncountable languages. These may be constructed as synonymity classes of terms; another construction of these will be done below.
The generalization of 2. to infinite sets is false. A counter-example is given by I=ℕ, Xi=ℕ\Vi and fij = IdXj.
∀i,j∈I, i≤j ⇒ ϕj∘fij = ϕi
The construction of colimits and inductive limits in the category of sets, usually forms the bulk of their construction in other concrete categories.{((i,x),(j,y))∈U2 | ∃k∈I, i≤k ∧ i≤j ∧ fik(x) = fjk(y)}
Let us qualify an inductive system as injective if all fij are injective ; then all ϕi of the inductive limit are also injective.As a first example, the ground term algebra over any infinite language L, is the inductive limit in the category of L-systems, with I = ℘fin(L) with the inclusion order, Xi a ground i-term algebra, and for any i≤j, fij the unique i-morphism from Xi to Xj (which is injective, and also an L-morphism).
A second example is the construction of objects with infinite basis in any concrete category,
out of those with bases of all finite cardinalities. For any two objects with equinumerous bases,
every bijection between bases is uniquely extensible as an isomorphism. Thus, all
objects with a finite basis are essentially described, up to isomorphism, by a sequence of objects with basis
Vn for every n∈ℕ. Now let
B an infinite set, I = ℘fin(B) with the inclusion order,
Xi an object with basis i for every i∈I, and fij the unique
morphism extending Idi. This forms an injective inductive system, since, as mentioned earlier,
all fij are sections.
It is easy to see that any object with basis B
is its inductive limit in the given category, and that, in the general case, its inductive
limit in the category of sets is naturally a subset of it.
In practice, both will usually coincide.
In particular for categories of algebras, for any inductive system of algebras, its inductive limit as defined in
the category of sets is also naturally an algebra. So the above constructed inductive limit of
algebras with finite basis, is an algebra, and thus is also an object (and the inductive limit in that category)
just if that category admits an object with
basis B and if any subalgebra of an object is also an object.
(the proof makes crucial use of the axiom of infinity in the form of infinite products; if only assuming stability of a class of finite algebras by finite products, the result no more holds, although a counter-example may fail to be expressible in finite set theory, as its definition uses a quantifier in ℕ ; the theorem may then be replaced by the more complicated Reiterman's theorem involving another concept of equations with infinite sizes)
Let us split it in two easier statements:
Q is stable by intersections because any intersection ⋂i∈I Ri of congruences from Q, is the congruence of
⊓i∈I πi ∈ Mor(TB, ∏i∈I M/Ri)
whose image is a subset of a product, thus in C according to (S) and (P).B is a basis of FB = TB/⋂Q in C because
Proof 2. Let N be any algebra which satisfies them.
Let B be any generating subset of N (possibly B = N).
The unique f∈ Mor(TB, N) satisfies
∼B ⊂ ∼f. So
f/∼B ∈ Mor(FB, N) is a quotient.
By (H), since FB is in C we conclude N is in C.∎