Perdona, es culpa mía que enseguida me voy por las ramas haciendo comentarios que no vienen al caso.
Me refiero a que si usas deducción natural una de las reglas es que si bajo una suposición arbitraria \( p \) deduzco \( q \) entonces la regla de introducción del implicador da una deducción de \( p \rightarrow q \), sin suposiciones (se dice que has descartado la suposición \( p \)).
Vale... No entiendo cómo esto nos ayuda a probar la validez el razonamiento... 
.
En este caso en nada. Trataba de darle una explicación al hecho de que hayas metido una suposición "por la cara" (en sistemas de deducción natural puedes hacerlo, pero después debes descartarla usando la regla de introducción del implicador). Mejor olvida todo esto y quédate con que no puedes introducir suposiciones arbitrarias.
Suelo marearme mucho y perder el foco de atención en todo esto. Me concentré mucho en entender la cita y ahora me olvidé cómo debíamos proseguir en nuestra prueba.
Pues, ¡exactamente igual que antes, cuando teníamos la \( p \)!. Fíjate que antes hemos dado una demostración de \( \neg r \) a partir de \( \neg s \) y \( 5) \) (numeración de la prueba antigua), que no involucran ninguna \( p \). Para obtener ahora \( \neg s \) usas la premisa \( 3) \) (numeración nueva) y el antiguo \( 5) \) es exactamente la premisa \( 2) \) actual. Así que puedes hacer
exactamente el mismo razonamiento para obtener \( \neg r \).
Seguramente haya mucha redundancia entre este hilo y los demás. El problema está en que ante dos enunciados que me parecen tan distintos recurro a ustedes, porque yo siento que no puedo solo. Esto me ocurre porque yo creo haber aprendido y ante el cambio de otro razonamiento matemático, se me nubla la vista parcialmente.
No te lo tomes a mal (no es nada malo), pero creo que te falta un punto de "madurez matemática" (o lógica, en este caso). Esto quiere decir que te falta un poco de práctica con demostraciones formales de este estilo. En realidad, todas siguen más o menos la misma estructura, y con suficiente práctica no te debería costar mucho hacer demostraciones formales de este nivel de dificultad, incluso debería convertirse en algo más o menos mecánico. La clave está en ser capaz de explicar con palabras la deducción, una vez tienes claro cómo va el argumento traducirlo a reglas a aplicar y demás es lo de menos.
Claro, pero siento como que nos hemos ido por las ramas (aunque no lo sea). ¿Cómo damos una demostración válida de \( \neg r \)? No lo veo porque no veo que se pueda demostrar \( \neg r \) (no me parece una proposición, como lo es "Si \( f \) es derivable entonces es continua" o "Todo número natural distinto de \( 1 \) puede escribirse como un único producto de números primos sin importar el orden de los factores").
Con demostración aquí me refiero a una demostración formal. Es decir, una demostración del estilo que estás haciendo (aplicando reglas de inferencias y demás) que pruebe que de las tres premisas que tienes se sigue \( \neg r \).
(Inciso, o ida por las ramas: Una proposición como "Si \( f \) es derivable entonces es continua" es una proposición igual de válida que \( \neg r \) una vez formalizada, y puedes dar una demostración formal del mismo estilo de las que estamos haciendo aquí, solo que mucho más larga y difícil. De hecho, precisamente para esto se inventaron los cálculos deductivos en lógica, para dar demostraciones formales de proposiciones matemáticas.)
Mitad y mitad 
. Es para un compañero de la universidad pero a la vez me ayuda a mí entender estas cosas, porque me encanta estudiar esto (por más que lo aprenda una y otra vez con el correr de la apertura de hilos muy parecidos, porque no soy capaz de ver las similitudes...).
La lógica es muy divertida, a mí también me encanta.
Sobre lo de no ver las similitudes, es cuestión de práctica como te he dicho. Tienes que pasar de fijarte en razonamientos muy concretos de unas proposiciones muy concretas a ver el bosque, es decir, a cuándo te enfrentes con la prueba de algo pensar "ah, quiero probar una conjunción, así que voy a probar cada una de las proposiciones que los componen por separado, voy a mirar qué premisas tengo y puedo usar para ello, etc". A veces también me da la sensación de que eres demasiado formalista y pierdes de vista el significado intuitivo de las cosas. Hay que entender las reglas, por qué funcionan a nivel intutivo, qué significan los conectores a nivel intuitivo, etc. Hay que aprovechar la intuición y el significado de las cosas, es una de las pocas ventajas que tenemos sobre las máquinas.
Gracias por acordarte. Aprecio tu interés. Me gusta la informática pero jamás se me ocurriría diseñar un lenguaje de programación diseñado a demostración de teoremas porque últimamente estoy creyendo que necesitaría años y años para recopilar todos los axiomas y todas las posibles combinaciones de demostraciones posibles (¿cuándo sabemos que algo es "evidente por sí mismo"? o, ¿cómo sabemos que el programa no cruzará los cables para que dos pruebas del mismo enunciado no sean contradictorias?). Suponer todo eso me aniquila, porque no quiero diseñar (ni testear) un programa al que le pasen esas cosas, por más que sea poco o nada probable.
Así que no he probado Coq ni Agda y jamás había escuchado hablar de ellos. Pero buscando por la web parecen muy prometedores e interesantes pero por fuera de mi alcance (tengo una máquina con Windows, además nunca usé Linux o Mac OS por ejemplo).
En realidad no es que diseñes un lenguaje de programación para demostrar teoremas. Estos lenguajes ya tienen las reglas de la lógica incorporadas y te sirven para hacer lo mismo que hacemos aquí con las demostraciones formales, pero validadas por el programa, de manera que te aseguras de que no has cometido errores o has usado reglas de manera incorrecta.
De todas maneras, aprender algo de Coq o Agda, aunque sea interesante, no es tan fácil y lleva su tiempo.
Sobre lo de recopilar axiomas y demás no tienes por qué hacerlo, ya lo han hecho muchos lógicos antes por nosotros. En cualquier libro de lógica puedes encontrar cálculos deductivos con unos pocos axiomas y unas pocas reglas que te permiten demostrar cualquier teorema válido.
