function and are actually equivalent. Axiomatic system is very traditional and occurs in the most of textbook. Robbinson put up with resolution method, which continued the work of Herbrand Beth and Smullyan construct a tableaux proof system. It is the simplest proof system and is easy to use Leibniz had a dream to construct a machine to find all theorems. hilbert followed him and for- malized many mathematical branch in his era. But Godel ruined their dream by his famous incompleteness theorem. This course just covers a very small part of provable topics ogic aims to formalize statements and relationship between them. Actually, a programming language can also be taken as a type of formal language. Then they both follow the same approach So this course is another training about programming. It can go further. If you are unlucky, you will learn computability, decidability, and enumerability, which is the theory of computation, the base of computer science 3 Introduction to logic In remaining classes, first order logic will be introduced. First order logic is composed of two parts: propositional logic and predicate logic. Propositional logic is much simpler than predicate logic. However, propositional logic sets up a framework. Predicate logic is more powerful than propositional logic. It can express much more complicated scenarios. But it still follows the same framework. A fact will be proved that propositional logic can be embedded into predicate logic very special form We will learn logic system from two aspects. One is syntax and another one is semantics. The syntax part consists of form of proposition or sentence and the proof system. Proof system defines how you can deduce some consequences from a set of sentences with some rules. There are three typical proof system. Axiom proof system is very classic, which is widely adopted by textbook for mathematical student. Resolution system is a foundation of every logic programming language e.g. prolog. We will use tableaux method. It is more vivid and easier to use. If a sentence is false, you can even construct a counterexample based on you proof procedure The semantics of a proposition or a sentence means whether it is true or false. Herbrand charac terizes a set of sentences in semantic approach. It finally formed into model theory. However you need not worry about the semantics of sentences while using proof system. Actually we hope that every result proved by proof system should be right and a right result should be provable During early study, two sides are split and taught in an twisted way. Is there any connection between them? It is sure. Completeness theorem guarantees that it has a proof if a sentence holds Soundness theorem assure the validity of the result you derived from a proof procedure. Finally a very beautiful result, compactness theorem, will be proved In first order logic it has only two value: true or false. Some logic system may extend to multiple values. Once you master first order logic, it is not difficult for you. Similarly, more complicated logic system are coined for some purpose, including high order logic, modal logic, intuitional logic, ogic is developed to fix the paradox resulted from set theory, which is the foundation of modern mathematics. It tries to formalize statement in order to eliminate ambiguity and to make prooffunction and are actually equivalent. Axiomatic system is very traditional and occurs in the most of textbook. Robbinson put up with resolution method, which continued the work of Herbrand. Beth and Smullyan construct a tableaux proof system. It is the simplest proof system and is easy to use. Leibniz had a dream to construct a machine to find all theorems. Hilbert followed him and for￾malized many mathematical branch in his era. But G¨odel ruined their dream by his famous incompleteness theorem. This course just covers a very small part of provable topics. Logic aims to formalize statements and relationship between them. Actually, a programming language can also be taken as a type of formal language. Then they both follow the same approach. So this course is another training about programming. It can go further. If you are unlucky, you will learn computability, decidability, and enumerability, which is the theory of computation, the base of computer science. 3 Introduction to logic In remaining classes, first order logic will be introduced. First order logic is composed of two parts: propositional logic and predicate logic. Propositional logic is much simpler than predicate logic. However, propositional logic sets up a framework. Predicate logic is more powerful than propositional logic. It can express much more complicated scenarios. But it still follows the same framework. A fact will be proved that propositional logic can be embedded into predicate logic as a very special form. We will learn logic system from two aspects. One is syntax and another one is semantics. The syntax part consists of form of proposition or sentence and the proof system. Proof system defines how you can deduce some consequences from a set of sentences with some rules. There are three typical proof system. Axiom proof system is very classic, which is widely adopted by textbook for mathematical student. Resolution system is a foundation of every logic programming language, e.g. prolog. We will use tableaux method. It is more vivid and easier to use. If a sentence is false, you can even construct a counterexample based on you proof procedure. The semantics of a proposition or a sentence means whether it is true or false. Herbrand charac￾terizes a set of sentences in semantic approach. It finally formed into model theory. However you need not worry about the semantics of sentences while using proof system. Actually we hope that every result proved by proof system should be right and a right result should be provable. During early study, two sides are split and taught in an twisted way. Is there any connection between them? It is sure. Completeness theorem guarantees that it has a proof if a sentence holds. Soundness theorem assure the validity of the result you derived from a proof procedure. Finally a very beautiful result, compactness theorem, will be proved. In first order logic it has only two value: true or false. Some logic system may extend to multiple values. Once you master first order logic, it is not difficult for you. Similarly, more complicated logic system are coined for some purpose, including high order logic, modal logic, intuitional logic, and temporal logic. Logic is developed to fix the paradox resulted from set theory, which is the foundation of modern mathematics. It tries to formalize statement in order to eliminate ambiguity and to make proof 2