課程名稱 
演繹邏輯之形式化 Formalization of Deductive Systems 
開課學期 
1061 
授課對象 
文學院 哲學研究所 
授課教師 
楊金穆 
課號 
Phl7714 
課程識別碼 
124EM3000 
班次 

學分 
3.0 
全/半年 
半年 
必/選修 
選修 
上課時間 
星期五7,8,9(14:20~17:20) 
上課地點 
哲研討室二 
備註 
本課程以英語授課。C領域。 總人數上限：15人 


課程簡介影片 

核心能力關聯 
核心能力與課程規劃關聯圖 
課程大綱

為確保您我的權利,請尊重智慧財產權及不得非法影印

課程概述 
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 wellformed 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 metatheorems, 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 metatheorems; 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 metatheorems 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 68 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, Subfaculty 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.153.
For axiom systems:
Hamilton, A. G. (1988), Logic for Mathematicians, especially chapters 14 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: SpringerVerlag.
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: McGrawHill Inc.
Smullyan, R. M. (1995), Firstorder 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 Chinmu 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. 
Endofterm 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 ℒKsequents

第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 Henkinstyle 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 nonclosed 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 nonclosed 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
Localcompleteness 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.Firstorder language with identity suitable for CQC and the classical semantics
Elements of firstorder language
A naïve firstorder language ℒQC suitable for CQC
Semantics for ℒQC:
Structures for substitutional interpretation of quantification
Structures for objectual interpretation of quantification
Trueiniinterpretation in a structure and iequivalence interpretation
TrueinM (a structure) and trueinM+ (an expansion of M)
Semantic entailment and validity

第10週 
11/17 
9.A standard firstorder 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 firstorder 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 Secondorder logic
Pure logic vs. applied logic
Firstorder theories
A formal number theory
Manysorted firstorder logic
ωlogic and infinitary logic
Weak secondorder logic 
第17週 
1/05 
16.Free logic and inclusive logic

第18週 
1/12 
Endofterm exam 
