# 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.

-
I suggest looking at the answers to the following related question (in the context of $PA$). mathoverflow.net/questions/65837/… –  Ali Enayat Mar 15 '13 at 4:30
You need to assume sat ZF also for the first claim, since indeed, the nonprovability of any formula at all already implies consistency. For Goedel's proof, what you need for the second claim is the $\omega$-consistency of the theory, a stronger assumption than mere consistency. Rosser's formulation omits the need for this extra assumption. –  Joel David Hamkins Mar 15 '13 at 10:17

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.
One interesting observation: induction is the only reason that nonstandard models can't define a cut (=proper inductive initial segment of the model's natural numbers). As an example of what I mean, starting with a weak theory of arithmetic assuming only $\Sigma^0_n$-induction (so, $P^-+I\Sigma_n$), it is consistent that there is a $\Sigma^0_{n+1}$-definable cut. One thing I don't know: are there models of $P^-+I\Sigma_n$ in which the true natural numbers form a $\Sigma^0_{n+1}$-definable cut? –  Noah Schweber Mar 10 '14 at 3:43