Método de forçamento usado no papel de relativização de Baker-Gill-Solovay e na prova de independência de hipóteses de Cohen por prova de continuidade

15

Em geral, estou interessado no método de forçar usado por Baker-Gill-Solovay e Cohen. Estou procurando o maior número possível de fontes sobre a própria técnica ou seu uso. Alguém tem sugestões?

djkern
fonte
1
quem ressalta que é a mesma técnica?
vzn

Respostas:

17

Para mais usos de forçar (via chamados oráculos genéricos) na teoria da complexidade, consulte O Oracle Builder's Toolkit ( disponível gratuitamente na página inicial da Fortnow ) por Fenner, Fortnow, Kurtz e Li. Eles dão uma teoria geral dos oráculos genéricos e mostram suas muitas aplicações em complexidade.

Se você estiver interessado em saber como os oráculos em complexidade são como provas de independência na teoria dos conjuntos, você pode estar interessado nos seguintes artigos:

Para os usos de forçar na teoria dos conjuntos, consulte o livro Teoria dos Conjuntos ( Teoria dos Conjuntos na Amazônia ), de Jech, especialmente as Partes II e III do livro (não confunda com "Introdução à Teoria dos Conjuntos", de Hrbáček e Jech).

Joshua Grochow
fonte
9

Para usos de forçar técnicas semelhantes na complexidade da prova, você pode querer considerar:

O método de prova é um análogo aritmético de forçar (do tipo já usado por Paris e Wilkie). Mais combinatórios (e limites inferiores melhorados) estão em J. Krajıcek, P. Pudlak e A. Woods, limites inferiores exponenciais ao tamanho das profundidades limitadas Provas de Frege do princípio do pombo , Random Structures Algorithms, 7 (1995), pp. 15-39. e T. Pitassi, PW Beame e R. Impagliazzo, Limites inferiores exponenciais para o princípio do buraco de pombo , Comput. Complexidade, 3 (1993), pp. 97-140.

Veja também:

Recentemente, Jan Krajicek publicou um livro que unifica essas técnicas de forçamento:

Iddo Tzameret
fonte
salto interessante, mas nunca vi alguém nos papéis / livros comparar o forçamento com o princípio / provas ...
vzn
Princípio do buraco de pombo aqui é o nome de uma declaração. Para mostrar que a afirmação é independente de uma certa teoria, usamos construções semelhantes a forçantes. As referências acima mostram como fazer isso.
Iddo Tzameret
ok, mas as provas de tamanho exponencial do SAT usando resolução (via construções de pombos) não são "independentes", ao que parece ... são apenas "grandes" ... quaisquer referências on-line apontando a conexão? admitir sou um pouco surpreso porque muitas refs em provas classificar em SAT não se referem a qualquer coisa sobre "forçando" ....
vzn
1
Estabelecer limites inferiores de tamanho super-polinomial em provas proposicionais para uma família (uniforme) de declarações proposicionais implica a independência da fórmula correspondente de primeira (ou segunda) ordem na teoria formal de primeira (ou segunda) ordem correspondente. Por exemplo, o princípio do pigeonhole é independente (isto é, verdadeiro no modelo padrão, mas improvável) deV0 0, ou seja, a teoria de "UMAC0 0raciocínio "que corresponde a Frege de profundidade constante (isso NÃO é resolução); (eu uso aqui a terminologia de Cook & Nguyen, Fundação Lógica de Complexidade de Prova, 2010; ver Cor. VII.2.4 lá).
Iddo Tzameret
1
(cont.) Veja também o livro de Jan Krajicek "Aritmética limitada, lógica proposicional e teoria da complexidade", Cambridge, 1995, sobre isso. Todas as referências acima (excluindo o livro de Krajicek de 1995) estão disponíveis on-line. A conexão com o forçamento é explicada, por exemplo, na 2ª referência de Ajtai acima.
Iddo Tzameret
4

veja também Forcing in proof theory por Avigad, 30pp, 2004. ele cita BGS75, mas não em detalhes. há alguma referência a Scott / Solovay como uma reformulação do forçamento para modelos com valor booleano.

As idéias no forçamento influenciaram a complexidade computacional; por exemplo, a separação de classes de complexidade relavitizadas para um oráculo (por exemplo, como no BGS75) geralmente pode ser vista como versões de forçamento com recursos limitados.

vzn
fonte