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 [word 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 $~$\Sigma^* = \{\neg,\wedge,\vee,=,+,\cdot ,0,a_1,a_2,a_3,…\}^*$~$.

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 $~$n+1$~$-[-tuples] that represent a function from $~$n$~$ 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 $~$A\rightarrow B$~$ and another of the form $~$A$~$ you can deduce $~$B$~$. 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 $~$S$~$ 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 $~$S$~$. 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].