Que paradigma de prova automatizada de teoremas é apropriado para a formalização no estilo Principia Mathematica?

11

Possuo um livro que, inspirado nos Principia Mathematica de Russell e no positivismo lógico, tenta formalizar um domínio específico, determinando axiomas e deduzindo deles teoremas. Em suma, ele tenta fazer por seu domínio o que o PM tentou fazer pela matemática. Como o PM, foi escrito antes que a prova automatizada de teoremas (ATP) fosse possível.

Estou tentando representar esses axiomas em um sistema moderno de ATP e tentar deduzir teoremas, inicialmente aqueles deduzidos pelo autor (à mão). Eu nunca usei um sistema ATP antes e, considerando a infinidade de opções (HOL, Coq, Isabelle e muito mais), cada uma com seus pontos fortes, pontos fracos e aplicativos pretendidos, está se mostrando difícil decidir qual é apropriado para minhas necessidades específicas. objetivo.

O formalismo do autor espelha de perto o PM. Existem classes (conjuntos?), Classes de classes e assim por diante até 6 níveis de hierarquia. Há lógica de primeira ordem e possivelmente de ordem superior. Dada a conexão com o PM, eu investiguei inicialmente o Metamath, pois vários teoremas do MP foram provados no MetaMath por outras pessoas. No entanto, Metamath é obviamente um verificador de prova e não um sistema ATP.

Passando por descrições de vários sistemas ATP, vejo várias características, como implementações da teoria de tipos de Church, teorias de tipos construtivas, teorias de tipos intuicionistas, teoria de conjuntos tipificados / não tipados, dedução natural, tipos de cálculo lambda, polimorfismo, teoria de funções recursivas e a existência de igualdade (ou não). Em resumo, cada sistema parece implementar uma linguagem muito diferente e deve ser apropriado para formalizar coisas diferentes. Suponho que as bibliotecas existentes para formalizar a matemática não sejam relevantes para o meu propósito.

Qualquer conselho sobre as características que devo procurar ao escolher um ATP, ou qualquer outro conselho que você possa ter depois de ler esta pergunta, será muito apreciado. Para referência, aqui está uma página de amostra do livro. Infelizmente, como o PM, está na notação Peano-Russell.

Página do livro

O livro -

"O método axiomático em biologia" (1937), JH Woodger, A. Tarski, WF Floyd

Os axiomas começam com o mereológico. Por exemplo,

xααxyxzαy

S=Dfx^α^{αPx:.(y):yPx..(z).zα.PyPzΛ}

Novamente, observe que essa é a notação de Peano-Russell (a notação de Principia).

Axiomas posteriores têm conteúdo biológico, como

7.4.2 Quando gametas de dois membros de uma classe Mendeliana se unem em pares para formar zigotos, a probabilidade de qualquer par se unir é igual à do outro par.

Pelo que entendi, isso era um postulado da genética mendeliana.

Omiti a notação disso, porque tem três linhas e se baseia em conteúdo definido anteriormente.

Exemplo de um teorema -

Teorema

Aparentemente, isso carrega uma interpretação significativa na genética mendeliana, que, não sendo historiador da biologia, eu não entendo. No livro, foi deduzido à mão.

Obrigado!

Atriya
fonte
Existe um interesse histórico em seguir exatamente o livro, ou você poderia simplesmente extrair a essência (a configuração básica e os axiomas) e formalizar a teoria em um sistema moderno disponível?
Andrej Bauer
@andrej: Sim, extrair e formalizar a essência de um sistema moderno é o meu objetivo. Não seria necessário deduzir todos os teoremas deduzidos à mão no livro. Em vez disso, seria legal deduzir teoremas que não estão no livro, a partir dos axiomas do livro.
Atriya
5
Nesse caso, você deve entender o texto e, em seguida, fazê-lo em qualquer assistente de prova e / ou provador de teoremas que pareça mais adequado ao seu objetivo.
Andrej Bauer

Respostas:

8

Principia Mathematica foi uma grande resposta aos vários paradoxos descobertos na lógica matemática na virada do século XX. No entanto, o trabalho em si, que muitas vezes tem sido obliquamente elogiado como uma "obra-prima ilegível", é um pouco desajeitado e fundações mais modernas foram criadas. Para descrever a maior parte da matemática, você tem várias opções: a teoria das categorias é uma, a teoria dos tipos tem sido popular em alguns projetos como uma extensão do cálculo lambda, mas a mais bem compreendida e fundamental é provavelmente a teoria dos conjuntos.

A teoria dos conjuntos tem várias formulações diferentes; A teoria dos conjuntos de Zermelo Frankel, com o axioma da escolha, é a mais ortodoxa, carinhosamente referida como pelos entusiastas da teoria dos conjuntos. A teoria dos conjuntos de Tarski-Grothendiek é outra amplamente semelhante ao que inclui o axioma de Tarski para raciocinar sobre grandes categorias. Isso é interessante para verificação, mas um pouco mais difícil para a prova automatizada de teoremas, porque o esquema de substituição de axiomas admite um número infinito de axiomas que representam um desafio para implementação. Embora essas fundações sejam perfeitamente razoáveis ​​para sistemas de verificação de provas, como Mizar para Tarski-Grothendiek, teoria dos conjuntos e Metamath paraZFC ZFCZFC, para um sistema real de prova de teoremas, seria bom ter axiomatização finita.

