課程資訊

Formalization of Deductive Systems

106-1

Phl7714

124EM3000

3.0

In the course Elementary Logic, we have already studied that a deductive system in general consists of three main parts: (i) a suitable formalized language, (ii) an appropriate semantics for the given language, and (iii) a formal system of derivations. The formal language in use consists of two components (i) a class of primitive symbols, known as alphabet, and a finite set of formation rules which tells us how to construct the basic units of linguistic expressions in use, referred to as formulae/sentences (or well-formed formula, wff). The intended semantics for the given language will give interpretations for the expressions of the language so that the truth values of formulae/sentences can be evaluated. Accordingly, the notion of validity and the entailment relations can be defined. While the main concern of a formal system is to reduce reasoning─or at least a sizeable part of mathematical reasoning─to a finite number of rules of inference which should be in principle mechanical.

It is striking that formal logic has flourished since 1879, and by now a great number of important and significant results (in particular, those referred to as meta-theorems, such as the compactness theorem, the soundness theorem and the completeness theorem) have been discovered and proved. In the meantime, several different ways, or styles, of constructing a formal system for a certain subject matter have been proposed. That is to say, based on a given language and the same semantics, a variety of different formal systems can be constructed, each of which is equivalent to the others. And each one has its own advantages and disadvantages. One can find that, though a particular style of formal system may serve admirably for one of the uses which a logical system may be supposed to serve, none can be at all suitable for all of the uses to which logical systems have been put.

The primary concern of this course is firstly to study, in details, formal proofs of these meta-theorems; and secondly, to study the various types of th

The aim of this course is (i) to study, in details, formal proofs of the fundamental meta-theorems for propositional logic and predicate logic; and (ii) to study a variety of types of the formulation of logic systems.

Problem sheets will be distributed each week; the student is expected to spend 6-8 hours per week doing the exercises. Answers will be marked and return in the class. Students are requested to return their answers by 1:oo pm next Tuesday.

Office Hours

Suggested Textbooks

Introductory books including four types

Bostock, D. (1997), Intermediate Logic, Oxford: Clarendon Press.
Scott, D., et. al. (1981), Notes on the Formalization of Logic, Sub-faculty of Philosophy, Oxford University.
Sundholm, G. (2001), ‘Systems of Deduction’ (Chapter 2.1of Handbook of Philosophical Logic, vol. 2, 2nd ed., D. M. Gabbay and F. Guenthner (eds.), Kluwer Academic Publishers, 2001), pp.1-53.

For axiom systems:

Hamilton, A. G. (1988), Logic for Mathematicians, especially chapters 1-4 and sections 1, 2 of Chapter 5, Cambridge: Cambridge University Press.

For systems of natural deduction with the derivations set out linearly:

Lemmon, E. J.(1965), Beginning Logic, Chapman and Hall.

For systems of natural deduction with the derivations set out diagrammatically:

van Dalen, D. (1994), Logic and Structure, 3rd edition, New York: Springer-Verlag.
Tennant, N. W. (1978), Natural Logic, Edinburgh: Edinburgh University Press.

For systems of formal tableaux:

Jeffrey, R. C. (1991), Formal Logic: Its scope and limits, 3rd ed., New York: McGraw-Hill Inc.
Smullyan, R. M. (1995), First-order Logic, first edition 1968, New York: Dover.

For sequent calculi:

There is no particular logic textbook adopting this system; but one can find some version of this type in some introductory books to other branches of formal logic, e.g. G.Takeuti, Proof Theory, (2nd ed., North Holland), 1987, Chapter One.

Syraya Chin-mu Yang, The Formalization of Deductive Systems, Lecture notes in Formal Logic No. 2. The Department of Philosophy, National Taiwan University. Fall Semester 2012.

(僅供參考)

 No. 項目 百分比 說明 1. Class performance 20% 2. Weekly assignment 30% 3. End-of-term exam 50%

 課程進度
 週次 日期 單元主題 第1週 9/15 Part I Formalization of Classical Propositional Logic (CPC) ○. Introduction 1.Formal language suitable for CPC and the classical semantics A formal propositional language ℒK: alphabet; connectives, formation rules Arguments by cases, proof by induction Classical semantics for ℒK: structures vs. Boolean functions, semantic sequents Test the validity of ℒK -sequents and the decidability of ℒK-sequents 第2週 9/22 2.Some properties of semantic entailments, functional completeness, expressive adequacy, DNF/CNF, the interpolation theorem, compactness of ℒK 第3週 9/29 3.The construction of formal systems: A survey Derivations, axioms and rules of inferences, structural rules Two types of the presentation of derivations: derivations set out linearly and derivations set out diagrammatically Syntactic sequents, consistency, theorems Soundness and completeness - general approach to a formal proof of the soundness theorem and the Henkin-style proof of the completeness theorem for a formal system Gödel's incompleteness theorems 第4週 10/06 4.Axiomatic systems for CPC The characteristics of axiom systems An axiom system HPC for CPC The deduction theorem The soundness theorem for HPC The completeness theorem for HPC: Post's proof, Kalmar's proof and Henkin's proof The independence of axioms, some remarks on the nature of axioms 第6週 10/20 6.Formal tableaux systems for CPC Tableaux and formal tableaux systems A tableaux system T for CPC, the soundness theorem and completeness theorem The search of counterexamples in non-closed tableaux Structural rules in tableaux systems A more concise tableaux system Tableaux system with signed formulae A tableau proof of interpolation theorem and DNF theorem. 第6週 10/20 6.Formal tableaux systems for CPC Tableaux and formal tableaux systems A tableaux system T for CPC, the soundness theorem and completeness theorem The search of counterexamples in non-closed tableaux Structural rules in tableaux systems A more concise tableaux system Tableaux system with signed formulae A tableau proof of interpolation theorem and DNF theorem. 第7週 10/27 7.Sequent calculi for CPC Gentzen's sequents and sequent calculi Axiomatization of entailment relations Gentzen's calculi and the construction of derivations A sequent calculus with rules corresponding to tableau rules Local-completeness of rules of inference for connectives in GS Equivalence of sequent calculi and tableau systems 第8週 11/03 Midterm 第9週 11/10 Part II Formalization of Predicate Logic (CQC) 8.First-order language with identity suitable for CQC and the classical semantics Elements of first-order language A naïve first-order language ℒQC suitable for CQC Semantics for ℒQC: Structures for substitutional interpretation of quantification Structures for objectual interpretation of quantification True-in-i-interpretation in a structure and i-equivalence interpretation True-in-M (a structure) and true-in-M+ (an expansion of M) Semantic entailment and validity 第10週 11/17 9.A standard first-order language with identity ℒQ and a Tarskian style of semantics 第11週 11/24 10.Some basic semantic properties of ℒQ Semantic theorems concerning identity The congruence theorem for ℒQ Prenex normal form (PNF) The compactness of ℒQ The decidability/undecidability of first-order languages General properties of formal system for classical predicate logic Counterexamples Skolemization: Skolem functions, Skolemize form and Skolem axioms 第12週 12/01 11.Axiom systems for CQC 第13週 12/08 12.Natural deduction systems for CQC 第14週 12/15 13.Tableaux systems for CQC 第15週 12/22 14.Sequent calculi for CQC, the elimination of Cut Theorem 第16週 12/29 15.Beyond predicate logic: First order theories and Second-order logic Pure logic vs. applied logic First-order theories A formal number theory Many-sorted first-order logic ω-logic and infinitary logic Weak second-order logic 第17週 1/05 16.Free logic and inclusive logic 第18週 1/12 End-of-term exam