Pregunta sobre la prueba 3.3 en los Principia Mathematica

Por lo que puedo entender, la clave de PM es asegurarse de que no haya saltos ni lagunas al hacer inferencias. En otras palabras, todas las premisas y reglas de inferencia deben enumerarse explícitamente con la excepción de ❊1.11. Me pregunto, en la demostración de ❊3.3, ¿por qué se omite Syll en el primer y tercer paso pero se menciona en el último paso?ingrese la descripción de la imagen aquí

Esto no es una pregunta. ¿Puede explicar por qué esto pertenece aquí y qué tipo de respuesta está esperando?
@iphigenie: La última oración se puede reescribir fácilmente como una pregunta.
@DBK: Gracias. Lo he reformulado como una pregunta.
George, Metamath es un buen compañero para tener en tu viaje a través de PM. No me sorprendería si 3.3, en una notación más agradable, se encontrara entre los miles de pruebas en ese sitio web. Así que mira eso.

Respuestas (2)

primero reescribamos la prueba de Russels en notación moderna:

Id(*3.01) = |- (((P & Q) -> R) -> (~(~P v ~Q) -> R)
transp                         -> (~R -> (~P v ~Q))
Id (*1.01)                     -> (~R -> (P -> ~Q))
comm                           -> (P -> (~R -> ~Q))
transP.syll                    -> (P -> (Q -> R))) |-. prop

Creo que Russel usa la regla del silogismo (|- P -> Q, |- Q -> R => |- P -> R ) sin mencionarlo, porque solo hace que la prueba sea innecesariamente complicada.

para agregarlos a la prueba se convierte en

Id(*3.01)   = |- (((P & Q) -> R)   -> (~(~P v ~Q) -> R)
transp      = |- (~(~P v ~Q) -> R) -> (~R -> (~P v ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (~R -> (~P v ~Q))
Id (*1.01)  = |- (~R -> (~P v ~Q)) -> (~R -> (P -> ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (~R -> (P -> ~Q))
comm        = |- (~R -> (P -> ~Q)) -> (P -> (~R -> ~Q))
--syllogism-- |- (((P & Q) -> R)   -> (P -> (~R -> ~Q))
transP.syll = |- (P -> (~R -> ~Q)) -> (P -> (Q -> R)))
--syllogism-- |- (((P & Q) -> R)   -> (P -> (Q -> R)))

solo hace que la prueba sea 4 líneas más larga y mucho menos espacio en blanco, pero si lo encuentra mejor, hágalo de esta manera (ps, pero incluso aquí, ¿no quiere volver a los axiomas?

Gracias, @Willemien. En esta etapa, lo que es obvio para los autores es un gran vacío para mí. Por eso creo que vale la pena trabajar en los primeros cinco capítulos. Espero poder "ver" lo que los autores "ven" después.

Tiene razón tu comentario.

La prueba se basa en una "cadena" de condicionales ; por lo tanto, necesitamos a Syll .

En el tercer paso, para pasar de:

⊢ (pq ⊃ r) ⊃ ( ~r ⊃ (p ⊃ ~q) ) --- (3)

a :

⊢ (pq ⊃ r) ⊃ (p ⊃ ( ~r ⊃ ~q) ) --- (4)

tenemos que construir la "cadena":

(3) --- ⊢( ~r ⊃ (p ⊃ ~q) ) ⊃ (p ⊃ ( ~r ⊃ ~q) ) --- por Comm --- (4) --- por Syll .

Toda la prueba de hoy se simplificará enormemente mediante el uso del teorema de deducción ; falta en PM porque Tarski y Herbrand lo descubrieron de forma independiente durante los años 30.

PD: creo que un lugar más adecuado para este tipo de preguntas es math.stackexchange.
Gracias, @Mauro ALLEGRANZA. Mi objetivo aquí es volver sobre el viaje mental de Whitehead y Russell. Por eso uso la primera edición. Lo que se proponen probar no es tan importante como el proceso de sus pruebas. Creo que tienes razón, necesito moverlo a math.stachexchange
Me gusta mucho tu comentario. @Mauro ALLEGRANZA Gracias por brindar el contexto histórico. No sé si alguien de la comunidad matemática tiene este tipo de calibre.
En PM, el paso 3 de @Mauro ALLEGRANZA sería ❊2.16 Transp. A partir del capítulo tres, PM aún no ha producido nada como el teorema de deducción, se las arregla con ❊1.11, una Pp. (proposición primitiva): cuando tanto Phi(x) como Phi(x) -> Psi(x) pueden ser afirmado, entonces Psi(x) puede ser afirmado.
Te confirmo que el Teorema de la Deducción no está presente en PM: fue enunciado por primera vez durante los años '30. *1.11 es más como una versión de Modus Ponens para fórmulas con variables libres.
Gracias, Mauro ALLEGRANZA. En PM, si se puede afirmar r o si se puede afirmar p=>q es irrelevante. Por Transp, (p=>q)=>(~q=>~p) puede afirmarse; junto con Syll y *1.11, r=>(p=>q) .=>. r=>(~q=>~p) puede afirmarse. Todo lo que queremos afirmar es que de r=>(p=>q) podemos inferir r=>(~q=>~p). Creo que este es el verdadero espíritu de PM, es decir, las matemáticas te dicen lo que sigue a tus premisas pero no te dicen si tus premisas son verdaderas.