¿Cuántas componentes exige probar P∧Q?
Una por proposición.
La conjunción P∧Q exige una prueba de P y una de Q.
Cada una ocupa una componente de su constructor.
Se necesitan2 componentes.
¿Un mensaje convincente de IA equivale por sí solo a prueba formal comprobada? Sí o no.
Distingue proponer y verificar.
Una salida de IA es una propuesta de texto o de término.
Debe ser aceptada para el enunciado y contexto correctos por el comprobador pertinente.
La respuesta es no: la apariencia convincente no equivale a prueba formal comprobada.
¿Añadir la conclusión como axioma demuestra que se deduce de las hipótesis originales? Sí o no.
Se ha cambiado el contexto lógico.
Al añadir la conclusión como axioma, se introduce una hipótesis nueva.
La aceptación posterior puede depender precisamente de ese supuesto.
La respuesta es no: eso no demuestra deducción desde las hipótesis originales.
¿Debe comprobarse que el enunciado formal representa la pregunta original? Sí o no.
Un comprobador puede aceptar una afirmación distinta.
El núcleo comprueba el enunciado que recibe, con sus tipos y definiciones.
Ese enunciado podría representar mal la pregunta informal.
La respuesta es sí: se revisa la fidelidad además de la aceptación del término.
Describe una auditoría de una prueba formal generada por IA.
Incluye enunciado, dependencias y configuración.
Revisaría dominio, tipos, cuantificadores, definiciones y todas las hipótesis frente al problema original.
Comprobaría el término sin omisiones e inspeccionaría axiomas, dependencias y componentes adicionales de confianza.
Guardaría archivos, versión, bibliotecas y procedimiento para repetir la comprobación, manteniendo una explicación matemática legible.