Resultados no CS teórico independente do ZFC

37

Vou fazer uma pergunta bastante vaga, já que nem sempre é fácil distinguir a fronteira entre a teoria da computação e a matemática.

PERGUNTA: Você tem conhecimento de algum resultado interessante no CS que seja independente do ZFC (isto é, teoria dos conjuntos padrão) ou que foi originalmente provado no ZFC (+ algum outro axioma) e somente posteriormente comprovado no ZFC?

Estou perguntando porque estou perto de terminar minha tese de doutorado, e meu principal resultado (a determinação de uma classe de jogos que são usados ​​para dar "semântica de jogos" a um modal probabilístico -calculus) está comprovado no momento no ZFC estendido com outros axiomas (ou seja, a negação da hipótese de Continuum e, Axiom Martin ).¬ C H M Aμ¬CHMA

Portanto, a configuração é claramente Ciência da Computação (o modal -calculus é uma lógica temporal, e eu a estou estendendo para trabalhar com sistemas probabilísticos).μ

Gostaria de citar na minha tese outros exemplos (se você tiver conhecimento de algum) desse tipo.

Agradeço antecipadamente,

tchau

Matteo

IamMeeoh
fonte
9
Essas perguntas anteriores podem ser úteis: cstheory.stackexchange.com/questions/4816/… cstheory.stackexchange.com/questions/1923/…
Mark Reitblatt
9
Eu estava indo para resposta que Matteo Mio e Alex Simpson usado Axiom de Martin para provar resultados muito interessantes ...
Andrej Bauer
7
Este pode ser o melhor exemplo que eu já vi de uma pergunta cuja melhor resposta está contida na própria pergunta! Eu não sabia do seu resultado muito interessante.
Timothy Chow

Respostas:

19

Embora eu não esteja ciente de tais resultados, além dos seus, acho que você poderia ampliar um pouco o escopo e perguntar: que resultados no TCS foram provados usando (qualquer tipo de) axiomas não-padrão. Por não padrão aqui, quero dizer algo diferente da lógica clássica com ZF (ou ZFC).

Um belo exemplo do tipo de trabalho que tenho em mente são os resultados de Alex Simpson sobre propriedades de linguagens de programação usando a teoria de domínio sintético. Ele usa a teoria dos conjuntos intuicionistas com axiomas que contradizem a lógica clássica.

Além disso, Alex e eu usamos axiomas intuicionistas com princípios de continuidade anti-clássicos para mostrar resultados sobre a computabilidade de Banach-Mazur.

No entanto, nenhum dos exemplos mencionados possui um status "aberto", como suas provas, porque sabemos que os axiomas não-padrão que usamos podem ser entendidos simplesmente como trabalhando dentro de um modelo de matemática intuicionista, onde o modelo pode existir. no ZFC. Portanto, a configuração não padrão é realmente uma maneira de fazer as coisas com mais elegância e, em princípio, elas podem ser feitas no ZFC direto (embora eu tenha medo de pensar em como exatamente isso seria).

Andrej Bauer
fonte
Obrigado! Vou perguntar a alex mais detalhes sobre isso quando escreverei a introdução.
IamMeeoh 08/04
13

Depende da sua definição de "Ciência da computação". Veja o exemplo abaixo - isso conta?

A codificação dos inteiros é um código binário exclusivamente decodable de . Se o comprimento das palavras de código não for decrescente, chamamos o código de monotônico . Um código C 1 é melhor que um código C 2 se | C 1 ( n ) | - | C 2 ( n ) | - . Em outras palavras, para cada G , a partir de algum ponto sobre as palavras de código de C 1 são, pelo menos, L bits de mais curto.NC1C2|C1(n)||C2(n)|LC1L

Um conjunto de códigos é chamado Cofiñal se para cada código C não é um código D S que é melhor do que C . É bem ordenado se for bem ordenado em relação a "melhor". Uma escala é um conjunto de códigos cofinais bem ordenados.SCDSC