A base provavelmente mais apropriada para isso é a teoria dos conjuntos de Von Neumann-Bernays-Gödel, ou , que admite axiomatização finita por ser uma teoria de duas classes que possui uma ontologia de classes e conjuntos adequados. Além disso, ficou provado que é uma extensão conservadora de , de modo que qualquer teorema de é um teorema deN B G Z F C N B G Z F CNBGNBGZFCNBGZFC. A razão pela qual essa teoria é a mais apropriada para o raciocínio automatizado, na minha opinião, é expressável em lógica de primeira ordem, que admite um cálculo de prova eficaz, sólido e completo, e axiomatização finita significa que ela pode ser usada com resolução de primeira ordem, que nos fornece a resultado organizado: se uma declaração for decidida, uma prova será encontrada.

A lógica proposicional não é expressiva o suficiente, e a lógica de ordem superior, embora muito mais expressiva, não admite um cálculo de prova eficaz, sólido e completo. A lógica de primeira ordem com a teoria dos conjuntos permite representar e mapear teorias lógicas de ordem superior, portanto, para fundações esse é o ponto ideal ... exceto a possibilidade de declarações indecidíveis (graças a Gödel.) E é por isso que as teorias de primeira ordem com classificação quantificadora suficiente são frequentemente descritos como semi-decidíveis.

Art Quaife fez algum trabalho sobre isso em: Desenvolvimento automatizado de teorias matemáticas fundamentais, onde implementou na lógica de primeira ordem em forma de oração, para que pudesse ser usado por um provador de teoremas baseado em resolução (Otter) e uma excelente referência para abordar as bases para esse tipo de trabalho são a Introdução à lógica matemática de Elliott Mendelson .NBG

Agora, os assistentes de prova modernos geralmente se preocupam menos com os fundamentos do paradigma da Principia Mathematia e são mais úteis para a comprovação de teoremas para o trabalho cotidiano e, portanto, têm algum suporte para fragmentos de lógica de ordem superior, resolução de SAT / SMT, teorias de tipos e outros abordagens mais informais e menos fundamentais. Mas se você está tentando fazer algo como o Principia Mathematica, é ideal um provador de teoremas de resolução de primeira ordem com uma teoria de conjuntos de primeira ordem finamente axiomatizável.

Para alguns exemplos de como os provadores de teoremas automatizados atacam os problemas dessas fundações, o site TPTP (Milhares de problemas para provedores de teoremas ) tem um bom número de problemas e você notará que muitos dos problemas fundamentais da teoria dos números são encontrados em teoria dos conjuntos . Se você tiver tempo, confira NUM006-1.p no site: a conjectura de Goldbach. Você pode tentar executá-lo, e se o seu decidable, uma prova vai finalmente ser encontrada.NBG

Os teoremas de seu livro quase certamente serão teoremas de vez que foram escritos na linguagem da teoria dos conjuntos. Os axiomas da genética nesse livro quase certamente serão representados como definições em predicados teóricos definidos, da mesma forma que a aritmética Peano é representada em como definições de predicados. A partir daí, você segue o procedimento de resolução em qualquer ATP. Escolha uma afirmação que deseja provar, negue-a, converta para a forma normal de Skolem, depois para a forma de oração e siga a resolução. Quando você encontra a cláusula vazia, encontrou uma contradição, comprovando a afirmação.N B GNBGNBG

A tarefa que você tem em mãos, se quiser tentar definir a teoria em termos da teoria dos conjuntos, é encontrar as definições de predicado relacional separadas da teoria dos conjuntos, que permitirão que você faça os predicados em termos da teoria dos conjuntos. Novamente, um exemplo disso é como definimos a aritmética Peano na teoria dos conjuntos, que por si só não possui definições de números, adição, multiplicação ou mesmo igualdade. Como exemplo de uma definição teórica definida de uma relação como igualdade, podemos defini-la em termos de associação como tal:

xy ( z (z x z y) x = y)

Um bom aviso: a curva de aprendizado para isso é realmente muito acentuada. Se você pretende fazer isso, pode se encontrar vários anos antes de entender o problema completo, como foi minha experiência. Você pode examinar a teoria de uma abordagem menos fundamental antes de assumir a enorme tarefa de incorporá-la em uma linguagem básica para tudo. Afinal, você não precisa necessariamente raciocinar sobre conjuntos incontáveis ​​de genes misturados.

