Let ZF be the ZermeloFraenkel set theory, ZFC be ZF with choice, con(ZF) be the consistency of ZF and con(ZFC) be the consistency of ZFC. Let IN be the hypothesis "There exists one (strongly) inaccessible cardinal". It is known that "ZFC + IN " proves con(ZFC), so also "ZFC + con(ZFC)" and "ZF+ con (ZF)". Question 1: Do we know an hypothesis H such that "ZFC + H" is strictly weaker than "ZFC + IN" but sufficient to prove "ZFC + con(ZFC)"? Question 2: Do we know an hypothesis K such that "ZF + K" is strictly weaker than "ZF+ IN", (with an adequate definition of IN without choice) but sufficient to prove "ZF + con(ZF)" ? Gérard LANG

7$\begingroup$ Let $H$ be Con(ZFC)? Or that there exists an $\omega$model of ZFC, or a wellfounded model of ZFC, or... There are a lot of them. The same answers should apply to your second question. $\endgroup$– Benedict EastaughApr 27 '14 at 10:29

$\begingroup$ Cantor's Attic lists a number of statements strictly below inaccessible, but above Con(ZFC): cantorsattic.info/Upper_attic. $\endgroup$– Joel David HamkinsApr 27 '14 at 11:20

$\begingroup$ Thank you.But how do you prove that "ZFC + con(ZFC)" is strictly weaker that "ZFC + IN" ? $\endgroup$– Gérard LangApr 27 '14 at 11:30

1$\begingroup$ @GérardLang Con(ZFC) is absolute for transitive models of ZF. So, if $\kappa$ is inaccessible, $V_\kappa\vDash ZFC + Con(ZFC)$. So, ZFC + IN will prove Con(ZFC + Con(ZFC)). $\endgroup$– Sam RobertsApr 27 '14 at 12:09
This has been addressed both here and in MSE a few times. See for instance here and here.
If $T_0=\mathsf{ZF}$, and $T_{n+1}=T_n+\mathrm{Con}(T_n)$, then each $T_n$ is strictly stronger than their predecessor. This is immediate from the second incompleteness theorem.
An $\omega$model of set theory is a model whose set of natural numbers is isomorphic to the standard set. The theory $T$ asserting that there is an $\omega$model of $\mathsf{ZF}$ is strictly stronger than all the $T_n$ (by a large margin). This is because any $\omega$model is correct about arithmetic statements. In particular, since there is an $\omega$model $M$ of $\mathsf{ZF}$, then $\mathrm{Con}(\mathsf{ZF})$ holds, but this is an arithmetic ($\Pi^0_1$) statement, so it is true in $M$. Hence $M$ witnesses the consistency of $T_1$, so $\mathrm{Con}(T_1)$ holds, and since this is an arithmetic statement, then it is true in $M$, etc. Note how we can now proceed to iterate" there is an $\omega$model of" and obtain another increasing chain of theories.
The theory $S$ asserting that there is a wellfounded (or transitive) model of $\mathsf{ZF}$ is strictly stronger than $T$ (and all the iterates suggested at the end of the last paragraph, again, by a large margin). This is because the statement "There is an $\omega$model of $\mathsf{ZF}$" is a $\Sigma^1_1$ statement, and therefore absolute between transitive models of $\mathsf{ZF}$. This follows from results by Luzin and Sierpiński on absoluteness of wellfoundedness between transitive models of set theory, and is usually called Mostowski's absoluteness theorem. (The relevant coding required, and Mostowski's theorem are described in both Kanamori's book on large cardinals, and in Recursive Aspects of Descriptive Set Theory by Mansfield and Galen Weitkamp, among other places.) Note how we can proceed to iterate "there is a wellfounded model of" to form stronger theories.
Since given any $M$ model of $\mathsf{ZF}$, the model $L^M$ ($L$ in the sense of $M$) is a model of $\mathsf{ZFC}$, so in the above, whether we use $\mathsf{ZF}$ or $\mathsf{ZFC}$ does not matter.
The theory $S$ is much weaker than the existence of an $\alpha$ such that $V_\alpha$ is a model of $\mathsf{ZF}$. This follows from the Mostowski collapsing theorem: Any countable elementary substructure of $V_\alpha$ collapses to a countable transitive model of $\mathsf{ZF}$, but any such model belongs to $V_\alpha$. Any such $\alpha$ is now called a worldly cardinal.
The remark that working on $\mathsf{ZF}$ or $\mathsf{ZFC}$ does not make a difference still holds here, but we need to be a bit careful in $\mathsf{ZF}$ since we do not have choice, so the possibility of forming elementary substructures is perhaps not immediate. One way of proceeding is to find a $\theta>\alpha$ such that $V_\theta$ satisfies a finite, but strong, fragment of $\mathsf{ZF}$. This model sees that $V_\alpha$ is a model of $\mathsf{ZF}$ and therefore that $L_\alpha=L^{V_{\alpha}}$ is a model of $\mathsf{ZFC}$. But $L_\alpha$ has definable Skolem functions, so we can form elementary substructures of it (provably in $\mathsf{ZF}$), and proceed as described above.
The smallest worldly cardinal is of countable cofinality. The second such cardinal (the existence of which is an assertion strictly stronger than the existence of one) is again of countable cofinality. The next one (whose existence, again, is a stronger assertion) is again of countable cofinality, and on and on for a long while. Much later we finally find a worldly cardinal of cofinality $\omega_1$, but then the next one has again cofinality $\omega$. This should give you an idea of how ridiculously stronger the assertion that there is an inaccessible $\alpha$ is than the theories so far described. See here and here.