The prooffor(x,y) predicate in godel's 1st incompleteness theorem is primitive recursive, so if there is a statement ' S ' within the theory , which would be 1st order PA in godel's case , and it has a proof ' P ' then the statement prooffor(P,S) is also provable within the theory.
This also means that prov(S) is also provable, where prov(x) is the provability predicate, since the predicate uses prooffor(x,y) as the only property in its definition.
So, can there be a theory , godelian , which admits both standard and non-standard model , where even though a proof exists for a statement " S' "( provably so ) but the statement prov(S') is not provable ? Regardless of whether the theory admits standard or non standard model.....
If so then it should be a contradiction right ? Because the predicate prooffor(x,y) is definitely provable for S' but still prov(S') is not ... this would show the theory is actually inconsistent ( not even non standardly consistent ) i.e. a flaw in the logical language expressing the theory itself...