Suppose we have a consistent axiomatizable theory $T$ extending the theory of $A_E$ where $A_E$ are these axioms (slide 5 here). Can we find some sentence $\varphi$ such that $T$ proves that it doesn't prove $\varphi$? So if we had a predicate $Proves(\sigma)$ it would be true iff $T \vdash \sigma$ and we'd represent this problem by showing there's some sentence $\varphi$ such that $T \vdash \neg Proves( \varphi)$.
I'm thinking that the negation of a tautology could work since propositional logic and hence $T$ proves that a contradictory sentence evaluates to false and thus there is no proof of it. Is this on the right track? Is there some more formal method of proof?
It turns out, perhaps surprisingly, that the answer to your question is no!
Note that - for an appropriate theory $T$ - if $T$ proves "$T$ doesn't prove $\varphi$" for some sentence $\varphi$, then $T$ proves "$T$ is consistent" (since $T$ proves that inconsistent theories prove everything). So by Godel's theorem, $T$ is inconsistent.
How do we reconcile this with the fact that there are statements $T$ clearly knows are false? Well, the point is that $T$ - in order to be consistent - can't "trust itself" too much. While $T$ proves (say) $\neg(0=1)$, and $T$ proves "$T$ proves $\neg(0=1)$," $T$ does not prove "$T$ doesn't prove $0=1$." As far as $T$ knows, $T$ might be inconsistent.
Statements of the form "Provable things are true" are called soundness principles. Soundness principles are related to consistency principles, but soundness is much stronger than mere consistency (e.g. PA+$\neg$Con(PA) is consistent but not sound). In fact, Lob's theorem shows that in a precise sense a reasonable theory $T$ won't prove any nontrivial amount of soundness about itself.
It's worth noting that these foundational theorems (Lob and Godel) have some subtle limitations, including:
Depending how we talk about provability, Lob's theorem can break down.
When we pass from axiomatizable theories to definable theories, Godel's theorem can break down. For example, there is a formula $\varphi$ defining a theory such that (1) PA proves that the theory defined by $\varphi$ is consistent but (2) the theory defined by $\varphi$ is in fact PA itself (the resolution of this apparent paradox being of course that PA can't prove point (2)); see here for details.