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 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 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 Order Logic for application adopts a special set of its own notations. For convenience to read text book we just follow the terminology in text book. Then, we need change the definition of partial order, which are slightly different with the one learned in last semester. And tree is also a very important tool to our class. And it is totally represented in an order approach, as a partial order In Logic for application, partial order is defined as following Definition 1(Partial order). A partial order is a set S with a binary relation on S, which is transitive and irreflexive You should mind that partial order is irreflexive other than reflexive defined in previous semester and the most of text book on set theory Whatever the change of partial order, linear order is always the same Definition 2(Linear order). A partial order is a linear order, if it satisfies the trichotomy law <y or t=y or y <a As we know, there are many partially ordered sets. For further investigation, we can divide them into two categories, something bad and something good. Here, we define what is good as following Definition 3(Well ordering). A linear order is well ordered if every nonempty set A of s has a least element The set N is a reference of countable set. countable is defined base on set of natural number Definition 4( Countable). A set A is countable if there is a one-to-one mapping from A to M As a rational number can be represent as a pair of two natural number. Q is a set of countable elements, which also contains natural number as a very small part of it Specially, when we can count a set clearly, here we mean a exact number, we define the followin conceptfunction 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 Order Logic for application adopts a special set of its own notations. For convenience to read text book, we just follow the terminology in text book. Then, we need change the definition of partial order, which are slightly different with the one learned in last semester. And tree is also a very important tool to our class. And it is totally represented in an order approach, as a partial order. In Logic for application, partial order is defined as following: Definition 1 (Partial order). A partial order is a set S with a binary relation < on S, which is transitive and irreflexive. You should mind that partial order is irreflexive other than reflexive defined in previous semester and the most of text book on set theory. Whatever the change of partial order, linear order is always the same. Definition 2 (Linear order). A partial order < is a linear order, if it satisfies the trichotomy law: x < y or x = y or y < x. As we know, there are many partially ordered sets. For further investigation, we can divide them into two categories, something bad and something good. Here, we define what is good as following. Definition 3 (Well ordering). A linear order is well ordered if every nonempty set A of S has a least element. The set N is a reference of countable set. countable is defined base on set of natural number. Definition 4 (Countable). A set A is countable if there is a one-to-one mapping from A to N . As a rational number can be represent as a pair of two natural number. Q is a set of countable elements, which also contains natural number as a very small part of it. Specially, when we can count a set clearly, here we mean a exact number, we define the following concept. 2