Árvores Genealógicas

Linguagem das Árvores Genealógicas

Este domínio inclui factos como "Zeus é o pai de Atenas" e regras como "A avó de uma dada pessoa é a mãe de um progenitor dessa pessoa".

• Os termos deste domínio são as pessoas ou os deuses do Olimpo (Para desenjoar de famílias reais).
• Duas relações unárias determinam o sexo: $${\text{Masculino}}_1,{\text{Feminina}}_1.$$
• As relações familiares são representadas por relações binárias (palavras terminadas em "$\epsilon$" são versões neutras): $$\begin{array}{c}{\text{Progenitor}\epsilon }_2,{\text{Irm}\epsilon }_2,{\text{Irma˜o}}_2,{\text{Irma˜}}_2,{\text{Descendente}}_2,{\text{Filha}}_2,\\ {\text{Filho}}_2,{\text{Coˆnjuge}}_2,{\text{Marido}}_2,{\text{Esposa}}_2,{\text{Av}\epsilon }_2,{\text{Net}\epsilon }_2,{\text{Ti}\epsilon }_2\end{array}$$
• Como cada pessoa tem exatamente um pai e uma mãe biológicos usam-se funções: $${\text{Pai}}_1,{\text{Ma˜e}}_1.$$

Veja também:

• O sistema xy para determinar o sexo.
• Substantivos sobrecomuns.

Regras das Árvores Genealógicas

A mãe de uma pessoa é a progenitor feminina. $$\forall x,m\text{Ma˜e}\left(x\right)=m\leftrightarrow \text{Feminina}\left(m\right)\wedge \text{Progenitor}\epsilon \left(m,x\right)$$

O marido de uma pessoa é o cônjuge masculino. $$\forall x,m\text{Marido}\left(m,x\right)\leftrightarrow \text{Masculino}\left(m\right)\wedge \text{Coˆnjuge}\left(m,x\right).$$

Masculino e Feminina são conjuntos complementares. $$\forall x\text{Masculino}\left(x\right)\leftrightarrow \neg \text{Feminina}\left(x\right).$$

Progenitor e descendente são relações inversas. $$\forall x,y\text{Progenitor}\epsilon \left(x,y\right)\leftrightarrow \text{Descendente}\left(y,x\right).$$

Axiomas, Definições e Teoremas

Os axiomas são as regras "iniciais", que proporcionam o funcionamento básico de um domínio.

• Os axiomas também exprimem factos básicos: Leto é a mãe de Apolo.
• As regras das árvores genealógicas (e mais algumas nos exercícios) formam os axiomas deste domínio.

As definições são axiomas da forma

$$\forall x,yp\left(x,y\right)\leftrightarrow \cdots$$

onde uma relação ($p$ neste caso) tem uma forma equivalente ($\leftrightarrow \cdots$) onde apenas ocorrem expressões "já" definidas.

No domínio das árvores genealógicas as regras assentam apenas nas relações

$$\text{Descendente},\text{Coˆnjuge},\text{Feminina}$$

Algumas afirmações sobre um domínio são teoremas, isto é são deduzidas, via dedução natural, a partir dos axiomas. Por exemplo (exercício):

$$⊢\forall x,y\text{Irm}\epsilon \left(x,y\right)\leftrightarrow \text{Irm}\epsilon \left(y,x\right).$$