# Introduction:

 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 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.

# Truth Functional:

 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.

 Classical or Boolean In a classical, boolean or two-valued logic every proposition is either true or false and no other feature of the proposition is relevant.
 Three Valued Logics In these the possibility that a proposition is neither true nor false is admitted. An extra "truth value" (perhaps called undefined) is admitted for propositions such as "the king of France is bald" where neither the proposition nor its negation is true.
 Many-Valued Logics Truth functional logics in which there are more than three truth values are also possible.

# Intensional:

 A logic which is not truth functional is sometimes called intensional.

 modal logics Modal logics are concerned with a variety of non truth functional operators over sentences. These concern necessity and possibility, knowledge and belief, temporal concepts, and many others. Modal logics can generally be treated semantically using possible worlds and the details of the semantics is then determined by an accessibility relationship between the worlds (which in temporal logic corresponds to the order structure of time).
 intuitionistic logics Intuitionists are unhappy about proof by contradiction in its full generality, particularly because of its possible use in set theory for demonstrating the existence of entities satsifying some property without the need to exhibit any particular individual satisfying the property. Intuitionistic logics limit the power of proof by contradiction.
 relevance logics These logics have been devised by philosophers dissatisfied with material implication. Seeking a form of implication which is closer to the use of "implies" in ordinary language they have sought logics in which, for example, not all propositions are implied by a falsehood. non-monotonic logics Non-monotonic logics originated in work on Artificial Intelligence. In a non-monotonic logic it is sometimes possible to derive fewer conclusions when additional premises are made available.

# Judgement Forms:

 For a variety of reasons formal logics usually involve an extra layer of structure above the propositions or sentences which are its subject matter. At this level a sentence may be asserted, or a more complex judgement involving several sentences may be expressed and proven.

 Frege's Judgements Judgements of the kind we are considering here were first introduced by Frege in his Begriffsscrift. In ordinary language writing or uttering a sentence is normally understood as asserting it, and special measures are necessary to mention a sentence without asserting it (e.g. enclosing it in quotation marks), Frege chose to reverse the defaults for his formal notation, using the symbol "" to be used in front of an expression to make an asserted judgement. (in Frege this is the combination of "|", asserting and "-" forming a judgement but the pair have since been treated as a single symbol)
 Hilbert's Metanotation Hilbert introduced the field of metamathematics, in which mathematical methods were applied to the study of formal mathematical notations. This involved the use of two languages, an object language being studied, and a meta-language in which claims about the object language are expressed. "" was then pressed into service as metanotation. " p" asserts the provability of p in the object logic, "p q" asserts (in the metalanguage) that q is derivable from p in the object logic.
 Judgements in Object Language Possibly because of their convenience as a means for controlling the structure of proofs, judgement forms are now part of the object language in most formal logical systems. The forms of judgement chosen are important in the pragmatics of describing and constructing formal proofs in the object logic, or may influence the ease with which the metatheory can be developed.

# 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.