Evert Willem Beth
# Evert Willem Beth

Evert Willem Beth (7 de julho de 1908 – 12 de abril de 1964) foi um filósofo e lógico holandês, que trabalhou, principalmente, em questões relacionadas aos fundamentos da matemática.

## Biografia

Beth nasceu em Almelo, uma pequena cidade no leste da Holanda. Seu pai estudou matemática e física na Universidade de Amesterdã, onde ele tinha sido premiado com um Ph.D. Evert Beth estudou as mesmas disciplinas na Universidade de Utrecht, mas depois também estudou filosofia e psicologia. Seu Ph. D. em filosofia foi em 1935.
Em 1946, tornou-se professor de lógica e fundamentos da matemática em Amesterdã. Além de duas breves interrupções – de uma temporada em 1951, como um assistente de pesquisa para Alfred Tarski, e em 1957, como professor visitante na Universidade Johns Hopkins – ele ocupou o cargo continuamente, até sua morte em 1964. O seu curso foi o primeiro de pós em lógica e fundamentos da matemática em seu país, e durante esse tempo, ele contribuiu ativamente para a cooperação internacional no estabelecimento de lógica como disciplina acadêmica.
Em 1953 tornou-se membro da Academia Real das Artes e Ciências dos Países Baixos.
Ele morreu em Amsterdã.

## Contribuições para a lógica
### Teorema da definição

O teorema da definição afirma que um predicado (ou função, ou constante) é implicitamente definível se e somente se ele é explicitamente definível. Explicação adicional é fornecida sob a definibilidade de Beth

### Tableaux semânticos

Tableaux semânticos é um método de prova para sistemas formais, tais como, dedução natural de Gentzen, cálculo de sequentes, ou até mesmo o método da resolução de J. Alan Robinson e sistema axiomático de Hilbert . É considerado por muitos um método intuitivamente simples, especialmente para os alunos não familiarizados com o estudo de lógica (Wilfrid Hodges , por exemplo, apresenta tableaux semânticos em seu livro-texto introdutório, Logic, e Melvin Fitting faz o mesmo em sua apresentação de lógica de primeira ordem para cientistas da computação, First-order logic and automated theorem proving).
O método começa com a intenção de provar que um determinado conjunto $\Gamma$ de fórmulas implica outra fórmula $\varphi$, dado um conjunto de regras determinadas pela semântica dos conectivos (e quantificadores, na lógica de primeira ordem) das fórmulas. O método procede admitindo verdadeiras cada membro do conjunto $\Gamma$ e $\neg \varphi$ (a negação de $\varphi$) e, em seguida, aplica as regras de ramificação em uma estrutura de árvore de fórmulas (mais simples) até que todos os possíveis ramos contenham uma contradição (ou não). Neste ponto, vai ter sido estabelecido que $\Gamma \cup \{\neg \varphi \}$ é inconsistente (insatisfatível), e, portanto, que as fórmulas de $\Gamma$ juntas implicam em $\varphi$.

### Modelos de Beth

Estas são classes de modelos relacionais para a lógica não-clássica (A semântica de Kripke).