Satz von Karp-Lipton:

Wenn es polynomiell grosse Schaltkreise fuer SAT gibt, dann kollabiert die PH auf der 2. Stufe.

Erlaeuterung: Die Voraussetzung des Satzes bedeutet, dass ein Polynom
s(n) existiert und fuer jedes n ein boolescher Schaltkreis C_n der
Groesse s(n) und mit n Eingaengen, sodass fuer alle aussagenlogischen
Formeln phi mit |phi|<=n gilt C_n(phi)=1 <=> phi:SAT. Hierbei bedeutet
C_n(phi) den Output des Schaltkreises C_n, wenn an seinen n Eingaengen
die Binaerkodierung der Formel phi eingespeist wird. Der Schaltkreis
C_n ist also ein "SAT-Chip", der das SAT-Problem fuer alle Instanzen
der *festen* Groesse <=n loesen kann. Wichtig ist, dass C_n als
Schaltkreis nur polynomielle Groesse hat. Solche Schaltkreise
exponentieller Groesse lassen sich leicht angeben. Sie koennten
z.B. die gesamte Wahrheitstafel der Groesse 2^n als grosse
Fallunterscheidung festverdrahten.

Liegt solch ein Schaltkreis C_n vor, so kann er leicht in einen
Schaltkreis D_n von ebenfalls polynomieller Groesse umgebaut werden,
der im Falle einer positiven Antwort auch noch eine erfuellende
Belegung liefert.

Hat etwa phi die Variablen x1..xm, so ergibt sich D_n aus folgendem Pseudocode:

if (C_n(phi)) return (_,false);
if (C_n(phi[x1:=true])) v1=true; else v1=false;
if (C_n(phi[x1:=v1,x2:=true])) v2=true; else v2=false;
if (C_n(phi[x1:=v1,x2:=v2,x3:=true])) v3=true; else v3=false;
...
if (C_n(phi[x1:=v1,x2:=v2,...,x(m-1):=v(m-1),xm:=true])) vm=true; else vm=false;
return ([x1->v1,\dots,xm->vm],true)

Es ist klar, dass die Groesse von D_n ebenfalls polynomiell beschraenkt ist, sagen wir |D_n|<=q(n) und dass fuer |phi|<=n gilt:

phi:SAT <==> D_n(phi)=(eta,true) & eta|=phi

Wir nennen solch einen Schaltkreis "selbstzertifizierenden
SAT-Tester". Die Tatsache, dass ein solcher aus C_n gewonnen werden
kann, bezeichnet man als "Selbstreduzierbarkeit von SAT".

Jetzt zum Beweis des Satzes. Wir zeigen zunaechst Pi_2^P <= Sigma_2^P.

Wir fixieren L:Pi_2^P, also

x:L <=> forall_p(|x|) y.exists_p(|x|) z. (x,y,z):L'

wobei p ein Polynom ist und L':P. Erinnerung: exists_n x.A(x) bedeutet
exists x.|x|<=n & A(x).

Es ist nunmehr:

x:L <=> exists_s(q(t(|x|))) D.
    "D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)" &
    forall_p(|x|) y.D("exists_p(|x|) z.(x,y,z):L'")=(_,true)


Hier steht "exists_p(|x|) z.(x,y,z):L'" fuer eine Boolesche Formel,
die erfuellbar ist, gdw exists_p(|x|) z.(x,y,z):L' und t(|x|) ist ihre
Groesse. Klar kann t polynomiell gewaehlt werden. Die Variablen dieser
Formel repraesentieren den Wert von z.

Die Eigenschaft "D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)" 
kann nun wie folgt als Pi_1^P Formel geschrieben werden:

"D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)"  <=>

forall_t(|x|) phi.D(phi)=(eta,true) & eta|=phi \/
              D(phi)=(_,false) & forall_t(|x|) rho.rho|=/=phi

<=>

forall_t(|x|) phi.forall_t(|x|) rho. D(phi)=(eta,true) & eta|=phi \/
              D(phi)=(_,false) & rho|=/=phi


Somit gilt


x:L <=> exists_s(q(t(|x|))) D.
forall_t(|x|) phi.forall_t(|x|) rho. forall_p(|x|) y.
(D(phi)=(eta,true) & eta|=phi \/
              D(phi)=(_,false) & rho|=/=phi) & 
    D("exists_p(|x|) z.(x,y,z):L'")=(_,true)

was das geforderte Sigma_2^P Format hat. 

Der Kollaps der PH auf die zweite Stufe ergibt sich daraus als
einfache praedikatenlogische Konsequenz.