Herbrandization

Herbrandiseringen av en logisk formel (uppkallad efter Jacques Herbrand ) är en konstruktion som är dubbel till skolemiseringen av en formel . Thoralf Skolem hade övervägt Skolemiseringarna av formler i prenex-form som en del av sitt bevis på Löwenheim-Skolem-satsen (Skolem 1920). Herbrand arbetade med denna dubbla föreställning om Herbrandization, generaliserad till att gälla även icke-prenex-formler, för att bevisa Herbrands teorem (Herbrand 1930).

Den resulterande formeln är inte nödvändigtvis likvärdig med den ursprungliga. Precis som med Skolemization, som bara bevarar tillfredsställelse , bevarar Herbrandization, som är Skolemizations dubbla, giltighet : den resulterande formeln är giltig om och endast om den ursprungliga är det.

Definition och exempel

Låt $F$ vara en formel på språket för första ordningens logik . Vi kan anta att $F$ inte innehåller någon variabel som är bunden av två olika kvantifieringsförekomster, och att ingen variabel förekommer både bunden och fri. (Det vill säga att $F$ skulle kunna ombokstavas för att säkerställa dessa villkor, på ett sådant sätt att resultatet blir en ekvivalent formel).

Herbrandiseringen av $\displaystyle F}$ { erhålls sedan enligt följande:

• Ersätt först eventuella fria variabler i $F$ med konstantsymboler.
• För det andra, ta bort alla kvantifierare på variabler som antingen är (1) universellt kvantifierade och inom ett jämnt antal negationstecken, eller (2) existentiellt kvantifierade och inom ett udda antal negationstecken.
• Slutligen, ersätt varje sådan variabel $v$ med en funktionssymbol $f_{v}(x_{1},\dots ,x_{k})$ , där $x_{1},\dots ,x_{k}$ är de variabler som fortfarande är kvantifierade och vars kvantifierare styr $v$ .

Tänk till exempel formeln $F:=\för allt y\exists x[R(y,x) \wedge \neg \exists zS(x,z)]$ . Det finns inga fria variabler att ersätta. Variablerna $y,z$ är den typ vi överväger för det andra steget, så vi tar bort kvantifierarna $\forall y$ och $\exists z$ . Slutligen ersätter vi $y$ med en konstant $c_{y}$ (eftersom det inte fanns några andra kvantifierare som styrde $y$ ), och vi ersätter $z$ med en funktionssymbol $f_{z}(x)$ :

$F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].$

Skolemiseringen av en formel erhålls på liknande sätt, förutom att i det andra steget ovan skulle vi ta bort kvantifierare på variabler som antingen är (1) existentiellt kvantifierade och inom ett jämnt antal negationer, eller (2) universellt kvantifierade och inom ett udda tal av negationer. Sålunda, med tanke på samma $F$ från ovan, skulle dess Skolemisering vara:

$F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].$

För att förstå betydelsen av dessa konstruktioner, se Herbrands sats eller Löwenheim–Skolems sats .

Se även

• Predikatfunktionslogik

• Skolem, T. "Logiko-kombinatoriska undersökningar i tillfredsställelsen eller bevisbarheten av matematiska påståenden: Ett förenklat bevis på ett teorem av L. Löwenheim och generaliseringar av teorem". (I van Heijenoort 1967, 252-63.)
• Herbrand, J. "Undersökningar i bevisteori: egenskaperna hos sanna påståenden". (I van Heijenoort 1967, 525-81.)
• van Heijenoort, J. Från Frege till Gödel: A Source Book in Mathematical Logic, 1879-1931 . Harvard University Press, 1967.