課程資訊
課程名稱
演繹邏輯之形式化
Formalization of Deductive Systems 
開課學期
106-1 
授課對象
文學院  哲學研究所  
授課教師
楊金穆 
課號
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 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