|
課程名稱 |
演繹邏輯之形式化
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 |
|
|
指定閱讀 |
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. |
|
參考書目 |
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.
|
|
評量方式
(僅供參考) |
|
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 |
|