[proofplan] We force over the given countable transitive model $M$ with the finite-support iteration $\mathbb P_\kappa$. The [finite-support iteration theorem for ccc forcing](/theorems/6573) gives that the whole iteration is ccc, while the cardinal arithmetic hypotheses keep the final forcing of size $\kappa$. The bookkeeping then ensures that every small ccc forcing problem with fewer than $\kappa$ dense sets appears at some stage, where the stage generic meets the required dense sets; later forcing does not remove this filter. Finally, the repeated Cohen stages give at least $\kappa$ reals, while the ccc size bound gives at most $\kappa$ nice names for reals, so the continuum is exactly $\kappa$. [/proofplan]

[step:Force with the finite-support iteration and preserve ZFC and cardinals] Let $G\subseteq\mathbb P_\kappa$ be an $M$-generic filter, and for each $\alpha\leq\kappa$ let $G_\alpha:=G\cap\mathbb P_\alpha$ denote the induced $M$-generic filter for $\mathbb P_\alpha$. By hypothesis, each iterand is forced by the previous stage to be ccc. Therefore the finite-support iteration theorem for ccc forcing implies, by induction on $\alpha\leq\kappa$, that every $\mathbb P_\alpha$ is ccc in $M$. In particular, $\mathbb P_\kappa$ is ccc. Since $M\models\mathrm{ZFC}$, the forcing preservation theorem for ZFC over transitive models gives $M[G]\models\mathrm{ZFC}$. By the ccc cardinal-preservation theorem, forcing with $\mathbb P_\kappa$ preserves cardinals and cofinalities at least $\omega_1^M$. In particular, it preserves $\omega_1^M$ and preserves the fact that $\kappa$ is a cardinal. Thus $\omega_1^{M[G]}=\omega_1^M$. Since $M\models\kappa>\omega_1^M$, we have $\kappa>\omega_1^{M[G]}$ in the final extension. [/step]

[step:Bound the size of the final forcing by $\kappa$]We verify the size estimate for the iteration using the standard size lemma for finite-support iterations: if $\kappa$ is regular, $\kappa^{<\kappa}=\kappa$, the length is at most $\kappa$, and each iterand is forced to have size $<\kappa$, then the finite-support iteration has size at most $\kappa$, and every proper initial segment of length $<\kappa$ has size $<\kappa$. The lemma is proved by choosing in $M$, for each $\alpha<\kappa$, a $\mathbb P_\alpha$-name $\dot e_\alpha$ for a surjection from some ordinal $\mu_\alpha<\kappa$ onto $\dot{\mathbb Q}_\alpha$. Thus every coordinate value in a condition may be represented by a name indexed below $\mu_\alpha$, so a condition in $\mathbb P_\gamma$ is coded by a finite subset of $\gamma$ together with finitely many ordinals below $\kappa$ and finitely many relevant deciding conditions from earlier stages. Inducting on $\gamma\leq\kappa$, regularity of $\kappa$ and $M\models\kappa^{<\kappa}=\kappa$ bound the number of such finite codes by $\kappa$. If $\gamma<\kappa$, the same induction gives $|\mathbb P_\gamma|<\kappa$, because the union of fewer than $\kappa$ many sets of size $<\kappa$ again has size $<\kappa$. Hence $|\mathbb P_\kappa|\leq\kappa$. For the reverse inequality, let $S\subseteq\kappa$ be the set of stages at which the bookkeeping schedules Cohen forcing, so $|S|=\kappa$ in $M$. For each $\beta\in S$, let $p_\beta\in\mathbb P_\kappa$ be the condition with support $\{\beta\}$ whose $\beta$-coordinate is the Cohen condition deciding the first bit to be $1$, and whose other coordinates are trivial. If $\beta\neq\gamma$, then $p_\beta$ and $p_\gamma$ have different supports, hence they are distinct conditions. Thus $\{p_\beta:\beta\in S\}$ witnesses $|\mathbb P_\kappa|\geq\kappa$, and therefore $|\mathbb P_\kappa|=\kappa$.[/step]

