we know from Godel that not all true sentences can be shown true in propositional logic. — Leontiskos
That is not what Godel said nor what we take from Godel.
To show a sentence is to prove the sentence from a set of axioms and rules of inference.
But if a sentence is contingent, then to show that the sentence is true requires specifying which model or models 'true' pertains to.
Propositional logic:
We have the soundness and completeness theorem:
G |- P if and only if G |= P.
That is, a set of formulas G proves a formula P if and only if every model in which all the formulas of G are true is a model in which P is true.
Soundness (if G |- P then G |= P). Proof is straightforward by induction on length of derivation. I don't know who first proved it.
Completeness (if G |= P then G |- P). It seems this was first proved by Post in 1921.
So:
If a sentence is contingent, then the sentence is not provable by logical axioms alone. (Soundness) Moreover, there is a mechanical method to demonstrate that the sentence is not provable by logical axioms alone (that is, there is mechanical method to adduce a model in which the sentence is false).
If a sentence is contingent, then the negation of the sentence is not provable by logical axioms alone. (Soundness) Moreover, there is a mechanical method to demonstrate that the negation of the sentence is not provable by logical axioms alone (that is, there is mechanical method to adduce a model in which the sentence is true).
If a sentence is logically true, then the sentence is provable by logical axioms alone. (Completeness) Moreover, there is a mechanical method to adduce such a proof.
If a sentence is logically false, then the negation of the sentence is provable by logical axioms alone. (Completeness) Moreover, there is a mechanical method to adduce such a proof.
Also, if a sentence is true in a given model, then it can be demonstrated that it is true in that model. Moreover, there is a mechanical method to demonstrate that it is true in that model.
Also, if a sentence is false in a given model, then it can be demonstrated that it is false in that model. Moreover, there is a mechanical method to demonstrate that it is false in that model.
Predicate logic:
We have the soundness and completeness theorem:
G |- P if and only if G |= P.
That is, a set of formulas G proves a formula P if and only if every model in which all the formulas of G are true is a model in which P is true.
Soundness (if G |- P then G |= P). Proof is straightforward by induction on length of derivation. I don't know who first proved it.
Completeness (if G |= P then G |- P). This was first proved by Godel in 1930, but Henkin's very different proof in 1949 is the one usually referred to.
So:
If a sentence is contingent, then the sentence is not provable by logical axioms alone. (Soundness) But there is no mechanical method to demonstrate that the sentence is not provable by logical axioms alone (that is, there is no mechanical method to adduce a model in which the sentence is false) (follows from Church 1936, corollary of incompleteness theorem).
If a sentence is contingent, then the negation of the sentence is not provable by logical axioms alone. (Soundness) But there is no mechanical method to demonstrate that the negation of the sentence is not provable by logical axioms alone (that is, there is no mechanical method to adduce a model in which the sentence is true) (follows from Church 1936, corollary of incompleteness theorem).
If a sentence is logically true, then the sentence is provable by logical axioms alone. (Completeness) But there is no mechanical method to adduce such a proof (follows from Church 1936, corollary of incompleteness theorem).
If a sentence is logically false, then the negation of the sentence is provable by logical axioms alone. (Completeness) But there is no mechanical method to adduce such a proof (follows from Church 1936, corollary of incompleteness theorem).
Incompleteness (Godel-Rosser in modern form):
If (1) T a formal theory (has a recursive axiomatization and recursive inference rules), and (2) T is consistent, and (3), e.g., Robinson arithmetic is interpretable in T, then T is incomplete (that is, there is a sentence P in the language for T such that neither P nor ~P are theorems of T).
"[...] not all true sentences can be shown true in propositional logic."
The best I can make that a definite thought as to formal logic: If a sentence is contingent, then it is not provable in propositional logic from logical axioms alone. That is true, but it is merely the soundness theorem for propositional logic, and I see no reason to think it is something that comes from Godel.