Gerhard Gentzen

Gerhard Gentzen Imagem na Infobox. Gerhard Gentzen em Praga em 1945 Biografia
Aniversário 24 de novembro de 1909
Greifswald
Morte 4 de agosto de 1945(em 35)
Praga
Enterro Cemitério Ďáblice ( em )
Nome na língua nativa Gerhard Karl Erich Gentzen
Nacionalidade alemão
Treinamento Universidade de Göttingen
Atividades Matemático , filósofo , professor , professor universitário
Outra informação
Trabalhou para Universidade Charles de Praga , Universidade de Göttingen
Campo Matemática
Partido politico Partido Nacional Socialista dos Trabalhadores Alemães
Membro de Sturmabteilung
Diretores de teses Paul Bernays , Hermann Weyl

Gerhard Gentzen (24 de novembro de 1909em Greifswald -4 de agosto de 1945em Praga ) é um matemático e lógico alemão , cujo trabalho é fundamental na teoria da demonstração . Ele foi um dos alunos de Weyl na Universidade de Göttingen de 1929 a 1933. Ele morreu em um campo de prisioneiros de guerra em 1945, depois de ser preso pelos soviéticos por sua lealdade nazista .

Biografia

Gentzen é aluno de Paul Bernays na Universidade de Göttingen . Mas este último foi rejeitado como um "não-ariano" emAbril de 1933, Hermann Weyl torna-se formalmente seu orientador de tese. Gentzen juntou-se às seções de assalto em novembro de 1933, quando não tinha nenhuma obrigação. No entanto, ele permaneceu em contato com Bernays até o início da Segunda Guerra Mundial . Em 1935, ele se correspondeu com Abraham Fraenkel em Jerusalém e foi reconhecido pelo sindicato dos professores nazistas como aquele que “mantém contato com o Povo eleito”. Em 1935 e 1936, Hermann Weyl, diretor do departamento de matemática em Göttingen de 1933 até sua renúncia sob pressão nazista, fez grandes esforços para levá-lo para participar do Instituto de Estudos Avançados de Princeton .

Entre Novembro de 1935e 1939 foi assistente de David Hilbert em Göttingen. Gentzen juntou-se ao partido nazista em 1937. EmAbril de 1939, Gentzen faz um juramento de lealdade a Adolf Hitler como parte de seu cargo na Universidade. A partir de 1943 ele foi professor da Universidade de Praga. Sob um contrato com a SS , Gentzen trabalha para o projeto V-2 .

Após a guerra, ele morreu de fome em um campo depois de ser preso em Praga, o 7 de maio de 1945.

Trabalho

Gentzen inventou dois sistemas de dedução para lógica de primeira ordem, dedução natural e cálculo de sequentes . Para este último, ele demonstrou seu Hauptsatz (teorema principal), denominado mais explicitamente "teorema da eliminação do corte", publicado em 1934 em sua Pesquisa sobre dedução lógica .

“O teorema fundamental afirma que qualquer demonstração puramente lógica pode ser reduzida a uma determinada forma normal, que aliás não é de forma alguma unívoca. As propriedades essenciais de tal prova normal podem ser formuladas aproximadamente da seguinte maneira: ela não envolve quaisquer desvios. Não é introduzido nenhum conceito que não esteja contido em seu resultado final e que, portanto, não deva necessariamente ser utilizado para obter esse resultado. "

Gentzen, por outro lado, demonstrou a consistência da aritmética de Peano (em 1936) usando um princípio de indução até o ordinal contável ε 0 , mas para fórmulas de baixa complexidade lógica. Os métodos usados ​​para esta demonstração provaram ser essenciais para a teoria da demonstração moderna.

A teoria em que esta prova pode ser formalizada é necessariamente mais forte do que a aritmética de Peano de acordo com o segundo teorema da incompletude de Gödel (no sentido de que se permite demonstrar a consistência da aritmética de Peano, sua consistência não pode ser demonstrada nesta aritmética). Pudemos ver essa prova, na qual Gödel se interessou muito, como uma tentativa de reabilitar o programa de Hilbert , estendendo a noção de métodos finitários para recorrências até certos ordinais como ε 0 . A consistência da teoria usada por Gentzen para sua prova, embora mais forte, seria menos duvidosa do que a consistência da aritmética de Peano, porque a indução, embora até um ordinal (necessariamente maior que a dos inteiros), é feita em fórmulas simples. Esta última afirmação dificilmente tem mais defensores. Mais objetivamente, essa demonstração nos permite analisar as razões da consistência da aritmética de Peano; por exemplo, o resultado da coerência torna possível medir sua “força” refletida pelo uso do ordinal ε 0 . Generalizando esse princípio, fomos capazes de iniciar uma classificação de teorias aritméticas.

Teoremas de Gentzen

Gentzen é conhecido por dois teoremas:

  1. o teorema da eliminação de cortes no cálculo de sequentes,
  2. o teorema da consistência aritmética (ver também teorema da consistência aritmética  (em) )

Referências

  1. Jean-Louis Gardies , Sketch of a Pure Grammar , Vrin ,1975( apresentação online ) , p.  35
  2. Gerhard Gentzen ( trad.  R. Feys e J. Ladrière), Pesquisa sobre dedução lógica [“Untersuchungen über das logische schließen”], Presses Universitaires de France, 1955, p.  4-5.Traduzido e comentado
  3. Gerhard Gentzen, “  Untersuchungen über das logische Schließen. I  ”, Mathematische Zeitschrift , vol.  39, n o  21934, p.  176-210 ( ler online ).
  4. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie , Math. Ann .. 112 (1936), 493-565. Tradução francesa A consistência da aritmética elementar de Jean Largeault , em Intuicionismo e teoria da demonstração, páginas 285-357 Paris, Vrin, 1992
  5. Neue Fassung des Widerspruchsfreiheitsbeweises fur die Reine Zahlentheorie , Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, neue Folge, Heft 4, p. 19-44. S. Hirzel, Leipzig, 1938. Tradução francesa Nova versão da demonstração de consistência para aritmética elementar por Jean Largeault , em Intuicionismo e teoria da demonstração páginas 359-394 Paris, Vrin, 1992

Bibliografia

links externos