A consistent theory can believe it has a proof of contradiction

Deduction theorem for sentence assumptions: In ZF, for a sentence theory $T$, a sentence $\sigma$ and any formula $\theta$,

$T\cup \{\sigma \}⊢\theta ⟺T⊢\sigma \to \theta \mathrm{.}$

The forward transformation also works for an open discharged assumption $\sigma$ provided every variable generalized or existentially eliminated in the given derivation is absent from $\mathrm{FV}(\sigma )$; the other assumptions remain sentences.

Second incompleteness for standard provability: If T is consistent and has the arithmetic/interpretation and D1–D3 hypotheses above for the displayed standard predicate, T does not prove its displayed $\mathrm{Con}(T)$. Numeralwise correctness of an arbitrary predicate is insufficient.

Models and consistency for countable theories: In external ZF, an explicitly countable sentence theory is consistent iff it has a nonempty set model, and iff it has a model with carrier injecting into $\omega$. For an effective presentation, external consistency agrees with the truth of its certified Con formula in standard arithmetic. No transitivity or external well-foundedness of a model follows.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.