 In the early 1940s the recognition of the semantical nature of the notion of logical truth led Rudolf Carnap to an informal explication of this notion in terms of Leibnizian possible worlds. At the same time, he recognized that the many syntactical advances in modal logic from 1918 on were still not accompanied by adequate semantic considerations. One notable exception was Gödel’s interpretation of necessity as provability and the resulting preference for S4. Carnap instead thought of necessity as logical truth or analyticity. Considerations on the properties of logically true sentences led him to think of S5 as the right system to formalize this ‘informal’ notion. Carnap’s work in the early forties would then be focused on (1) defining a formal semantic notion of L-truth apt to represent the informal semantic notions of logical truth, necessity, and analyticity, that is, truth in virtue of meaning alone (initially, he drew no distinction between these notions, but clearly thought of analyticity as the leading idea); and (2) providing a formal semantics for quantified S5 in terms of the formal notion of L-truth with the aim of obtaining soundness and completeness results, that is, prove that all the theorems of quantified S5 are L-true, and that all the L-truths (expressible in the language of the system) are theorems of the system.