¿Cómo llamas a una afirmación que se acepta como verdadera pero nunca se ha probado?

¿Cómo se llama un enunciado P que nunca ha sido probado formalmente pero que todas las observaciones hasta ahora lo verifican?

Esta pregunta surge de este escenario: algunas personas usan un software para trabajar. A menudo utilizan una función específica. Cuando se diseñó esta función, los desarrolladores temían que pudieran ocurrir algunos errores. Sin embargo, estos errores nunca ocurren y los trabajadores lo han usado durante años. Por supuesto esta función funciona correctamente, porque nunca ha fallado. Sin embargo, ningún desarrollador se ha tomado el tiempo de entender cómo.

En este ejemplo, P es la afirmación " esta función no tiene errores ".

una conjetura Ver la conjetura de Fermat antes de 1994.
Informalmente, podrías referirte a él como una 'posibilidad'.
No está claro lo que está preguntando ahora, después de su edición. La afirmación "esto siempre ha funcionado aunque no sabemos cómo" es simplemente cierta (confiando en su palabra). Entonces, ¿a qué afirmación te refieres cuando dices "afirmación que nunca ha sido probada"? ¿Quieres preguntar: cómo llamamos a una situación en la que no sabemos cómo funciona algo?
@EliranH Alberto está describiendo una inducción. "No sabemos con certeza si el software seguirá funcionando, porque no podemos demostrar que lo hará, pero siempre ha funcionado en el pasado, así que creemos que seguirá funcionando". La afirmación no comprobada es que seguirá funcionando .
¿Qué significa "esta funcionalidad"? ¿No querrás decir "este programa"? La prueba se trata de proposiciones/programas, no de funcionalidad.
@mobileink Lo siento, escribo "funcionalidad", pero quiero escribir "función" (un programa es una función).
Ah, pero los programas no son realmente funciones, son procedimientos que representan o aproximan fns. La prueba de un programa, funcional o no, se trata de la implementación, que es un texto específico. Lamento ser tan quisquilloso, pero esta es una buena pregunta que toca muchas cosas, así que cuanto más precisos podamos ser, mejor.
sugerencia: "La implementación de esta función está libre de errores". Un fn dado podría tener muchas implementaciones.

Respuestas (6)

Depende en parte del área temática en la que se encuentre la declaración y cómo ha sido respaldada por hechos (p. ej., simplemente no contradicha aún frente a rigurosamente probada y corroborada). Construyendo a partir de los comentarios:

Puede llamar a esto una conjetura si se relaciona con las matemáticas o la lógica, o si aún no se ha corroborado bien.

En ciencia se llamaría una hipótesis .

Un término más general sería una posibilidad [epistémica] . Tenga en cuenta que es epistémico porque estamos hablando de evidencia y formas en que podemos saber que algo es cierto; La modalidad no es realmente relevante.

Editado después de la pregunta:

Su ejemplo es interesante porque no parece encajar perfectamente en los términos que se han sugerido. Yo diría que este es un caso más general de una afirmación inductiva ("Siempre funcionó en el pasado, por lo tanto, seguirá funcionando"). Podrías llamar a la conclusión de que seguirá funcionando una inducción . Esto sigue el patrón de referirse a una conclusión deducida como una deducción .

Sócrates es sabio, y Sócrates es un hombre. Mi deducción es que algunos hombres son sabios.

Cada vez que he dejado caer una manzana cerca de la superficie de la tierra, ha caído hacia abajo. Mi inducción es que seguirá haciéndolo en el futuro.

Este es un uso un poco inusual, lo admito, pero creo que se adapta mejor a su situación.

Gracias por la respuesta. Vea mis ediciones si necesita aclaraciones.
@Alberto He editado mi respuesta con otra sugerencia.
Gracias @Era, el ejemplo de Apple es exactamente lo que estaba tratando de decir. Creo que la inducción encaja en mi caso.
Gracias @Era, encontré que "conjetura" era la palabra correcta

Dado que su pregunta se refería al software, aquí hay una respuesta relacionada con el software: el software que se usa en producción durante años y aún no ha fallado se llama confiable o maduro .

Esto no hace ninguna suposición sobre su corrección real. Ambos términos solo dicen que ha funcionado hasta ahora en el mundo real, no que se haya demostrado que es correcto bajo ninguna circunstancia.

Por supuesto esta funcionalidad es correcta, porque nunca ha fallado

Esta es una conclusión inválida. El hecho de que aún no haya fallado no significa que no lo hará en el futuro. No podemos estar seguros.

Hay formas de probar que ciertas propiedades se mantienen bajo ciertas condiciones, y eso se hace rigurosamente en software crítico. Se espera que algunas piezas de software, como el sistema operativo VxWorks, tengan solo un BSOD cada 30 años.

Para la situación de software específica que está describiendo, eche un vistazo a Hoare Logic, como se explica, por ejemplo, en https://en.wikipedia.org/wiki/Hoare_logic

