What follows from assuming not Con(ZF)? 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.
 A: A model of ZF$\perp$ must contain non-standard natural numbers (for instance, the Gödel number of the proof of a contradiction in ZF) and this implies that it cannot be well-founded (starting from a non-standard number, you can define a $\in$-decreasing sequence). Hence, if we are assuming the foundation axiom as a part of ZF, your model $\mathbb Z\mathbb F$ must be a pair $(M,R)$, where the relation $R\subset M\times M$ cannot be the true membership relation, since this is well-founded.
Hence, I assume that when you write $|X|$, you are talking in fact about the cardinality of the extension of $X$, i.e. $|\{x\in M\mid x\,R\,X\}|$. The true cardinality of $X$ as a set would have no direct relation with the model.
In this setting, such a formula $P(X)$ cannot exist. If so, you could define in $(M,R)$ the set $S=\{n\in\omega\mid P(n)\}$, which would be the set of all standard natural numbers. This would be an inductive set ($0\in S\land \forall n\in \omega (n\in S\rightarrow n+1\in S))$, but $S\neq \omega$. Hence the induction principle would fail in the model.
