Math 470 Spring 2005 Overview

Mathematical logic is concerned with the basis of reasoning – under what circumstances is it correct to deduce a statement from a set of other statements? It has been considered a branch of philosophy, of mathematics, and of computer science.

Its ingredients include syntax (the definition of correctly formed statements) and semantics (the definition of the conditions under which a statement is considered true) and proof theory (methods to prove that a statement or argument is valid).

During this semester, we have worked with propositional and predicate logic. Their main characteristics are listed below:

	Propositional Logic	Predicate Logic
Syntax
Atomic Formula	Propositional Letter	N-ary Relation symbol applied to n terms. Terms made from variables, constant symbols, function symbols
Formula	Atomic formulas combined with propositional connectives ^, v, Ø, ->, <->	Atomic formulas combined with propositional connectives and quantifiers.
Semantics	Valuation: Assignment of truth values to propositional letters.	Structure: Choice of a set A over which the variables range, elements of A for the constant symbols, functions and relations on A for the function and relation symbols.
Validity	A proposition is valid ( a tautology) if it is true under every valuation; unsatisfiable if it is false under every valuation. This is decidable, for example by construction of truth tables (which is NP-complete).	A formula is valid if it is true in every structure; unsatisfiable if it is true in no structure. In general, this is undecidable. The undecidability can be proved by a diagonal argument related to the unsolvability of the halting problem.
Proof method: Tableau	Tableaux are formed according to rules given in Fig 9, Section 1.4 –page 28 of the text. To determine whether or not a proposition A is valid, construct a Complete Systematic Tableau with root FA. If the tableau is contradictory, A is valid. If not, A is not valid.	Tableaux are formed according to rules given in Fig 29, Section 2.6 –page 110 of the text. To determine whether or not a formula A is valid, construct a Complete Systematic Tableau with root FA. If the tableau is contradictory, A is valid. If not, A is not valid. But note in this case that if the tableau is not contradictory, it may be infinite.
Proof Method: Axiomatic Theory Axioms Rules of Inference Theorems follow from axioms by (repeated ) application of rules of inference.	A set of axiom schemes for propositional logic is given in Section 1.7 (page 47) of the text. The rule of inference is Modus Ponens: From A and A-> B, deduce B.	A set of axiom schemes for predicate logic is given in Section 2.8 (page 127) of the text. The rules of are Modus Ponens and Generalization: From A deduce "x A.
Proof Method: Resolution	The resolution rule for propositional logic: The resolvent of C U {P} and D U {ØP} is C U D. To prove A by resolution, put its negation into conjunctive normal form (a set of clauses regarded as their conjunction, with each clause a disjunction of atomic formulas and their negations) and resolve it to the empty clause.	The resolution rule for predicate logic: The resolvent of C U {Pti} and D U {ØPtj} is C U D if the {Pti) and {Ptj} can be unified. To prove A by resolution, first put its negation into prenex normal form, then skolemize it and remove the universal quantifiers. Put the resulting open formula into conjunctive normal form and resolve it to the empty clause.
Soundness: provable => valid and Completeness: valid => provable	All of the above proof methods can be proved sound and complete. We have done so for the tableau and resolution methods.
Compactness: A set of formulas is satisfiable ó every finite subset is satisfiable.	Since any proof uses only finitely many assumptions, if a set of formulas S leads to a contradiction, that contradiction is derivable from a finite subset of S. This can be used to prove the existence of non-standard models for arithmetic (natural numbers) and analysis (real numbers).