[guided]The point of the size calculation is that the iteration is long enough to handle $\kappa$ many forcing problems, but not so large that it creates more than $\kappa$ many names for reals. We use the standard size lemma for finite-support iterations. The hypotheses of that lemma are exactly the present ones: the length is $\kappa$, the cardinal $\kappa$ is regular, $M\models\kappa^{<\kappa}=\kappa$, and each $\mathbb P_\alpha$ forces $|\dot{\mathbb Q}_\alpha|<\kappa$. Here is the coding behind the lemma. For each $\alpha<\kappa$, choose in $M$ a $\mathbb P_\alpha$-name $\dot e_\alpha$ and an ordinal $\mu_\alpha<\kappa$ such that $\mathbb P_\alpha$ forces that $\dot e_\alpha:\mu_\alpha\to\dot{\mathbb Q}_\alpha$ is surjective. A finite-support condition $p\in\mathbb P_\gamma$ is determined by its finite support $\operatorname{supp}(p)\subseteq\gamma$ and, for each $\alpha\in\operatorname{supp}(p)$, by a $\mathbb P_\alpha$-name for a condition in $\dot{\mathbb Q}_\alpha$. Using $\dot e_\alpha$, every such coordinate name can be replaced by a name for an ordinal below $\mu_\alpha$, together with the earlier forcing information that decides enough of that ordinal-name to define the coordinate. By the inductive hypothesis, the earlier forcing has size $<\kappa$ at proper stages and size at most $\kappa$ at the endpoint, so the number of possible earlier pieces of deciding information is bounded by $\kappa$. Now induct on $\gamma\leq\kappa$. A condition in $\mathbb P_\gamma$ has finite support contained in $\gamma$. For each coordinate in that finite support, the possible coded coordinate data has size at most $\kappa$, and at proper stages below $\kappa$ it has size $<\kappa$. Therefore the set of all codes for conditions in $\mathbb P_\gamma$ injects into the set of finite sequences drawn from $\gamma\times\kappa$. If $\gamma\leq\kappa$, this has size at most $\kappa^{<\omega}\leq\kappa^{<\kappa}=\kappa$. Hence $|\mathbb P_\kappa|\leq\kappa$. For a proper initial segment $\gamma<\kappa$, the same induction gives the sharper estimate $|\mathbb P_\gamma|<\kappa$. Indeed, all supports are finite subsets of $\gamma$, there are fewer than $\kappa$ possible finite supports, and for each fixed finite support the coordinate data is drawn from fewer than $\kappa$ many possibilities; regularity of $\kappa$ ensures that the union of fewer than $\kappa$ many sets of size $<\kappa$ still has size $<\kappa$. Finally, let $S\subseteq\kappa$ be the set of stages at which Cohen forcing is scheduled, so $|S|=\kappa$. For each $\beta\in S$, form the condition $p_\beta$ whose support is $\{\beta\}$, whose $\beta$-coordinate is the Cohen condition deciding the first bit to be $1$, and whose other coordinates are trivial. Distinct $\beta$ give distinct supports, hence distinct conditions. Thus $|\mathbb P_\kappa|\geq\kappa$, and therefore $|\mathbb P_\kappa|=\kappa$.[/guided]

