The Levi problem: pseudoconvexity, domains of holomorphy, and holomorphic convexity

Given: The Axiom of Choice and a domain $\mathrm{\Omega }\subseteq {\mathbb{C}}^n$, $n\ge 1$.

Hartogs pseudoconvexity gives a continuous plurisubharmonic exhaustion on $\mathrm{\Omega }$ (Hartogs pseudoconvexity yields a continuous plurisubharmonic exhaustion).

In Demailly, Complex Analytic and Differential Geometry, Ch. I §7.A, Theorem 7.2(c) implies (e): a plurisubharmonic exhaustion on a proper open subset of ${\mathbb{C}}^n$ makes $-\log d(z,{\mathbb{C}}^n\setminus \mathrm{\Omega })$ plurisubharmonic, which is his pseudoconvexity criterion. Ch. VIII §9, Theorem 9.11(a), printed pp. 392–393, says that an open subset of ${\mathbb{C}}^n$ is a domain of holomorphy if and only if it is pseudoconvex. Its proof of the forward implication used here applies Skoda's Theorem 9.10 to the coordinate functions $z_j-a_j$ at a boundary point $a$ with a plurisubharmonic distance weight; the resulting identity ${\sum }_j(z_j-a_j)h_j=1$ prevents common holomorphic continuation across $a$.

For a domain in ${\mathbb{C}}^n$, being a domain of holomorphy is equivalent to holomorphic convexity (Cartan-Thullen theorem).

Every domain of holomorphy in ${\mathbb{C}}^n$ is Hartogs pseudoconvex (Domains of holomorphy are Hartogs pseudoconvex).

The holomorphic hull of a compact set is closed in its ambient domain and bounded in each coordinate (Basic properties of the holomorphic hull). A closed bounded subset of ${\mathbb{C}}^n\cong {\mathbb{R}}^{2n}$ is compact (Complex $m$-space and its real coordinate dictionary, Heine-Borel in ${\mathbb{R}}^n$: with the Euclidean metric a subset of ${\mathbb{R}}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

AC supplies the ambient choice assumptions of the source theorem and the cited library interfaces (The Axiom of Choice).

Choice use. AC is the stated ambient hypothesis. The proof itself makes no new arbitrary selection; the nontrivial existence theorem imported in [F2] is used under its classical choice setting.