課程概述 
This course is in essence an intermediatelevel course for formal logic. I shall hence assume that the student has a nodding acquaintance with topics in Elementary Logic. Some basic knowledge of Elementary Set Theory is extremely helpful though not essential. I shall confine this course to the four main styles of formal systems for propositional logic (i.e.CPC) and predicate logic(i.e., CQC):
(a) HilbertFrege style (axiom) systems,
(b) Systems of natural deduction,
(c) (Formal) tableaux systems, and
(d) Sequent calculi.
The syllabus is to be described as below:
The construction of a formal language suitable for propositional logic, and the standard semantics Application of arguments by cases, and proofs by induction
Formal proofs of general properties of semantic entailments, and some important results in propositional logic, including functional completeness, expressive adequacy, disjunctive normal form (DNF) and conjunctive normal form (CNF), the interpolation theorem, compactness, and decidability
The construction of formal systems
Formal proofs of the soundness theorem and completeness theorem for propositional logic.
The construction of axiomatic systems, systems of natural deduction, formal tableaux systems, and sequent calculi for propositional logic
The construction of a firstorder language suitable for predicate logic and the standard semantics
Substitutional interpretation of quantification and objectual interpretation of quantification: trueiniinterpretation in a structure and iequivalence interpretation; trueinM (a structure) and trueinM+ (an expansion of M); a Tarskian style semantics
The congruence theorem, prenex normal form (PNF) and compactness of firstorder language, Skolemization: Skolem functions, Skolemized form and Skolem axioms
The construction of axiomatic systems for predicate logic, the independence of axioms and the nature of axioms.
The construction of systems of natural deduction for predicate logic, and normalization of natural deduction
The construction of systems of formal tableaux for predicate logic.
The construction of sequent calculi for predicate logic and its normalization
Formal proofs of the soundness and completeness theorem for predicate logic, the decidability/ undecidability of firstorder languages
The equivalence of systems of distinct styles
