Origem: Wikipédia, a enciclopédia livre.
Na lógica de predicados , generalização (também generalização universal ou introdução universal ,[ 1] [ 2] [ 3] GEN ) é uma regra de inferência valida . Ela afirma que se
⊢
P
(
x
)
{\displaystyle \vdash P(x)}
⊢
∀
x
P
(
x
)
{\displaystyle \vdash \forall x\,P(x)}
A regra da generalização completa permite hipóteses à esquerda da Catraca(simbolo) , porém com restrições. Assuma que Γ é um conjunto de fórmulas, φ uma fórmula, e
Γ
⊢
φ
(
y
)
{\displaystyle \Gamma \vdash \varphi (y)}
Γ
⊢
∀
x
φ
(
x
)
{\displaystyle \Gamma \vdash \forall x\varphi (x)}
y não é mencionado em Γ e x não ocorre em φ.
Essas restrições são necessárias devido à correção . Sem a primeira restrição pode-se concluir
∀
x
P
(
x
)
{\displaystyle \forall xP(x)}
P
(
y
)
{\displaystyle P(y)}
∃
z
∃
w
(
z
≠
w
)
{\displaystyle \exists z\exists w(z\not =w)}
∃
w
(
y
≠
w
)
{\displaystyle \exists w(y\not =w)}
Instanciação existencial )
y
≠
x
{\displaystyle y\not =x}
Instanciação existencial )
∀
x
(
x
≠
x
)
{\displaystyle \forall x(x\not =x)}
Isso supostamente mostra que
∃
z
∃
w
(
z
≠
w
)
⊢
∀
x
(
x
≠
x
)
,
{\displaystyle \exists z\exists w(z\not =w)\vdash \forall x(x\not =x),}
Provar:
∀
x
(
P
(
x
)
→
Q
(
x
)
)
→
(
∀
x
P
(
x
)
→
∀
x
Q
(
x
)
)
{\displaystyle \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))}
Prova:
Number
Formula
Justification
1
∀
x
(
P
(
x
)
→
Q
(
x
)
)
{\displaystyle \forall x\,(P(x)\rightarrow Q(x))}
Hipótese
2
∀
x
P
(
x
)
{\displaystyle \forall x\,P(x)}
Hipótese
3
(
∀
x
(
P
(
x
)
→
Q
(
x
)
)
)
→
(
P
(
y
)
→
Q
(
y
)
)
)
{\displaystyle (\forall x\,(P(x)\rightarrow Q(x)))\rightarrow (P(y)\rightarrow Q(y)))}
Instanciação universal
4
P
(
y
)
→
Q
(
y
)
{\displaystyle P(y)\rightarrow Q(y)}
De (1) e (3) por Modus ponens
5
(
∀
x
P
(
x
)
)
→
P
(
y
)
{\displaystyle (\forall x\,P(x))\rightarrow P(y)}
Instanciação universal
6
P
(
y
)
{\displaystyle P(y)\ }
De (2) e (5) por Modus ponens
7
Q
(
y
)
{\displaystyle Q(y)\ }
De (6) e (4) por Modus ponens
8
∀
x
Q
(
x
)
{\displaystyle \forall x\,Q(x)}
De (7) by Generalização
9
∀
x
(
P
(
x
)
→
Q
(
x
)
)
,
∀
x
P
(
x
)
⊢
∀
x
Q
(
x
)
{\displaystyle \forall x\,(P(x)\rightarrow Q(x)),\forall x\,P(x)\vdash \forall x\,Q(x)}
Resumo de (1) à (8)
10
∀
x
(
P
(
x
)
→
Q
(
x
)
)
⊢
∀
x
P
(
x
)
→
∀
x
Q
(
x
)
{\displaystyle \forall x\,(P(x)\rightarrow Q(x))\vdash \forall x\,P(x)\rightarrow \forall x\,Q(x)}
De (9) por Teorema da dedução
11
⊢
∀
x
(
P
(
x
)
→
Q
(
x
)
)
→
(
∀
x
P
(
x
)
→
∀
x
Q
(
x
)
)
{\displaystyle \vdash \forall x\,(P(x)\rightarrow Q(x))\rightarrow (\forall x\,P(x)\rightarrow \forall x\,Q(x))}
De (10) por Teorema da dedução
Nessa prova , a Generalização universal foi usada no passo 8. O Teorema da dedução era aplicável nos passos 10 e 11 porque as formulas sendo movidas não têm variáveis livres.
↑ Copi and Cohen
↑ Hurley
↑ Moore and Parker
