¿Prueba de la regla de absorción en lógica proposicional?

Sé que hay una "prueba formal" para la "regla de absorción" que emplea la "ley del tercero excluido". Se presenta en Wikipedia (y creo que es de Russell): https://en.wikipedia.org/wiki/Absorption_(logic)#Formal_proof .

También es obvio cómo podría hacerse por medio de una prueba "condicional" o "indirecta".

Sin embargo, ¿existe una "prueba formal" en lógica proposicional para la "regla de absorción" que NO afirme la "ley del medio excluido (o de no contradicción)" como una regla de inferencia o emplee una "regla condicional (o indirecta)"? prueba"?

Es decir, ¿puede construirse una "demostración formal" en lógica proposicional (deducción natural o no) que vaya de la premisa p⊃q a la conclusión p⊃(p∙q) SIN usar la "ley del tercero excluido (LEM )" como regla de inferencia o empleando una "prueba condicional (CP)" o "prueba indirecta (IP)"?

Por curiosidad y considerando que no está aceptando la respuesta usando una tabla de verdad, ¿cómo define la operación funcional de verdad de un condicional para los propósitos de su pregunta? (normalmente se hace con una tabla de verdad)
No es que no acepte la respuesta. Por supuesto, una tabla de verdad nos muestra no solo que pasar de p⊃q a p⊃(p∙q) es válido, sino que además p⊃q y p⊃(p∙q) son declaraciones equivalentes (lo que hace que Copi aplique la absorción como una regla de implicación curiosa, pero estoy divagando). En pocas palabras, solo quiero saber acerca de su prueba en la llamada deducción natural, y si se puede hacer o no sin CP o LEM (parece que no puede ser, lo cual es revelador con respecto a la aplicabilidad de la absorción en la lógica filosófica). ¡Eso es todo!
Creo que estás malinterpretando mi comentario anterior. Intentaré volver a expresarlo. (1) la función p⊃q normalmente se define mediante una tabla de verdad ( en.wikipedia.org/wiki/Material_conditional ). Como en, p⊃q es precisamente la función que produce la salida que dicta la tabla de verdad. (2) la respuesta a continuación usa la tabla de verdad para derivar p⊃(p∙q). (3) se opone a responder ya que la tabla de verdad presupone bivalencia y/o LEM. (4) ¿No se seguiría que su objeción también se aplica a la definición de p⊃q?
Dicho de otra manera, si (3) es un problema, ¿entonces (1) no lo es también? Y si (1) no es un problema, entonces (3) tampoco parece serlo... Entonces parece que debería dar una definición de p⊃q que no sea una tabla de verdad o aceptar la validez de la demostración mediante tabla de verdad.
Ugh... Acepto la validez de la prueba a través de una tabla de verdad. ¿Cuándo dije que no? Diablos, he escrito en comentarios cosas como "Saber que es válido ..." Entonces, sabiendo que es válido , solo quiero saber si se puede hacer una prueba en deducción natural sin usar CP o LEM. Parece que no se puede.
Es decir, solo quiero saber si se puede hacer una demostración en deducción natural sin usar CP o explícitamente usando LEM, es decir, como una regla de inferencia dentro del sistema , a diferencia de la de aquí: en.wikipedia. org/wiki/Absorption_(logic) , que creo que originalmente es de Russell. De nuevo, parece que no se puede.
Puedo decir que debe estar frustrado, pero creo que mi punto es más simple (¿y/o en un nivel diferente?) de lo que está respondiendo... Para decirlo claramente, estoy de acuerdo en que puede ser imposible lograr tal prueba. sin CP, LEM o tablas de verdad. Donde estoy perdido es cómo puedes definir ⊃ sin darle la tabla de verdad estándar que esperamos.
y luego, una vez que hayamos hecho eso, ¿no nos hemos comprometido a aceptar la prueba de la tabla de verdad (como mínimo)? Estoy tratando de pensar en una buena analogía, pero nada me viene a la mente de inmediato. Lo mejor que tengo hasta ahora, si aceptamos que solo puedo comunicarme en francés y entiendes lo que digo, se deduce que nos estamos comunicando en francés.
Hola, virmaior... ¡Te tengo! Permítanme ir al grano aquí... ¿Es su consulta básica (y reparo) realmente, "¿Cuál es su punto, Stegdude? Una tabla de verdad demuestra la validez de la absorción (y, de hecho, la equivalencia). Dejemos de lado LEM como una regla dentro del sistema, ya que muchos no lo permiten, como los constructivistas. Sin embargo, CP es totalmente lógico y admisible en todos los sistemas de lógica proposicional en la Tierra. Entonces, ¿por qué te importaría si una prueba en deducción natural o no? se puede construir para la absorción sin CP?" ¿Te estoy entendiendo bien, virmaior? :)
No. Eso no es todo.
Mi punto final es: ¿puedes definir ⊃ sin usar una tabla de verdad (o esencialmente lo mismo)? Si es así, entonces me encantaría saber cómo. Si no, entonces no veo cómo podemos rechazar las tablas de verdad para probar la absorción.
Con toda honestidad, ni siquiera sé cuál es la pregunta, "¿puedes definir ⊃ sin usar una tabla de verdad (o esencialmente lo mismo)?" significa. Entonces, mi respuesta de facto es "No". Dicho esto, por enésima vez, no rechazo la prueba de absorción por tabla de verdad ( en.wikipedia.org/wiki/Absorption_(logic)#Proof_by_truth_table ). Solo quiero la "prueba formal" ( en.wikipedia.org/wiki/Absorption_(logic)#Formal_proof ), PERO sin usar LEM (como lo hace ese) o CP. Se puede hacer? Si es así, déjamelo a mí. Eso es todo lo que estoy pidiendo. Tengo la impresión de que no puede ser.
Estoy realmente perdido en cuanto a dónde no me estás siguiendo en este momento. La definición de ⊃ en la tabla de verdad parece usar LEM o al menos bivalencia. Y la prueba de absorción por tabla de verdad no es diferente en ese punto. Si ⊃ se define formalmente por su tabla de verdad, entonces la absorción se prueba formalmente por el mismo tipo de tabla de verdad. Si la definición es legítima, no hay más movimientos en la prueba de la tabla de verdad...
Según los enlaces que proporcioné (como ejemplos) ... No quiero la "prueba de la tabla de verdad". Estoy hablando de la "prueba formal". Esa distinción te está registrando, ¿verdad? Suponiendo que sí, ¿es su punto, entonces, que debido a que la "prueba por tabla de verdad" para la absorción usa LEM, la "prueba formal" para la absorción también debe hacerlo?
(1) No entiendo por qué la prueba de la tabla de verdad no califica como prueba formal. Claro, los métodos son diferentes de lo que llamas una "prueba formal", pero la teoría es sólida. (2) Assuming so, is your point, then, that because the "proof by truth table" for absorption uses LEM ... NO . Mi punto es que la definición de ⊃ en sí misma asume LEM antes de que pueda probar algo, ya sea que la prueba sea mediante una tabla de verdad o algún otro método. / Reiterado, lo que pareces querer evitar parece estar integrado en la naturaleza misma de ⊃ y no sé cómo puedes deshacerlo.
En primer lugar, edité mi pregunta en aras de la claridad. :) ... ¡Sí, tienes toda la razón, virmaior! La palabra clave allí es "asumir", una palabra que he estado haciendo todo lo posible para evitar usar. LEM se asume en ambos métodos de prueba. Si se "asumió", horneado en el pastel, entonces no debería tener que afirmarse como una regla explícita de inferencia para probar algo dentro del sistema. De hecho, casi ningún sistema contemporáneo de "prueba formal" (¿influido por el constructivismo?) emplea LEM como regla de inferencia. Entonces, ¿por qué de repente necesitamos afirmarlo para proporcionar una "prueba formal" para la absorción? ...
... Bueno, la verdad es que NO tenemos que hacer valer LEM. Puede permanecer asumido y, en cambio, podemos hacer una "prueba formal" para la absorción usando CP (o IP, que, por supuesto, es solo un tipo de CP). ¡Pero también hay problemas para hacerlo con CP! :(

Respuestas (2)

La regla de absorción se puede demostrar mediante una tabla de verdad (que no es ni una "prueba condicional" ni una "prueba indirecta") de la siguiente manera:

P Q | P ⊃ Q | (P ∙ Q) | P ⊃ (P ∙ Q) | (P ⊃ Q) ≡ [P ⊃ (P ∙ Q)]
-----------------------------------------------------------
0 0 |   1   |    0    |   1         |         1
0 1 |   1   |    0    |   1         |         1
1 0 |   0   |    0    |   0         |         1
1 1 |   1   |    1    |   1         |         1

Pero, si las tablas de verdad presuponen la ley del tercero excluido, entonces parecería que la regla de absorción no es demostrable dentro de las restricciones que ha impuesto.

¡Gracias por tu respuesta, Jayson! Sin embargo, no estoy buscando solo probar/demostrar que la "regla de absorción" es válida. Sabiendo que es válido, estoy buscando una "prueba formal", una deducción formal, (llamada) deducción natural o de otra manera, para la "regla de absorción". Dicho esto, respondiste directamente a mi pregunta con tu última oración... en (según lo que había escrito en mi mensaje antes de que fuera editado) la forma "sencilla" que he llegado a anticipar (después de haberme metido con esto durante bastante tiempo). tiempo), es decir, "¡NO!" ¿De verdad crees que ese es el resultado final?
Jayson, también, otro pensamiento... ¿Es que las tablas de verdad presuponen la "ley del tercero excluido" o el "principio de bivalencia"? Si es lo último, entonces su respuesta fue más acertada de lo que usted o yo le dábamos crédito. Dicho esto, en última instancia estoy buscando la "prueba deductiva formal", que ambos parecemos creer que no existe. XDD
La idea de que el valor de verdad de P y el valor de verdad de Q tienen que ser 0 o 1 es el LEM, ¿verdad? Si no quiere presumir el LEM, tendría que incluir opciones para los casos en que cualquiera de los dos aún estaba indeciso. También necesitaría un estándar de implicación que no asuma automáticamente que la implicación siempre tiene un valor de verdad.
@Stegfucius Diría que presuponen bivalencia, pero esa bivalencia como propiedad de la semántica se basa en LEM en el metalenguaje utilizado para establecer la semántica. Como mínimo, la intuición de que la verdad es una propiedad "on" o "off" de las proposiciones parece ser lo que motiva tanto al LEM como a la bivalencia. Si los valores semánticos de las proposiciones no se consideran valores de verdad, es difícil ver por qué insistes en que solo hay dos. Por ejemplo, considere a un intuicionista que reemplaza "verdad" con "prueba", o la construcción de modelos de valores booleanos más allá del álgebra booleana de dos elementos.
Bueno, la tabla de verdad es una herramienta poderosa. Al menos para la lógica binaria.

Esta es solo una respuesta parcial porque utiliza la eliminación condicional y la introducción condicional que pueden estar prohibidas. Sin embargo, no utiliza la ley del tercero excluido (LEM).

Según entiendo los comentarios, hay algunas dudas sobre la prohibición de reglas para condicionales si se permite un condicional en la premisa y un condicional en la conclusión. Si uno usa condicionales para establecer la prueba, se deben especificar las reglas para manipular el condicional.

La prueba se realizó utilizando el editor y comprobador de pruebas de deducción natural de Kevin Klement .

ingrese la descripción de la imagen aquí

Aquí está la prueba de absorción usando LEM en el artículo de Wikipedia citado, "Absorción (lógica)" :

ingrese la descripción de la imagen aquí