Existentiële instantiatie

In de predicatenlogica is existentiële instantiatie (EI) een afleidingsregel die uit een propositie over een bepaald object uit het domein een propositie afleidt over een specifiek object in dat domein. Deze propositie maakt gebruik van de existentiekwantor. Formeel verloopt existentiële instantiatie als volgt:

${\frac {\exists x\ P(x)}{P(c_{0})}}$

waarbij c₀ een nieuwe, nog niet eerder gebruikte constante is. Deze redenatie is geldig aangezien we alleen een naam geven aan een bestaande x. Een voorbeeld (met $\mathbb {N}$, de natuurlijke getallen als domein): "Er is een getal dat deelbaar is door 2. c is deelbaar door 2.". De constante c is één specifiek getal uit het domein dat deelbaar is door 2.

Bij het kiezen van een constante moet een nieuwe constante gekozen worden aangezien het predicaat niet hoeft te gelden voor eerder gebruikte (bekende) constanten. Een nieuw gekozen constante wordt ook wel een skolemconstante genoemd, vernoemd naar de Noorse wiskundige Albert Thoralf Skolem. Wanneer men een eerder gebruikte constante invult, is het mogelijk ongeldige proposities af te leiden: stel, men ontdekt een getal x waarvoor geldt:

$x=\lim _{n\to \infty }(1+{\frac {1}{n}})^{n}$.

dan is het mogelijk deze een nieuwe naam te geven, zoals e, maar het zou onjuist zijn om een al bestaande constante, zoals π, te gebruiken.

Als er voor de existentiekwantor nog universele kwantoren staan, dan dient men een functie in te vullen met de variabelen van die kwantor(en) aangezien het ingevulde object uit het domein afhangt van de objecten die ingevuld zijn bij de variabelen van de universele kwantor(en). Zo'n functie wordt een skolemfunctie genoemd.

Zie ook

• Existentiële generalisatie
• Universele instantiatie
• Universele generalisatie