Is the theory $TA+\lnot Con(TA)$ consistent? In particular, for every $TA \vdash \phi$, we take as an axiom $\phi$, and $TA \vdash \phi$. We also assert $TA \vdash 0 = 1$. We call this theory $TA + \lnot Con(TA)$. Note that the theory we are talking about does *not* include the statement that $TA$ is true (i.e. $TA \vdash \phi \iff \phi$). The theory can only see what $TA$ implies, and that $TA$ is a theory of first order arithmetic. Is this theory consistent? Note: TA + $\lnot Con(TA)$ is not a theory in the language of arithmetic. We are adjoining a symbol for $TA \vdash$ to the language (as an unary predicate on godel codes). You can also interpret it as a weak set theory. **** **** **EDIT: This is an attempt by someone other than the OP to describe the theory in question in a clearer way; this should not be taken as fully accurate until the OP weighs in.** Let $T_0$ be the theory, in the language of arithmetic together with a new unary predicate symbol $P$, consisting of the following axioms: - Each $\varphi\in $ TA. - Each sentence of the form "$P(n)$" for $n$ the Godel number of a sentence in TA. - $P(\ulcorner 0=1\urcorner)$. This is (I believe) the theory the OP describes. Meanwhile, here are some sentences which are **not** in our theory *(I'm explicitly mentioning them to make it clear that the above really is a complete description of the OP's theory in question)*: - **Internal modus ponens (IMP)**: The sentence $$\forall x, y[P(x)\wedge P(implies(x, y)\implies P(y)].$$ Here "$implies$" is an abbreviation for the usual primitive recursive binary function given by $(\ulcorner p\urcorner, \ulcorner q\urcorner)\mapsto \ulcorner p\implies q\urcorner$. *The point is that we could write this as an axiom scheme, ranging over all actual Godel numbers of appropriate sentences, but we can actually just get it with a single sentence. This isn't a big deal, and if one prefers one can use the scheme version without any impact here.* - **Reflection (R)**: the scheme "$P(\ulcorner \varphi\urcorner)\implies\varphi$" for arithmetic $\varphi$. - **Completeness (C)**: the scheme "$\varphi\implies P(\ulcorner\varphi\urcorner)$" for arithmetic $\varphi$.