Prezado Samuel, Você teria que procurar um enunciado que não seja absoluto para o universo construtível L. De fato, temos o seguinte resultado, já aludido em uma das respostas nesse link que você enviou:
- Se S é um enunciado absoluto para L em ZF, e S é demonstrável em ZFC, então S é demonstrável em ZF. Dem.: Se S é teorema de ZFC, então ZF demonstra que S vale no universo construtível L, pois ZF demonstra que L satisfaz todos os axiomas de ZFC. Mas S é absoluto para L, ou seja, ZF demonstra que "L satisfaz S é equivalente a S". Portanto, ZF demonstra S. Fim. Não há nada especial com o axioma da escolha no resultado acima, apenas usamos que ZF demonstra que este axioma vale em L. O mesmo se aplica, por exemplo, para GCH, que é mais forte que AC: Se S é demonstrável em ZF + GCH, então S é demonstrável em ZF. Você poderia usar até mesmo V=L para demonstrar S, pois ZF + V=L é conservativa sobre ZF para enunciados absolutos para L em ZF. Se assumirmos (bastante razoável) que qualquer enunciado da teoria da computação pode ser codificado na aritmética de segunda ordem, então você teria que procurar exemplos que sejam pelo menos Delta^1_3 na hierarquia analítica, pois os enunciados Sigma^1_2 ou Pi^1_2 em ZF são absolutos para L em ZF. Não parece fácil encontrar exemplo de interesse da teoria da computação que não seja Sigma^1_2 ou Pi^1_2 em ZF. Abraço Rodrigo -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAExWzU%2BuLaWJBTSaypNG0FF%2Ba%3DKE_SrKQ8uOOVGVRSMKaeu%3Dig%40mail.gmail.com.