dezakin
fonte
1
Muito obrigado por esta resposta detalhada e esclarecedora! Algumas perguntas: 1. A Wikipedia afirma que 'o esquema axiomático de substituição não é necessário para as provas da maioria dos teoremas da matemática comum' e que não era um dos axiomas originais de Z (foi adicionado por F). É possível que meus teoremas possam ser comprovados sem ele, negando assim a necessidade de NBG? Obviamente, suponho que nenhum provador de teoremas automatizado permitiria o uso de {ZFC - esquema de substituição do axioma}, se isso fosse possível?
Atriya
2. Dado que a lógica de primeira ordem + a teoria dos conjuntos é melhor para fundações, presumo que HOL / Isabelle / PVS / etc (todas de ordem superior) são um exagero para o meu propósito? Além disso, tudo baseado na teoria dos tipos (Coq et al.) Não é apropriado? Assim, gostos de Prover9 / Vampire / SNARK seriam apropriados? Eu tenho alguma experiência anterior com SNARK. Ele pode lidar com lógica de primeira ordem de várias classificações com igualdade, por resolução, mas não sei como representar a teoria dos conjuntos nela.
Atriya
1
Os provadores de teoremas automatizados podem usar esquemas de axioma, mas dificulta a implementação. Prover9 não os suporta. HOL, Isabelle, Coq apoiam a teoria dos conjuntos de primeira ordem, tanto quanto me lembro, e provavelmente são perfeitamente adequadas para o seu projeto. Mesmo que você possa incorporar outras teorias no NBG, isso não é absolutamente necessário. Não precisamos incorporar a aritmética Peano no NBG para provar coisas sobre números ... mas ajuda a aprender e entender a estrutura lógica.
dezakin
Você sempre pode incorporar sua teoria na teoria dos conjuntos posteriormente, definindo os predicados da teoria em termos do predicado de associação. Eu não me preocuparia em tornar seu projeto absolutamente fundamental imediatamente. Pode ser encaixado mais tarde.
dezakin
Parece então que virtualmente qualquer provador - mesmo os diferentes de Coq, HOL e Prover9 - pode ser usado para o meu projeto. Nesses casos, o que seria uma estratégia de decisão inteligente? Não estou familiarizado com tudo, exceto SNARK. O "ideal" é a descoberta de novos teoremas no sistema axioma fornecido.
Atriya
8

Vários pontos:

  1. Até onde eu sei, o Principia Mathematica usa essencialmente uma formalização da teoria dos conjuntos usando uma lógica de primeira ordem digitada. Portanto, seria tentador usar um provador de teoremas automatizado de primeira ordem como o Prover 9 ou possivelmente o ACL2 para formalizar suas declarações. No entanto, estou vendo várias construções da teoria dos conjuntos (como , ), que geralmente não funcionam muito bem com o ATP de primeira ordem., ,

  2. Qualquer assistente de prova interativo moderno certamente terá a expressividade para formalizar e provar suas declarações, como sugeriu Andrej. De fato, uma vez que parece haver algumas afirmações incluindo aritmética, seria aconselhável usar um sistema como Isabelle , Coq ou HOL que já possui teorias extensas para tratar afirmações aritméticas. Minha ênfase no moderno não é uma coincidência: grandes avanços na usabilidade foram feitos desde a Automath, e eu sinceramente acho que você faria um desserviço usando algo que não foi desenvolvido ativamente desde os anos 90 (se você pudesse conseguir um trabalhar!)

  3. Finalmente, ITP e ATP têm curvas de aprendizado bastante desafiadoras, e você não deve esperar poder inserir esses teoremas em um sistema como se estivesse escrevendo uma prova de . Espere frustração severa e perda de tempo, principalmente nos primeiros meses (sim, meses). Definitivamente, você precisa trabalhar com alguns tutoriais antes de chegar à formalização principal.LATEX

cody
fonte
Obrigado! Esse é o tipo de conselho geral que eu estava procurando. Marcando esta resposta como aceita. Provavelmente terei perguntas mais específicas / técnicas à medida que progredir.
Atriya
A teoria dos conjuntos é feita para a lógica de primeira ordem. Você pode reduzir toda a matemática a uma teoria de primeira ordem com apenas um predicado: associação. A partir daí, você pode construir definições de união, interseção, subconjunto, subconjunto apropriado e outras relações. Prover9 é totalmente apropriado.
21414 Dejankin
Em teoria? Sim. Na prática? Se você definir, digamos, os números naturais usando a teoria dos conjuntos, um sistema como o Prover9 não seria capaz de provar as declarações mais básicas, como a ordenação total de . Por natureza, sistemas como a teoria dos conjuntos exigem que várias heurísticas específicas sejam tratadas com eficiência pelos sistemas ATP. N
Cody
Prover9 usa construções teóricas definidas dos números naturais frequentemente. Verifique os problemas da teoria dos números e axiomas da teoria dos números no TPTP. Eles definem a teoria dos números como definições da teoria dos conjuntos. As heurísticas exigidas pelo ATP para os provadores de teoremas de resolução são justamente qual cláusula escolher para a lista utilizável ao procurar a cláusula vazia, e a teoria dos conjuntos não é uma exceção especial a isso. Outras teorias são definidas na teoria dos conjuntos por predicados relacionais.
dezakin