Can we effectively axiomatize a theory that proves the negation of its own Gödel's sentence?

Question

For any consistent and effective theory $T$ fulfilling Gödel's criteria, let $G_T$ be the Gödel sentence of $T$, that is: $$ G_T \iff \neg \exists x: \operatorname{Proof}_T(x,\ulcorner G_T \urcorner)$$ So, we have $T \not \vdash G_T$, which would make adding $\neg G_T$ to it consistent, but this would be another theory.

Is there an example of some effective [all it's theorems are recursively enumerable + represents all computable functions], consistent first order theory $T$ such that: $T \vdash \neg G_T$.

Of course $T$ would be unsound, since it's proving a false arithmetical statement; and it would be also incomplete by Gödel–Rosser proof. But, how can one effectively define such a theory?

Answer 1

$\newcommand{\Con}{\operatorname{Con}}$In fact, there is no issue here - already the "naive" approach does the job, and the subtlety you are worried about is irrelevant.

The Godel sentence $G_T$ for a ("reasonable") theory $T$ is $T$-provably-equivalent to $\Con(T)$. In particular, for any stronger theory $S$ we will have both $S\vdash \Con(S)\rightarrow \Con(T)$ and $S\vdash \neg G_T\leftrightarrow\neg \Con(T)$ as well as $S\vdash G_S\leftrightarrow \Con(S)$.

In particular, letting $S=T+\neg G_T$ we get $S\vdash \neg G_S$: this is because $S\vdash \neg \Con(T)$, so $S\vdash \neg \Con(S)$, so $S\vdash \neg G_S$ since $\Con(S)$ and $G_S$ are $S$-provably equivalent.

Answer 2

The answer is yes. Let $T$ be the theory PA + $\neg$Con(PA). So this theory proves $\neg$Con(PA) and hence also $\neg$Con(T). But as Noah mentions, Con(T) is provably equivalent in T to the Godel sentence for T, and so T proves the negation of its own Godel sentence.