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.