FiniteModelTheoryLecture10

1、1Finite Model TheoryLecture 10Second Order Logic2OutlineChapter 7 in the textbook: SO, MSO, 9 SO, 9 MSO Games for SO Reachability Buchis theorem3Second Order Logic Add second order quantifiers:9 X.f or 8 X.f All 2nd order quantifiers can be done before the 1st order quantifiers why ? Hence: Q1 X1. Q

2、m Xm. Q1 x1 Qn xn. f, where f is quantifier free4Fragments MSO = X1, Xm are all unary relations 9 SO = Q1, , Qm are all existential quantifiers 9 MSO = what is that ? 9 MSO is also called monadic NP5Games for MSOThe MSO game is the following. Spoiler may choose between point move and set move: Point

3、 move Spoiler chooses a structure A or B and places a pebble on one of them. Duplicator has to reply in the other structure. Set move Spoiler chooses a structure A or B and a subset of that structure. Duplicator has to reply in the other structure.6Games for MSOTheorem The duplicator has a winning s

4、trategy for k moves if A and B are indistinguishable in MSOk What is MSOk ? Both statement and proof are almost identical to the first order case.7EVEN MSOProposition EVEN is not expressible in MSOProof: Will show that if s = ; and |A|, |B| 2k then duplicator has a winning strategy in k moves. We on

5、ly need to show how the duplicator replies to set moves by the spoiler why ?8EVEN MSO So let spoiler choose U A. |U| 2k-1. Pick any V B s.t. |V| = |U| |A-U| 2k-1. Pick any V B s.t. |V| = |U| |U| 2k-1 and |A-U| 2k-1. We pick a V s.t. |V| 2k-1 and |A-V| 2k-1. By induction duplicator has two winning st

6、rategies: on U, V on A-U, A-V Combine the strategy to get a winning strategy on A, B. how ? 9EVEN 2 MSO + Why ?10MSO Games Very hard to prove winning strategies for duplicator I dont know of any other application of bare-bones MSO games !119MSOTwo problems: Connectivity: given a graph G, is it fully

7、 connected ? Reachability: given a graph G and two constants s, t, is there a path from s to t ? Both are expressible in 8MSO how ? But are they expressible in 9MSO ?129 MSOReachability: Try this: F = 9 X. f Where f says: s, t 2 X Every x 2 X has one incoming edge (except t) Every x 2 X has one outg

8、oing edge (except s)139 MSO For an undirected graph G:s, t are connected , G F Hence Undirected-Reachability 2 9 MSO149 MSO For an undirected graph G:s, t are connected , G F But this fails for directed graphs: Which direction fails ?st159 MSOTheorem Reachability on directed graphs is not expressibl

9、e in 9 MSO What if G is a DAG ? What if G has degree k ?16Games for 9MSOThe l,k-Fagin game on two structures A, B: Spoiler selects l subsets U1, , Ul of A Duplicator replies with L subsets V1, , Vl of B Then they play an Ehrenfeucht-Fraisse game on (A, U1, , Ul) and (B, Vl, , Vl)17Games for 9MSOTheo

10、rem If duplicator has a winning strategy for the l,k-Fagin game, then A, B are indistinguishable in MSOl, k MSOl,k = has l second order 9 quantifiers, followed by f 2 FOk Problem: the game is still hard to play18Games for 9MSO The l, k Ajtai-Fagin game on a property P Duplicator selects A 2 P Spoile

11、r selects U1, , Ul A Duplicator selects B P,then selects V1, , Vl B Next they play EF on (A, U1, , Ul) and (B, V1, , Vl)19Games for 9MSOTheorem If spoiler has winning strategy, then P cannot be expressed by a formula in MSOl, kApplication: prove that reachability is not in 9MSO in class ? 20MSO and

12、Regular Languages Let S = a, b and s = (, Pa, Pb) Then S* STRUCTs What can we express in FO over strings ? What can we express in MSO over strings ?21MSO on StringsTheorem Buchi On strings: MSO = regular languages. Proof in class; next time ?Corollary. On strings: MSO = 9MSO = 8MSO22MSO and TrClTheore