Evert Willem Beth

Evert Willem Beth

Biographie

Naissance	7 juillet 1908 Almelo (d)
Décès	12 avril 1964 (à 55 ans) Amsterdam
Nationalité	néerlandaise
Formation	Université d'Utrecht
Activités	Mathématicien, ingénieur, philosophe, professeur d'université
Père	Hermanus Johannes Elisa Beth (d)

Autres informations

A travaillé pour	Université d'Amsterdam (2 novembre 1949 - 14 février 1964) Université d'Amsterdam (2 novembre 1949 - 14 février 1964) Université d'Amsterdam (2 novembre 1949 - 14 février 1964) Université d'Amsterdam (2 novembre 1949) Université d'Amsterdam (1948 - 2 novembre 1949) Université d'Amsterdam (22 mai 1946 - 2 novembre 1949) Université Johns-Hopkins Université d'Amsterdam
Membre de	Académie royale néerlandaise des arts et des sciences
Directeur de thèse	Johannes Christiaan Franken (d)

modifier - modifier le code - modifier Wikidata

Evert Willem Beth (7 juillet 1908 - 12 avril 1964) est un philosophe et logicien néerlandais dont les travaux concernent essentiellement les fondements des mathématiques.

Biographie

Beth est né dans la petite ville de Almelo aux Pays-Bas. Son père avait étudié les mathématiques et la physique à l'université d'Amsterdam où il avait obtenu un doctorat. Evert Beth étudie lui aussi les mathématiques et la physique à l'université d'Utrecht, mais aussi la philosophie et la psychologie et en 1935 il obtient un doctorat en philosophie.

En 1946 il devient professeur de logique et de fondements des mathématiques à Amsterdam; poste qu'il occupera jusqu'à sa mort en 1964, hormis deux courtes interruptions, en 1951 comme assistant chercheur auprès de Alfred Tarski et en 1957 comme professeur invité à l'université Johns-Hopkins. Il fut le premier titulaire d'une chaire de logique et de fondement des mathématiques en Hollande et il contribua activement à faire reconnaître au niveau international la logique au sein des disciplines académiques.

Apports en logique

Théorème de définissabilité

Le théorème de définissabilité énonce qu'un prédicat (via aussi une constante ou une fonction) est implicitement définissable si et seulement s'il est explicitement définissable.

Les tableaux sémantiques

Les tableaux sémantiques sont une méthode de preuve logique alliant à la fois des notions syntaxiques et sémantiques. Il se différencie des systèmes de déductions purement syntaxiques comme la déduction naturelle et le calcul des séquents de Gentzen ou les systèmes axiomatiques dits "à la Hilbert".

Ce type de méthode de résolution est jugé plus simple à acquérir pour un étudiant novice en logique et est souvent présenté dans les manuels d'initiation sous des noms et des formes légèrement différentes. Voir par exemple Logic de Wilfrid Hodges, First-order logic and automated theorem proving de Melvin Fitting, ou dans une présentation très claire en français Introduction à la Logique de François Rivenc (méthode appelée dans ce dernier ouvrage, "méthode des arbres de vérité" et élaborée par Roger Martin).

Prouver qu'un ensemble de formules implique une formule

On veut prouver qu'un ensemble ${\displaystyle \Gamma }$ de formules implique une certaine formule ${\displaystyle \phi }$ conformément aux règles de la logique du premier ordre.

On procède par l'absurde.

On commence par former la théorie T formée de toutes les formules appartenant à ${\displaystyle \Gamma }$ et de ${\displaystyle \neg \phi }$ (la négation de ${\displaystyle \phi }$).

Puis on applique des règles d'inférence

1. de type sémantique (en éliminant les quantificateurs universels et existentiels des formules par l'introduction de constantes d'individus tentant à former l'ensemble de base d'un modèle de la théorie T) et
2. de type syntaxique (par embranchements prenant une forme arborescente)

qui amènent à des formules plus simples menant à des contradictions sur chacune des branches.

Parvenu à ce point, il est établi que ${\displaystyle \Gamma \cup \{\neg \phi \}}$ est incohérent (ou plus précisément, aspect sémantique, n'est pas satisfaisable (quelles que puissent être les constantes d'individus introduites) et que ${\displaystyle \Gamma }$ implique ${\displaystyle \phi }$.

Remarque fondamentale : cette procédure aboutit toujours au résultat escompté lorsque ${\displaystyle \Gamma }$ implique bien ${\displaystyle \phi }$.

Par contre lorsque ${\displaystyle \Gamma }$ n'implique pas ${\displaystyle \phi }$, le problème consiste alors à prouver que T est cohérent (ou dit en termes sémantiques est satisfaisable), ce qui n'est pas toujours possible. Voyons donc :

Prouver qu'un ensemble de formules est cohérent

Cette méthode peut aussi s'appliquer pour prouver qu'un ensemble ${\displaystyle \Gamma }$ de formules est cohérent en arrivant à en construire un modèle ayant pour base les constantes d'individus (ou plutôt leur interprétation, voir ...) introduites.

Mais cette procédure, contrairement à la précédente, n'aboutit pas toujours lorsque ${\displaystyle \Gamma }$ est cohérent mais n'a que des modèles infinis ; voir théorème de semi-décidabilité du calcul des prédicats du premier ordre de Church.

Modèles de Beth

C'est une classe de modèles pour les logiques non classiques. (voir Sémantique de Kripke).

Bibliographie

• (en) Evert W. Beth, Formal Methods: An introduction to symbolic logic and to the study of effective operations in arithmetic and logic. D. Reidel Publishing Company / Dordecht-Holland, 1970 (ISBN 90-277-0069-9)

Articles connexes

• Gerrit Mannoury (en)
• John Alan Robinson
• Prix de thèse E. W. Beth

Liens externes

• Ressources relatives à la recherche :
  • Mathematics Genealogy Project
  • Persée
• Notices dans des dictionnaires ou encyclopédies généralistes :

  • Biografisch Woordenboek van Nederland
  • Biografisch Portaal van Nederland
  • Britannica
  • Den Store Danske Encyklopædi
  • Internetowa encyklopedia PWN
  • Treccani
• Notices d'autorité :

  • VIAF
  • ISNI
  • BnF (données)
  • IdRef
  • LCCN
  • GND
  • Japon
  • CiNii
  • Espagne
  • Pays-Bas
  • Pologne
  • Israël
  • NUKAT
  • Catalogne
  • Vatican
  • Norvège
  • Croatie
  • Tchéquie
  • WorldCat