arXiv Computer Science AIPruebas sin nominales: El argumento ontológico de Gödel, su incrustación superficial y las preguntas abiertas de las Notas del Monatshefte
Resumen del corpus
El texto aborda la incrustación superficial de la lógica modal de orden superior en la lógica modal de orden superior clásica, utilizando el argumento ontológico de Gödel y Scott. Se discuten las preguntas abiertas de las Notas del Monatshefte y cómo se resuelven sin nominales. Se verifica la validez de los teoremas en Isabelle/HOL y Lean 4.