Logical systems (a.k.a. formal systems) are mathematical abstractions that aim to capture the notion of reasoning to reach valid conclusions from certain premises.
A logical system can be thought of as a procedure which divides a language in badly-formed and well-formed sentences, and further splits this last group into theorems and not theorems.
Logical systems are made from a series of elements: a language, a syntax, axioms and rules of inference.
A language consists of the words that can be formed from a set of symbols. Typically, we will want our language to be enumerable and computable. For example, a possible language for arithmetic is .
A syntax is the collection of rules which determine whether a word of our language is a well-formed formula.
The axioms are distinguished formulas of the language that are taken to true a priori. A logical system is axiomatizable if its set of axioms is computable.
The rules of inference are -tuples that represent a function from formulas (premises) to a new formula (conclusion). For example, we have modus ponens as a rule of inference, which says that from a formula of the form and another of the form you can deduce . Almost always we will want our rules of inference to be computable. Axioms can be thought of as rules of inference for which no premise is necessary.
Axioms and rules of inference are used to construct proofs. A proof of a sentence of the language is a finite sequence of sentences, such that every sentence is either an axiom or can be deduced from the previous sentences using a rule of inference, and the last sentence in the sequence is . Sentences which have a proof are called theorems of the system.
Note that logical systems are purely syntactical entities - they talk for themselves about nothing. Logical systems are given meaning through semantics.
Logical systems can relate to one another through translations.