Is the theory $TA+\lnot Con(TA)$ consistient?

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

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

Is the theory $TA+\lnot Con(TA)$ consistient?

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.

• Completeness (C): the scheme "$\varphi\implies P(\ulcorner\varphi\urcorner)$" for arithmetic $\varphi$.

Is the theory $TA+\lnot Con(TA)$ consistient?

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

Is the theory $TA+\lnot Con(TA)$ consistient?

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

Is the theory $TA+\lnot Con(TA)$ consistient?

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.

• Completeness (C): the scheme "$\varphi\implies P(\ulcorner\varphi\urcorner)$" for arithmetic $\varphi$.