复旦大学：《离散数学 Discrete Mathematics》英文讲稿_08 Syntax and semantics Soundness theorem Completeness theorem

Discrete mathematics Yi li Software sc Fudan unive April 18, 2012

Discrete Mathematics Yi Li Software School Fudan University April 18, 2012 Yi Li (Fudan University) Discrete Mathematics April 18, 2012 1 / 17

Review Atomic tableaux o CsT and properties

Review Atomic tableaux CST and properties Yi Li (Fudan University) Discrete Mathematics April 18, 2012 2 / 17

utline Syntax and semantics Soundness theorem o Completeness theorem

Outline Syntax and semantics Soundness theorem Completeness theorem Yi Li (Fudan University) Discrete Mathematics April 18, 2012 3 / 17

Syntax Semantics Example Give you two Chinese characters"更衣”, what's it mean? o It means change clothes in modern Chinese o It means go to washroom in ancient chinese Example Give an acronym "P", what's it mean? o Internet protocol in networl o Integer Programming in operation research o Interactive proof in complexity

Syntax & Semantics Example Give you two Chinese characters ”➁➓”, what’s it mean? It means change clothes in modern Chinese. It means go to washroom in ancient Chinese. Example Give an acronym ”IP”, what’s it mean? Internet Protocol in network. Integer Programming in operation research. Interactive proof in complexity. Yi Li (Fudan University) Discrete Mathematics April 18, 2012 4 / 17

Syntax Semantics am dle Give you the following programming segments O in C, printf("Hello World! ") O in Java, system. print("Hello World! " o in C++, cout<< Hello World! All of them just output"hello World! " on the screen

Syntax & Semantics Example Give you the following programming segments: 1 in C, printf(”Hello World!”); 2 in Java, system.print(”Hello World!”); 3 in C++, cout<<”Hello World!”; All of them just output ”Hello World!” on the screen. Yi Li (Fudan University) Discrete Mathematics April 18, 2012 5 / 17

Syntax Semantics in PL What's syntax o What's semantic? o What's relationship between them?

Syntax & Semantics in PL What’s syntax? What’s semantic? What’s relationship between them? Yi Li (Fudan University) Discrete Mathematics April 18, 2012 6 / 17

Soundness dle Consider pierce law (A→B)→A)→A. Give its tableau proof o Give its truth table

Soundness Example Consider Pierce Law ((A → B) → A) → A. Give its tableau proof. Give its truth table. Yi Li (Fudan University) Discrete Mathematics April 18, 2012 7 / 17

Sign Noncontradictory Path am dle Given proposition((A→B)→(A→C)→(B→C) there is a truth valuation which make it false Consider the tableau with the root as F(A→B)→(A→C)→(B→C)

Sign & Noncontradictory Path Example Given proposition ((A → B) → (A → C)) → (B → C), there is a truth valuation which make it false. Consider the tableau with the root as F ((A → B) → (A → C)) → (B → C) Yi Li (Fudan University) Discrete Mathematics April 18, 2012 8 / 17

Soundness emma If v is a valuation that agrees with the root entry of a given tableau T given as UTn, then t has a path P every entry of which agrees with V

Soundness Lemma If V is a valuation that agrees with the root entry of a given tableau τ given as ∪τn, then τ has a path P every entry of which agrees with V . Yi Li (Fudan University) Discrete Mathematics April 18, 2012 9 / 17

Soundness( Cont. Theorem(Soundness) If a is tableau provable, then a is valid, i.e. F a=ha

Soundness(Cont.) Theorem (Soundness) If α is tableau provable, then α is valid, i.e. ` α ⇒ α. Yi Li (Fudan University) Discrete Mathematics April 18, 2012 10 / 17