El mié, 11 de oct. de 2023 2:01 p. m., Juan Carlos Agudelo Agudelo < [email protected]> escribió:
> > On Tue, Oct 10, 2023 at 9:50 PM Joao Marcos <[email protected]> wrote: > >> Hummmm... E quem vem primeiro? Uma dada semântica para uma teoria de >> > primeira ordem com igualdade será correta/sound para uma lógica que >> tem (∃x)x=x como teorema sse ela exigir que os domínios das >> interpretações sejam não vazios. Não podemos pensar, assim, que esta >> é a _razão_ pela qual a lógica clássica faz esta bendita pressuposição >> sobre a não-vacuidade dos domínios? Numa lógica que não seja >> constrangida por tal pressuposto existencial o "normal" não seria que >> os domínios das estruturas de interpretação fossem conjuntos >> arbitrários? >> > > Sim dúvida, o fato da lógica de primeira ordem com igualdade poder > demonstrar (∃x)x=x, obriga a que a semântica considere só modelos com > domínios não vazios. > E nem se precisa ter igualdade, pois (∃ x)(P(x) → P(x)), para qualquer > fórmula P(x), também leva à necessidade de modelos com domínios não vazios. > O estraño é porque as lógicas de primeira ordem (clássica, intuicionista, > etc) permitem demonstrar este tipo de teoremas. De alguma maneira, a > exigência da existência de objetos nessas lógicas está implicitamente > estabelecida através dos axiomas e regras de inferência. A pergunta é: > onde?, e não tenho resposta para isso. (Na sessão que mencionei do livro do > Mendelson, ele propõe um sistema axiomático para lógica de primeira ordem, > cuja semântica permite domínios não vazios, mas ainda não compreendo bem > onde que está a "solução" para permitir interpretações em domínios vazios). > > Acho interessante que nas teorias de tipos isso não acontece: por exemplo, > na prova da correspondência Curry-Howard para o sistema de tipos puros λ > P, com a "lógica minimal intuicionista" (o fragmento da lógica > intuicionista de primeira ordem só com implicação e quantificador > universal), tem que se adicionar explicitamente o suposto de que os > domínios são não vazios, para poder obter a correspondência. Isso mostra, > que a formalização da lógica de primeira ordem em teoria de tipos admite > domínios não vazios (ver em > https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf, p. 142). > > >> Quando uma dada teoria tem um símbolo de constante qualquer, a >> semântica "standard" poderá justificar: aí está a razão, precisamos de >> um objeto no domínio para interpretar este símbolo de constante. Mas >> neste caso esbarramos em outra pressuposição da semântica "standard", >> a saber, a pressuposição de que as funções de interpretação sejam >> totais (e isto se aplica em particular à operação nulária que >> interpreta o dito símbolo de constante). Como o Henrique já apontou, >> aqui esbarramos na pressuposição de que "todos os termos denotam". >> Mas será que a gente já não sabe, tendo em vista todo o trabalho feito >> nos últimos anos formalizando a noção de *computabilidade*, que no >> mundo real não dá para escapar de _funções parciais_ (que >> eventualmente farão com que alguns termos não denotem)? >> > > Alguns desses problemas técnicos são abordados no capítulo de Mendelson, e > em https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf, p. 142, há > duas referências a trabalhos sobre "free logic". > > Abs, > Juan Carlos > -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- 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 ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CACkoYSqUphHsikLtWA91jY0rDhzp7%2BvOvsd2PR4SWmv018KjMw%40mail.gmail.com.