Aqui estão duas propriedades que são independentes do ZFC:

  1. Existe uma escala de códigos.
  2. Existe uma escala de códigos monótonos (isto é, um conjunto bem ordenado de códigos monótonos, que é fundamental no conjunto de todos os códigos monótonos).
Yuval Filmus
fonte
Olá Yuval, obrigado pela resposta. Não sei se o seu exemplo se encaixa na minha definição "Ciência da computação". Certamente falar sobre "códigos" não é suficiente para classificá-lo como CS. O que torna um artigo "um artigo de CS" imho é o seguinte: Ele apareceu em alguma conferência / revista de CS ou foi usado para provar algum resultado na conferência / jornal de CS? pelo artigo da CS, sou bastante flexível, mas os tópicos podem ser "teoria da informação, complexidade, lógica de programas / sistemas, teoria da recursão" etc. De qualquer forma, você pode citar a fonte do exemplo e / ou documentos que fazem uso de "existe uma escala de códigos "? Obrigado! Tchau
IamMeeoh
11
Trabalhos sobre códigos de números inteiros aparecem em periódicos de engenharia elétrica, como as transações do IEEE sobre teoria da informação. Isso atinge uma das suas palavras-chave.
Yuval Filmus
11
Eu não acho que exista algum papel usando esses resultados. Além disso, acredito firmemente que um resultado independente do ZFC não tem utilidade na complexidade; portanto, em certo sentido, sua pergunta é sobre estender os limites do que é considerado ciência da computação.
Yuval Filmus
11
Olá Yuval, antes de tudo, deixe-me agradecer novamente pelas respostas. Eu não concordo com sua posição forte no entanto. Por exemplo, o teorema de Robertson-Seymour (que parece exigir escolha) tem consequências importantes na complexidade. Portanto, está claro que a escolha é útil (talvez um pouco surpreendente) na teoria da complexidade. Agora, trabalhar com extensões consistentes do ZFC obviamente simplifica a tarefa de provar, por exemplo, resultados de complexidade, mesmo que esses resultados sejam prováveis ​​no ZFC, mas ninguém sabe como ainda.
IamMeeoh
11
Além disso, não vejo por que não deveria haver resultados concretos na complexidade independente do ZFC, da mesma forma que o teorema de Robertson-Seymour é (talvez) independente do ZF.
IamMeeoh
9

Um cone de graus de Turing é um conjunto de graus com alguma base b D de tal modo que para todos os graus C , b t c se e somente se c D .DbDcbTccD

A declaração da determinação do grau de Turing :

Todo conjunto de graus de Turing contém um cone ou é separado de algum cone

é uma conseqüência do axioma da determinação (AD), que é independente da ZF e incompatível com a ZFC. A declaração mais fraca

Todo conjunto de reais Borel fechado sob a equivalência de Turing contém um cone ou é separado de um cone

é uma conseqüência do teorema de Martin sobre a determinação de Borel, que é comprovável no ZFC. Ambas as afirmações foram estudadas antes da comprovação do resultado de Martin sobre a determinação de Borel, quando era sabido apenas que ambas eram prováveis ​​em ZF + AD.

SbcSbTcSS

Carl Mummert
fonte
0

Muita matemática construtiva. Veja o trabalho de Per Martin-Löf sobre teoria dos conjuntos construtiva, usada como base para linguagens de programação tipicamente dependentes.

Roubar
fonte
6
A IIRC, teoria do tipo Martin-Lof, tem a mesma força de consistência que a teoria dos conjuntos de Kripke-Platek, que é muito mais fraca que a ZFC. Além disso, o MLTT não possui princípios explicitamente anti-clássicos, como os axiomas de continuidade mencionados por Andrej.
Neel Krishnaswami
@ Neel Eu nunca disse nada sobre consistência ou força do MLTT. No entanto, considero que alguns resultados em matemática construtiva são relevantes para a questão, solicitando "resultado interessante no CS, que é ... independente do ZFC".
Rob
5
Suponho que "independente" aqui seja entendido no sentido formal.
Re