Can there be a sentence that is true in every model of an effective theory and yet not provable in that theory?

Formally this is:

$$\exists S [\forall \mathcal M (\mathcal (\mathcal M\models T) \to (\mathcal M \models S)) \wedge \neg (T \vdash S)]$$

In English: there is a sentence in the language of an effectively generated theory $$T$$ that is satisfied in every model of $$T$$, and yet not provable in $$T$$.

Can this occur in some effective logical systems other than first order logic? What are those systems?

[EDIT]In first order logic systems this cannot happen because of Godel's completeness theorem for first order logic, which implies that satisfiability corresponds to syntactical provability, so if a sentence is satisfiable in every model of a first order theory, then it must be a provable in that theory.

• You are perhaps aware, judging by your final paragraph, that this cannot happen in a finitely axiomatizable first-order theory (by Gödel's completeness theorem for the predicate calculus). It would be better to edit that into the body of the Question. – hardmath Apr 30 at 23:00
• Just take first order logic and remove all axioms and rules of inference, so nothing is provable. Then the set of logical validities will work as an example. Or, take the first-order theory of Peano arithmetic, keep the usual inference rules, and throw out every every model except the standard one. Now Con(PA) is true in every model, but not provable. (This is very close to the situation with second-order PA.) . There are also intermediate options, for example use Heyting Arithmetic with the collection of classical models. Now the law of the excluded middle is valid but unprovable. – Carl Mummert Apr 30 at 23:09
• For users to write a more useful answer, it would help if you could add some additional context - what are you thinking about that led you to this question? Given the ease of generating examples, I'm afraid the XY effect (xyproblem.info) may be at play here. – Carl Mummert Apr 30 at 23:18
• In second order logic, take a theory that says you're well-ordered, and that $c_{n+1} < c_n$ for constants $c_n$. It is contradictory, but there is no proof of $\bot$ in it – Max May 1 at 9:05
• @Zuhair - What do you mean by "effective theory"? The empty set, Peano arithmetic, and Heyting arithmetic are all effective theories / effectively generated theories in the usual meaning of the word - they have computable axiomatizations. The important point is that the definition of the logic itself determines both the deductive system and the collection of models - by changing either of those we can make syntactic provability differ from validity in all models. – Carl Mummert May 1 at 11:50