# Formal System and Formal Logical System

I was reading the Wikipedia article for Mathematical_logic. When reaching Formal_logical_systems, I was curious about its definition and clicked into its own article Logical_system, which redirected me to the article for Formal_system, where I found the definition for formal system:

In formal logic, a formal system (also called a logical calculus[citation needed]) consists of a formal language and a set of inference rules, used to derive (to conclude) an expression from one or more other premises that are antecedently supposed (axioms) or derived (theorems). The axioms and rules may be called a deductive apparatus. A formal system may be formulated and studied for its intrinsic properties, or it may be intended as a description (i.e. a model) of external phenomena.

A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to sentences of the formal language, that is, formulae that contain no free variables. A logic is sound if all sentences that can be derived are true in the interpretation, and complete if, conversely, all true sentences can be derived.

I thought logical system and formal system were the same concept by self-learning, but here it says logical system is a formal system plus semantics/interpretation. Isn't that in logical system we don't care about the semantics/meaning of propositions and that's the reason that the subject is called formal logic? But why here it says logical system has semantics/interpretation? How to understand "semantics" and whether logical system and formal system are the same?

Is logical system a special example of formal system, in the same sense as Lambda calculus is a special example of formal system as in examples of formal systems? Or is logical system a formal system with additional structure called "semantics", in the same sense as topological vector space is a vector space with additional topological structure?

Thanks and regards!

To answer your other questions, consider the simplest, most accessible case: propositional logic. We have atomic propositions, represented by simple symbols like P and Q, and then formulas built up from the usual connectives like and ($\wedge$), or ($\vee$), and not ($\neg$). Together with the proof theory which governs how we do deductions, we now have a formal system by your definition.
The semantics is built by introducing a separate meta-level, totally outside everything in the previous paragraph. In that level we define two truth values, true and false. In this level we also define a function which maps each propositional symbol to a truth value. Let's call this function I. Here's one possible version of I: {(P,true),(Q,false)}. I is the interpretation function. Finally, we define the usual semantics of the connectives: for example, and ($\wedge$) means both its arguments must be true.