¿Cuántos subobjetivos genera demostrar P∧Q por introducción?
Uno por cada componente.
La regla de introducción de la conjunción requiere evidencia de cada componente.
Aplicada a P∧Q abre el objetivo P y el objetivo Q en el mismo contexto.
Son 2 subobjetivos; resolver solo uno no termina la prueba.
¿Una prueba verificada depende de los axiomas declarados? Responde sí/no.
El núcleo verifica derivaciones relativas a un entorno.
El núcleo comprueba que el término tiene el tipo afirmado según las reglas y el entorno cargado.
Si ese término usa un axioma, la conclusión depende de él, directamente o a través de teoremas importados.
Por tanto sí: la garantía es relativa a los axiomas declarados, cuya dependencia conviene revisar.
¿Cuántos casos base tiene la inducción ordinaria en naturales desde 0?
Se separa base y paso.
La inducción ordinaria desde 0 separa la base P(0) del paso general P(n)→P(n+1).
El paso debe justificarse para un n arbitrario y no constituye otro caso base.
Formaliza en palabras la prueba de P→P.
Introduce una hipótesis del antecedente.
En el contexto ampliado la conclusión que queda por demostrar es P.
La hipótesis h la demuestra directamente. Al descargarla se obtiene la implicación, representada por la identidad λh.h.
Propón dos propiedades para especificar una función que ordena listas.
Ordenar no debe perder datos.
Fijamos el tipo de elementos y la relación con la que se quiere ordenar.
Primera propiedad: la lista de salida está ordenada según esa relación.
Segunda propiedad: la salida es una permutación de la entrada y conserva multiplicidades. Devolver [] para una entrada no vacía pasa la primera prueba, pero falla la segunda.