Hello.

Let $\operatorname{sat} X$ denote the satisfiability of a theory $X$.

From Gödel's second incompleteness theorem and his completeness theorem follows $$ZF \not\vdash \lceil \operatorname{sat} ZF \rceil$$ Assuming $\operatorname{sat} ZF$ in the metatheory, we can also say that $$ZF \not\vdash \lnot \lceil \operatorname{sat} ZF \rceil$$ that is, $\operatorname{sat} ZF$ is independent of $ZF$.

Most texts I have read about large cardinals assume the consistency of $ZF$ (and stronger systems created on top of $ZF$). I was wondering whether there is any research done about the system $ZF\cup \{ \lnot \lceil \operatorname{sat} ZF \rceil \}$, let us call it $ZF\bot$ in the following. Trivially $$ \operatorname{sat} ZF \Leftrightarrow \operatorname{sat} ZF\bot $$

I guess that a model $\mathbb{ZF}$ of $ZF\bot$ has another concept of "finite" sets, so i **guess**
$$ \not\exists_{P(x)\in \operatorname{For}} \forall_{X\in \mathbb{ZF}} . P^{\mathbb{ZF}}(X) \Leftrightarrow |X|<\omega$$
because $\mathbb{ZF}$ must consider some infinite proof trees of $ZF\vdash\bot$ finite - but I have no formal argument for this. This paper seems to be somewhat related, as it deals with the length of inconsistency proofs.

However, except for this, I have not found anything related, but it would be interesting to know.