Na lógica de predicados a Instanciação Universal^[1][2][3] (IU, também chamada Especificação Universal ou Eliminação Universal, e algumas vezes confundido com Dictum de omni) é uma regra de inferência válida a partir de uma verdade sobre cada membro de uma classe de indivíduos para a verdade sobre um grupo particular daquela classe. É geralmente dada como uma regra de quantificação para o quantificador universal, contudo também pode ser codificado em um axioma. Esse é um dos princípios utilizados na Lógica de primeira ordem.

Exemplo: 

Em símbolos a regra em um esquema de axioma é

${\displaystyle \forall x\,A(x)\Rightarrow A(a/x),}$

para algum termo a onde ${\displaystyle A(a/x)}$  é o resultado da substituição de a em todas as ocorrências de x em A.

E como uma regra de inferência é:

de  ⊢ ∀x A infer ⊢ A(a/x),

sendo A(a/x) o mesmo que foi mostrado acima.

Irving Copi  notou que a Instanciação universal "...resulta de variantes das regras para 'dedução natural',que foram elaboradas de forma independente por Gerhard Gentzen e Stanisław Jaśkowski em 1934." ^[4]

Instanciação Universal e Generalização existencial são dois aspectos de um único principio, para ao invés de dizer que "∀x x=x" implica "Socrates=Socrates", nós  poderíamos assim dizer que a contradição "Socrates≠Socrates"' implica "∃x x≠x". O principio embutido nessas duas operações é a ligação entre  quantificações  e os enunciados singulares que estão relacionados a eles como instâncias. No entanto é um principio somente por cortesia. Isso ocorre somente no caso onde há denominações nos termos, e, além do mais, por referência.^[5]

• Generalização existencial
• Quantificação universal
• Regras de inferencia