# Overview:

 an introduction to symbolic logic
 Introduction Logic is for constructing proofs, which give us reliable confirmation of the truth of the proven proposition. Formal Languages A language is formal if the syntax of the language is defined with sufficient precision that a computer could be programmed to check whether any particular sentence belongs to the language.
 Formal Logics An inference rule is a method of deriving conclusions from premises. When inference rules for a formal language are codified it becomes a formal logic. Varieties of Logic There are many different kinds of logical system within which proofs can be conducted.
 Philosophy of Logic A bit of philosophy might help us understand logic. Or it might not. Glossary Brief explanations of some of the words which have special significance in logic.

# Introduction:

 Logic is for constructing proofs which give us reliable confirmation of the truth of the proven proposition.

 reason Logic is the study of reason, that is, of rational ways of drawing or establishing conclusions. deductive reasoning "Deductive" and "demonstrative" are adjectives which describe those kinds of reasoning which are most reliable. If a logic is deductive then it must be sound, i.e. its rules must not not allow a falsehood to be derived from true premises. For this to work reliably you really need a formal language with formally defined logical axioms and inference rules.
 formal deduction Reasoning is formal and deductive if: The propositions derived are expressed in a formal language. The allowable steps of inference are codified formally so that well formedness of proofs is, at worst, semi-decidable (preferably, and usually, decidable). The permitted inferences are sound.
 non-deductive reasoning A method of reasoning is non-deductive if, even when correctly followed, it may permit the derivation of a conclusion which is false from premises which are all true, or if the inference rules are not sufficiently definite to settle questions about what can correctly be inferred. The most widely studied form of non-deductive reasoning is probably inductive reasoning, which has been supposed by many to justify inference to general scientific laws from particular experimental observations. Induction is neither sound nor definite.

# Formal Languages:

 A language is formal if the syntax of the language is defined with sufficient precision that a computer could be programmed to check whether any particular sentence belongs to the language.

 Diversity There are many different kinds of formal notation. Any of these may become part of a formal logic, though few do. A full understanding of the scope of logic depends upon understanding how arbitrary formal notations can be integrated into a logical system.
 Design The key aspect of a language which determines whether it can be made into a logic is the definition of the language, which is the primary output from the process of designing a language. A well-defined semantics is most highly desirable in a language intended for use as or with a logic.
 Application A language which has been formally defined is a candidate for use in or support by computer applications. If you can describe a problem in a formally defined language then you may find a computer program which will be able to solve the problem for you. Languages are so important to computer applications that in many application domains the development of new languages is prerequisite to the delivery of new kinds of functionality.

# Formal Logics:

 An inference rule is a method of deriving conclusions from premises. When inference rules for a formal language are codified it becomes a formal logic.

 sentences For a language to become a logic it must be capable of expressing propositions, for which purpose there must be an appropriate syntactic category, e.g. sentences, or formulae. Examples of languages which fail to be suitable for logics for lack of such a category are the lambda calculus and most programming languages, which are designed for defining algorithms or functions, not for making or proving assertions. In the case of a typed language a distinguished type may suffice, a type of propositions or truth values, e.g. BOOL in HOL. This technique was used by Alonzo Church to make a logic (his simple theory of types) from the typed lambda calculus.
 axioms To define the logic it is next necessary to determine the axioms of the logic. The axioms are those sentences which are to be considered true without proof. inference rules Next the inference rules must be defined. Inference rules determine how new theorems can be derived from one or more previously proven theorems. effectiveness It is normal that the definitions of the axioms and inference rules be effective in the sense that a computer could be used to check what is an axiom or to check the correctness of an application of an inference rule. consistency The logic is consistent (in the sense of Emil Post) if there are some sentences of the language which are not provable from the axioms using the inference rules.
 truth If the language has a semantics this will usually determine a subset of the sentences of the language which are "true", these are the sentences which should be provable in the logic. soundness If all the sentences which can be proven using the logic are true then the logic is sound. completeness If all the true sentences are provable then the logic is complete.

# Varieties of Logic:

 There are many different kinds of logical system within which proofs can be conducted.

 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.

# Philosophy of Logic:

 A bit of philosophy might help us understand logic. Or it might not.

 Topic Neutrality It is traditional to take the view that logic is topic neutral. To the extent that necessary truths, being true in all possible worlds, can say nothing which is particular to any one of those possible worlds, a necessary truth can be considered to have no subject matter in the real world. However, some propositions widely accepted as necessary are most naturally supposed as having a subject matter. For example, the truths of arithmetic may be considered necessary propositions whose subject matter is the collection of abstract entities known as the natural numbers. Even if the logicist thesis that mathematics is logic is put aside, the claim of topic neutrality seems to me difficult to justify. Classical propositional logic is the theory of boolean operators, they are its subject matter. There are many non-classical variants of propositional logic most of which have some purpose and rationale. For these alternatives to have any validity we must surely accept that they differ in subject matter. Neither intuitionistic nor many-valued logics are about boolean operators, even though they may use exactly the same symbols as classical logic.
 True in Virtue of their Form Symbolic logic is normally presented as codified in formal logical systems. Such codifications are called formal because they define formal criteria for theoremhood which remove the necessity for any understanding of the meaning of the sentences or terms involved in the demonstration of a theorem, making use exclusively of criteria which relate to the form of the sentences rather than their content. For a classic statement of the importance of this view of logic, together with an indication of some of the problems which it causes, see: Bertrand Russell on the definition of Logic. See also: Alfred Ayer on the analyticity of mathematics. An alternative approach is to regard particular formal logical systems as incomplete formalisations of the body of analytic truths, which cannot be completely formalised. Any analytic statement will be a theorem of some logical system (if only by devising a system of which it is an axiom), but it is theoremhood in a formal system which is formal, the ultimate characteristic of necessary or logical truths is semantic rather than formal. If the truths of arithmetic are allowed to be necessary, then it follows (after Gödel) that no sound formal system capable of expressing sufficiently many of the facts of arithmetic will be complete. For any formal (semi-decidable) set of true sentences of arithmetic there will then be some statements of arithmetic which are true and not members of the set. To regard logic as formal is therefore at the expense of denying that the truths of arithmetic are logically necessary (with which many are content), and depends upon some arbitrary choice of formal system.

# Glossary:

 Brief explanations of some of the words which have special significance in logic.