There are many different systems of symbolic logic. A system of symbolic logic has a number of components: the set of acceptable sentences, called well-formed formulas (or wffs); transformation rules for deriving new formulas from one or more initial formulas; the set of axioms, which is a subset of the set of wffs. The sets of wffs and axioms can be finite or infinite, so long as they are recursive; i.e. so long as there exists a procedure for determining whether any given sentence is a wff or axiom, which could be carried out in a finite number of steps by a device such as a Turing machine (sometimes, it is enough to require that these sets be [recursively enumerable]?).
The theorems of the system are the axioms and all the wffs that can be derived from the axioms by a finite number of applications of the transformation rules. In systems of [natural deduction]? the set of axioms is empty and the transformation rules correspond to patterns of reasoning such as modus ponens whose validity, or truth-preserving nature, is easily recognized.
For a symbolic logic system to be useful it helps to have two additional properties; soundness and completeness?. These properties relate the system of symbolic logic to some underlying model. The property of soundness states that if a theorem can be proven in the symbolic system then it is also true in the model. The property of completeness states that if the theorem is true in a model, then there is some proof for it in the associated symbolic logic. A symbolic logic is said to be determined by a model if it is both sound and complete. Logics of this kind are useful for systems of mechanical theorem proving.
Metalogic is the study of different systems of symbolic logic, and their properties. We can not only prove statements in a logical system; we can also prove statements about logical systems. The most important result along these lines are Gödel's incompleteness theorems which essentially show that every sufficiently powerful logical system does contain sentences which can be neither proved nor refuted from within the system.
There are three main types of logical systems which are used: propositional calculus, predicate calculus, and modal logic.
[Propositional logic]? deals with the logic of individual sentences. The primary system here is the classical system, which is the system most commonly used. Various alternatives to the classical system have been studied, including:
[Predicate logic]? extends propositional calculus to deal with predication and quantification. Again we have a classical system, and various deviations from this system. Most of the different systems of propositional calculus can be extended in this manner to produce systems of predicate calculus. There are two main varieties of systems of predicate calculus: first-order predicate calculus, which allows quantification over objects and is the standard logic used in mathematics (see set theory); and higher-order predicate calculus, which permits in addition quantification over predicates and predication of predicates.
There exist proofs for the soundness and completeness of both predicate and first order logic (see Goedels completeness theorem). Second and higher order logics are not complete however; in other words in all second and higher order logics there are theorems which are true in any model but are not provable within the symbolic system.
The term modal logic has two meanings. In a restricted sense, it means the logic of necessity and possibility. But more broadly, it also includes other logics with a similar structure: deontic logics (which deal with ideas of permission and obligation), temporal logics (which deal with the relationships of past, present and future between events), and doxastic logic (which deals with belief). What all these systems have in common is that they involve the application of unary operators (called modal operators) to statements of either propositional or predicate calculus. It is in this broader sense that the term is used here.
The various systems of modal logic include K, M, S4, S5 and B. The systems differ in having different axioms.
![[Home]](wikipedia.png)