Antes de cerrar un universo, alguien debe decidir qué entra en él

Pregunta editorial¿Qué prueba una formalización que toma como dado el perímetro cuya elección era el problema?
Reflexión del diálogoEn varios turnos Iván persigue una distinción difícil. Concede que una matemática rigurosa puede fijar un universo formal, establecer axiomas y decidir sobre clases concretas de objetos. Pero pregunta quién realiza la tarea previa de reconocer qué entradas del mundo corresponden a ese universo. Cuando su interlocutor intenta resolver el problema diciendo «basta con definir el conjunto de entradas», él vuelve a preguntar cómo se reconoce esa pertenencia en la práctica.

La frase es explícita: «somebody, some way, has to discriminate this single set of entries». Su crítica no necesita negar la coherencia de un sistema formal; señala la diferencia entre una propiedad asumida dentro de la formulación y el trabajo de conectar esa formulación con entradas y situaciones reales. En una empresa es el paso entre un dato tipado en un sistema y la realidad de la que se supone que procede.

Aquí deben evitarse dos extrapolaciones. Primero, no toda elección de dominio requiere una máquina universal: existen validadores locales efectivos y decidibles. Segundo, afirmar que hay un acto humano anterior no demuestra que la teoría axiomática incurra por ello en contradicción. La ficha conserva una pregunta de responsabilidad de frontera: ¿quién eligió el marco, con qué conocimiento, para qué casos, y cómo se reconocerá que deja de corresponder al mundo?