[step:Use bookkeeping to meet every small dense-set requirement] Work in $M[G]$. Let $\lambda<\kappa$, and consider an arbitrary instance of $\mathrm{MA}_\lambda$ in the final extension. Thus there is a ccc forcing notion $\mathbb R$ and a family $\mathcal D=\{D_\xi:\xi<\lambda\}$ of dense subsets of $\mathbb R$. By the stated reduction lemma, after replacing $\mathbb R$ by a regular suborder preserving the dense-set requirements, this instance is represented at some bounded stage. More precisely, there are $\alpha<\kappa$, a $\mathbb P_\alpha$-name $\dot{\mathbb R}$ for a ccc forcing notion of cardinality $<\kappa$, and a $\mathbb P_\alpha$-name $\dot{\mathcal D}$ for a family of fewer than $\kappa$ dense subsets of $\dot{\mathbb R}$ such that solving the represented problem solves the original instance of $\mathrm{MA}_\lambda$. By the closure property of the bookkeeping, the pair $(\dot{\mathbb R},\dot{\mathcal D})$ appears at some stage $\beta$ with $\alpha\leq\beta<\kappa$. We view the $\mathbb P_\alpha$-names $\dot{\mathbb R}$ and $\dot{\mathcal D}$ as $\mathbb P_\beta$-names via the complete embedding of $\mathbb P_\alpha$ into $\mathbb P_\beta$. Since $G_\beta\cap\mathbb P_\alpha=G_\alpha$, their interpretations at stage $\beta$ are still $\dot{\mathbb R}^{G_\alpha}$ and $\dot{\mathcal D}^{G_\alpha}$. The statement that each member of $\dot{\mathcal D}$ is dense in $\dot{\mathbb R}$ is forced already by $\mathbb P_\alpha$, so it remains true after passing to the larger intermediate model $M[G_\beta]$. At stage $\beta$, the iteration forces with this named ccc forcing notion, so the coordinate generic added at that stage gives a filter $H\subseteq\dot{\mathbb R}^{G_\alpha}$ meeting every member of $\dot{\mathcal D}^{G_\alpha}$. Since the later forcing from stage $\beta+1$ to $\kappa$ only extends the universe and does not remove sets already constructed, the same filter $H$ remains in $M[G]$ and still meets the same dense subsets. Therefore the original instance of $\mathrm{MA}_\lambda$ is satisfied. Because $\lambda<\kappa$ was arbitrary, we conclude $M[G]\models \forall\lambda<\kappa\ \mathrm{MA}_\lambda$. [/step]

[step:Compute the continuum in the final extension] The bookkeeping schedules Cohen forcing at $\kappa$ many stages. At each such stage, the corresponding coordinate generic adds a Cohen real over the model built up to that stage. Since a real added by a later Cohen stage is not already present in the earlier intermediate model, these $\kappa$ many Cohen stages yield at least $\kappa$ distinct reals in $M[G]$. Hence $M[G]\models 2^\omega\geq\kappa$. For the reverse inequality, use the ccc and size bounds for $\mathbb P_\kappa$. By the nice-name theorem for reals under ccc forcing, every $\mathbb P_\kappa$-name for a real can be replaced by a nice name, and a nice name for a real is coded by countably many antichains in $\mathbb P_\kappa$. Since $\mathbb P_\kappa$ is ccc, each such antichain is countable. Since $|\mathbb P_\kappa|=\kappa$ and $M\models\kappa^\omega=\kappa$, there are at most $\kappa$ many countable sequences of countable antichains of $\mathbb P_\kappa$. Therefore there are at most $\kappa$ many nice names for reals, and so $M[G]\models 2^\omega\leq\kappa$. Combining the two inequalities gives $M[G]\models 2^\omega=\kappa$. [/step]

[step:Conclude Martin's Axiom and the failure of CH] We have proved that $M[G]\models \forall\lambda<\kappa\ \mathrm{MA}_\lambda$ and $M[G]\models 2^\omega=\kappa$. Therefore $M[G]\models \forall\lambda<2^\omega\ \mathrm{MA}_\lambda$, which is precisely Martin's Axiom in the stated convention. Since $\mathbb P_\kappa$ is ccc, the ccc cardinal-preservation theorem preserves $\omega_1$ and preserves $\kappa$ as a cardinal. Because $M\models\kappa>\omega_1^M$, the final extension satisfies $2^\omega=\kappa>\omega_1$. Thus $M[G]\models\neg\mathrm{CH}$. We have shown $M[G]\models \mathrm{ZFC}+\mathrm{MA}+\neg\mathrm{CH}$. Consequently, under the same external consistency convention used to supply the countable transitive ground model, the existence of a model of $\mathrm{ZFC}$ yields a model of $\mathrm{ZFC}+\mathrm{MA}+\neg\mathrm{CH}$. Hence $\operatorname{Con}(\mathrm{ZFC}) \implies \operatorname{Con}(\mathrm{ZFC}+\mathrm{MA}+\neg\mathrm{CH})$. [/step]