Propositional Logics These are exclusively concerned with the logic of sentential operators such as "and", "or", "not". Such operators are usually, but not always, truth functional. Predicate Logics These usually cover propositional logic and the logic of quantifiers such as "all" and "some". Can be either first order, in which case quantification is permitted only over individuals, or higher order, in which case quantification over predicates or properties is permitted. Foundation Systems These are logical systems whose domain of discourse is rich enough to provide a basis for a substantial part of modern mathematics, e.g. set theory, higher order logic, or other type theories. Modal Logics Modal logics are usually propositional logics with added propositional operators concerning, for example, necessity, time, knowledge, belief, provability...

Type Theories The first type theory was Russell's, since then there have been many others. Logical type theories are higher-order logics in which the domain of discourse is divided by logical type and each quantifier must range over just one of these types. Relevance Logics Relevance logics provide an "implication" operator over propositions which is intended to be closer in meaning to the meaning of "implies" in natural English. In particular, not all propositions are implied by a falsehood. Constructive Logics Constructive logics are logics in which existence proofs are only possible for entities which can be constructed in a suitably concrete manner (e.g. as some kind of canonical term). They are usually intuitionistic. Combinatory Logics Combinatory logics are logics in which "combinators" are used instead of constructs involving bound variables (such as quantifiers).

Non-Monotonic Logics Logics (devised for AI) in which adding premises may diminish the set of derivable conclusions. Logical Frameworks These are logical systems which are intended to provide a framework within which work can be undertaken in a wide range of different logics. The framework may provide a formal metalanguage in which the various logics are defined, or a core logic, of which the various logics are extensions. Programming Logics These are logical systems customised to reasoning about programs in some particular programming language, or general schemes and methods for reasoning about programs (e.g. Hoare Logic). Specification Logics These are the inference systems associated with formal specification languages (such as may be used in the specification of highly secure or safety critical systems).

propositional logics:

Propositional logics are concerned with propositional (or sentential) operators which may be applied to one or more propositions giving new propositions.

Truth Functional Logics A logic is truth functional if the truth value of a compound sentence depends only on the truth values of the constituent atomic sentences, not on their meaning or structure. For such a logic the only important question about propositions is what truth values they may have. Substitution A key feature of the semantics of truth functional logics is that substitution in a compound sentence for a constitutent sentence of a sentence having the same truth value will not change the truth value of the compound sentence.

Intensional Logics A logic which is not truth functional is sometimes be called intensional. Substitution In such a logic the truth value of a compound sentence does not depend solely on the truth values of its constituent sentences and substitution of a sentence with the same truth value need not preserve the truth value of the compound sentence. Modal Logics Among the intensional logics are modal logics, which concern such topics such as necessity and possibility, knowledge and belief, provability and consistency.

Judgement Forms In many cases the things proven in a logic are not just sentences or propositions, but complex judgements formed from the sentences. The reasons for this concern the pragmatics of proof construction. Proof Structure Depending on the intended application of the logic, and connected with the various forms of judgement, different ways of structuring proofs distinguish the varieties of propositional logic.

:

---

© created 1999/10/5 modified 1999/10/5