Feferman–Vaught-satsen

Feferman–Vaught-teorem i modellteori är en teorem av Solomon Feferman och Robert Lawson Vaught som visar hur man på ett algoritmiskt sätt reducerar första ordningens teori om en produkt av första ordningens strukturer till första ordningens teori om element av strukturen.

Satsen anses vara ett av standardresultaten inom modellteori. Satsen utökar det tidigare resultatet av Andrzej Mostowski på direkta produkter av teorier. Den generaliserar (till formler med godtyckliga kvantifierare) egenskapen i universell algebra att likheter (identiteter) överför till direkta produkter av algebraiska strukturer (vilket är en följd av en riktning av Birkhoffs sats ).

Direkt produkt av strukturer

Betrakta en första ordningens logiksignatur L . Definitionen av produktstrukturer tar en familj av L -strukturer $\mathbf {A} _{i}$ för $i\in I$ för någon indexuppsättning I och definierar produktstrukturen ${\displaystyle \mathbf {A} =\prod _{i\in I}\mathbf {A} _{i}} ,$ som också är en L -struktur, med alla funktioner och relationer definierade punktvis.

Definitionen generaliserar direkt produkt i universell algebra till relationella första ordningens strukturer, som innehåller inte bara funktionssymboler utan även relationssymboler.

Om $r(a_{1},\ldots ,a_{p})$ är en relationssymbol med $p$ -argument i L och ${\displaystyle a_{1},\ldots ,a_{n}\in \Pi _{i\in I}\mathbf {A} _{i}} är element$ i kartesiskan produkt definierar vi tolkningen av $r$ i $\mathbf {A}$ av

$\mathbf {A} \models r(a_ {1},\ldots ,a_{p})\iff \forall i\in I,\ \mathbf {A} _{i}\modeller r(a_{1}(i),\ldots ,a_{p} (i))$

När $r$ är en funktionell relation reduceras denna definition till definitionen av direkt produkt i universell algebra .

Uttalande av satsen för direkta produkter

För en första ordningens logikformel $\phi ({\bar {x}})$ i signatur L med fria variabler, och för en tolkning ${\bar {a}}$ av variablerna ${\bar {x}}$ definierar vi uppsättningen av index $i$ för vilka $\phi ({\bar {a}} )$ håller i $\mathbf {A} _{i}$

$||\phi ({\bar {a}})||=\{i\mid \mathbf {A} _{i}\ modeller \phi ({\bar {a}}(i))\}$

Givet en första ordningens formel med fria variabler ${\displaystyle \phi ({\bar {x}})} ,$ finns det en algoritm för att beräkna dess ekvivalenta spelnormalform, vilket är en finit disjunktion $\bigvee _{i=0}^{k-1}\theta ({\bar {x}})$ av sinsemellan motstridiga formler.

Feferman-Vaught-satsen ger en algoritm som tar en första ordningens formel $\phi ({\bar {x}})$ och konstruerar en formel $\phi ^{*}$ som reducerar villkoret som $\phi ({\bar {a}})$ har i produkten till villkoret som $\phi ^{*}$ har i tolkningen av $k+1$ uppsättningar index:

$I,||\theta _{0}({\bar {a}})||,\ldots ,||\theta _{k-1}({\bar {a}})||$

Formel $\phi ^{*}$ är alltså en formel med $k+1$ fria mängdvariabler, till exempel i första ordningens teori för boolesk algebra av mängder.

Bevis idé

Formel $\phi ^{*}$ kan konstrueras enligt strukturen för startformeln $\phi ^{*}$ . När $\phi$ är kvantifieringsfri, så följer den, per definition av direkt produkt ovan,

${\begin{array}{rl}\mathbf {A} \models \phi ({\bar {a}})&\iff \forall i\in I.\ \mathbf {A} _{ i}\models \phi ({\bar {a}}(i))\\&\iff \{i\mid \mathbf {A} _{i}\models \phi ({\bar {a}}( i))\}=I\\&\iff ||\phi ({\bar {a}})||=I\end{array}}$

Följaktligen kan vi ta $\phi ^{*}(U,X_{1})$ för att vara likheten $U=X_{1}$ i språket för den booleska algebra av mängder (motsvarande fältet för mängder ).

Att utöka villkoret till kvantifierade formler kan ses som en form av kvantifierareliminering , där kvantifiering över produktelement ${\bar {a}}$ i $\phi$ reduceras till kvantifiering över delmängder av $I$ .

Generaliserade produkter

Det är ofta av intresse att överväga understrukturen av den direkta produktstrukturen. Om begränsningen som definierar produktelement som hör till understrukturen kan uttryckas som ett villkor på uppsättningarna av indexelement, då kan resultaten generaliseras.

Ett exempel är understrukturen av produktelement som är konstanta överhuvudtaget men ändligt många index. Antag att språket L innehåller en konstant symbol $c$ och betrakta understrukturen som endast innehåller de produktelement som $a$ för vilken uppsättningen

$\{i\mid {\textbf {A}}_{i}\models a(i)\neq c\}$

är ändlig. Teoremet reducerar sedan sanningsvärdet i en sådan understruktur till en formel $\phi ^{*}$ i den booleska algebra av mängder, där vissa mängder är begränsade till att vara ändliga.

Ett sätt att definiera generaliserade produkter är att överväga de understrukturer där uppsättningarna $||\phi (a)||$ tillhör någon boolesk algebra $B$ av mängder $X\subseteq I$ av index (en delmängd av powersetmängden algebra ${ \displaystyle 2^{I}}$ ), och där produktens understruktur tillåter limning. Här hänvisar erkännande av limning till följande stängningsvillkor: om $a,b$ är två produktelement och $X\in B$ är elementet i den booleska algebra, så är elementet det också $c$ definieras genom att "limma" $a$ och $b$ enligt $X$ :

$c(i)=\left\{{\begin{array}{rl}a (i),&{\mbox{ if }}i\in X\\b(i),&{\mbox{ if }}i\in (I\setminus X)\end{array}}\right.$

Konsekvenser

Feferman-Vaught-satsen antyder avgörbarheten av Skolem-aritmetiken genom att se, via aritmetikens grundläggande sats , strukturen naturliga tal med multiplikation som en generaliserad produkt (potens) av Presburgers aritmetiska strukturer.