En este modelo, la corrección de su programa está determinada por una colección de Hoare Triples de la forma {P}C{Q} , donde {P} = condiciones previas/entrada, C = su_programa, {Q} = condiciones posteriores/salida. Dada la entrada que satisface cualquiera de las condiciones previas prescritas, si la salida de su programa satisface las condiciones posteriores correspondientes, entonces es "correcto".

Como ejemplo simple, supongamos que C =programa_para_agregar_dos_números. Entonces un Hoare Triple podría ser {P}C{Q} , donde {P} =ambos_números_a_agregar_son_impares, y {Q} =la suma_es_par. Obviamente, ese Hoare Triple por sí solo no establece la corrección de C. Pero una colección apropiada de Hoare Triples por lo general lo hace. ("Por lo general" significa siempre que existe una colección de Hoare Triples que únicamente, en un sentido de si y solo si, especifica la función : entrada-->salida a calcular).

Y es posible que desee consultar algunos de los enlaces "Ver también" en la parte inferior de ese artículo de wikipedia para conocer otros modelos de corrección del programa. Como puede imaginar, la informática ha dedicado mucha investigación rigurosa a este tema.

editar: gracias, @JamesKingsbery Con respecto a su comentario de "término para este concepto", sí, debería haber mencionado explícitamente que puede buscar en Google el término "corrección del programa" para obtener mucha información adicional.

¡Bienvenido a Philosophy.SE! Gran respuesta a la pregunta, ¡no sabía que había un término para este concepto!

Según entiendo el uso estándar, una oración formalmente demostrable es un teorema, por lo que "P es un teorema" dice que P es verdadero y que la afirmación de que P es verdadero es justificable mediante prueba deductiva. Se propone una conjetura como verdadera, pero sin justificación formal, ni deductiva ni inductiva. Las afirmaciones empíricas nunca son formalmente comprobables, por lo que sus justificaciones son inductivas o abductivas. Esto es cierto incluso para las "leyes"; por ejemplo, la Ley de Ohm no es el tipo de cosas que pueden probarse formalmente. Lo mejor que podemos hacer es realizar muchos experimentos, observar que nunca falla e inferir (¿inductivamente? ¿abductivamente?) que debe ser cierto. Entonces lo llamamos una teoría (sobre el mundo natural).

Creo que su caso de uso es fundamentalmente diferente. Normalmente no llamamos teoremas a los programas, aunque podríamos hacerlo si comprobamos que son correctos. Lo más probable es que los llamemos "certificados" o similares. Un programa del que no se ha probado formalmente que es correcto, pero que nunca ha fallado, no es realmente como una teoría empírica, porque no es un artefacto natural. Tal programa podría, en principio, demostrarse que es correcto o incorrecto, a diferencia de una afirmación empírica.

Sugeriría basarse en la ingeniería en lugar de la lógica, y llamar a tales programas confiables . Esto tiene la ventaja de eliminar la noción de verdad, que es un tema filosófico sin relevancia para la ingeniería. También tiene una buena definición estadística formal con la que no los aburriré, y está relacionada con nociones como robustez, ya que la justificación de las afirmaciones de confiabilidad implicará variaciones: si su código se ha estado ejecutando durante 10 años sin errores, pero siempre con la misma entrada, entonces puede ser confiable para esa entrada, pero no tiene idea de qué tan robusto es, es decir, si es confiable en diferentes condiciones.

Se llaman afirmaciones aceptadas "sobre la fe", "sobre la confianza" o "con reservas". Un ejemplo de esto es la afirmación: las buenas personas van al cielo. La credibilidad de esta declaración depende más de la credibilidad de (la confianza en) la persona que la hace, que de la declaración misma.

Con respecto a los programas/funciones de software en particular, esto es algo completamente diferente. Un programa está hecho por una persona, por lo que si un programa funcionará "siempre", en "todas las condiciones posibles", depende de cuán minuciosamente el programador cubrió todas esas posibilidades de error y cuán minuciosamente el departamento de pruebas hizo su trabajo. . Obviamente, cuanto más minuciosas se hayan realizado estas actividades, menos probable es que el programa fracase. Sin embargo, la alta probabilidad de "errores humanos" hace que sea imposible garantizar que cualquier programa (o función) en particular funcionará siempre en todas las condiciones. Por lo tanto, la afirmación "esta función está libre de errores" debe ir precedida de "hasta ahora,esto...", para convertirlo en una afirmación "sensata" (una afirmación que tenga sentido).

¿Una afirmación que se acepta como verdadera pero que nunca ha sido probada? En matemáticas lo llamarías "incorrectamente aceptado como verdadero".

Incluso en el desarrollo de software, donde los estándares serán más bajos, nadie en su sano juicio llamaría a ningún software "libre de errores". Es posible que escuche que el software "no tiene errores conocidos" o "no tiene defectos informados".