¿Cómo puedo hacer que las demostraciones con fórmulas largas sean más legibles sin sacrificar la claridad?

Question

Pregunta

Actualmente, muchas cosas que estoy tratando de demostrar se están convirtiendo en un "infierno de notación", lo que creo que dificulta mucho su lectura. He intentado reducir esto asumiendo que mi lector entenderá qué definiciones están en juego, modularizando mis pruebas y omitiendo la explicación de pasos que espero sean obvios. También he intentado renombrar las fórmulas con nombres cortos (es decir, $\def\val#1{V_\pli(#1)}\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\def\pli{\mathscr{I}}\def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}\def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}\def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots)):=\,\s Q),$ pero para demostraciones de cualquier longitud parece ser más confuso que útil. ¿Cómo puedo hacer las demostraciones más legibles sin sacrificar la claridad?

---

Prueba Ejemplo

Sean $\p$ y $\q$ fórmulas bien formadas y $n\in\mathbb{N}$ (por favor, note que $0\not\in\mathbb{N}$). Queremos demostrar que $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ si y solo si $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))$.

En (L1) pruebo ambas direcciones de la bicondicional, lo cual no creo que sea necesario hacer porque estamos tratando con "=" - ¿es esto correcto? También creo que (L1) es tan básico que "por inspección" es apropiado - ¿es justo esto?

Lema 1 (L1)

Queremos demostrar por inducción que para alguna interpretación de PL, $\pli,$ $\val{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ si y solo si $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$.

Caso Base

• Si $\val{\p\to\q}=0$ entonces, por definición, $\val{\p}=1$ y $\val{\q}=0$. Si $\val{\p}=1$ y $\val{\q}=0$, entonces, por definición, $\val{\p\to\q}=0$

Hipótesis de Inducción (HI)

• Supongamos para algún $k\in\mathbb{N}$ arbitrario que $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ y $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$

Paso de Inducción

• Si $\val{\p_{k+1}\to(p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots)))}=0,$ entonces, como sabemos que $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$ por la (HI), $\val{\p_{k+1}}=1$. De la (HI) $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$, por lo tanto $\val{\p_{k+1}}=\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$

• Permita que $\val{\p_{k+1}}=1$. De la (HI) $\val{\p_k}=\val{\p_{k-1}}=\cdots=\val{\p_1}=1,$ $\val{\q}=0,$ y $\val{p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0,$ por lo tanto $\val{\p_{k+1}\to(p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots)))}=0$

Prueba de la Primera Dirección (P1)

1. Por reducción al absurdo, supongamos que no es el caso que $\aa\implies\ba$

2. Se sigue de (1) que existe una $\def\pli{\mathscr{I}}\pli$ tal que $\def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}\def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}\def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}\aa$ y $\bb$

3. Se deduce de (2) que $\def\val#1{V_\pli(#1)}\val{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}=0$

4. De (L1), la valoración en (3) solo puede ocurrir cuando $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$

5. Se sigue de (4) que $\ab$, lo cual contradice (2) y prueba nuestra primera dirección

Prueba de la Segunda Dirección (P2)

1. Por reducción al absurdo, supongamos que no es el caso que $\ba\implies\aa$

2. Se sigue de (1) que existe una $\pli$ tal que $\ba\text{ and }\ab$

3. De (2) tenemos $\ab$, por lo tanto, $\val{\p_n}=\val{\p_{n-1}}=\cdots=\val{\p_1}=1$ y $\val{\q}=0$

4. Se sigue de (3) y (L1) que $\bb\text{,}$ lo cual contradice (2) y prueba nuestra segunda dirección

(P1) y (P2) prueban ambas direcciones de la bicondicional, por lo tanto $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ si y solo si $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))\,\square.$

Answer 1

Sugerencia principal

En lugar de

Queremos demostrar $\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q$ si y solo si $\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))$

inténtalo de esta manera:

Queremos demostrar que $$\def\p{\phi}\def\q{\psi}\def\s{\vDash_{\tiny\text{PL}}}\def\ns{\nvDash_{\tiny\text{PL}}}\p_1,\,\p_2,\,\ldots,\,\p_n\s\q \tag{1}$$ si y solo si $$\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots)).\tag{2}$$

Después de eso, en lugar de repetir las fórmulas largas cada vez, simplemente llámalas $(1)$ y $(2)$:

Para la reducción al absurdo, supongamos que no es el caso que $(2)\implies (1)$. Entonces debe existir un $\mathscr I$ tal que $(2)$ se cumple pero $(1)$ no.

Sugerencias menores

1. Abrevia $$\phi_n\to(\phi_{n-1}\to(\cdots\to(\phi_1\to\q)\cdots))$$ como $$\Phi_n.$$ (No uses $Q$. ¿Por qué usarías $Q$?)

   En lugar de $$V_\mathscr{I}({p_k\to(\p_{k-1}\to(\cdots\to(\p_1\to\q)\cdots))})=0$$ ahora puedes escribir $$V_\mathscr{I}({p_k\to\Phi_{k-1}})=0$$ y el lector no extrañará que la primera variable sea un $p$ y no un $\phi$.

   Dijiste que abreviar parece "más confuso que útil". No lo es.

2. Abrevia $\phi_1,\phi_2,\ldots,\phi_n$ como $\vec\phi$.

3. Abrevia $$V_\mathscr{I}(\phi_n)=V_\mathscr{I}(\phi_{n-1})=\cdots=V_\mathscr{I}(\phi_1)=1$$ como $$V_\mathscr{I}(\phi_i) = 1\quad (i=1\ldots n)$$ o quizás $$V_\mathscr{I}(\phi_{1\ldots n}) = 1.$$

4. No estás abreviando las cosas correctas. No necesitas abreviar "si y solo si" como "iff", o "Lema 1" como "L1". El objetivo aquí no es eliminar todo el inglés normal de tu prueba. Estas abreviaturas son más confusas que útiles.

No hagas que el lector compare dos fórmulas largas para asegurarse de que son iguales, o preguntarse por qué no lo son. Diseña tu notación para resaltar las diferencias entre fórmulas similares.

La notación, al igual que el lenguaje, es flexible. No hay reglas; se te permite inventar cosas. $\vec\phi$ realmente no es un vector. No importa. Puedes explicarlo brevemente: "Abreviaremos $\phi_1,\phi_2,\ldots,\phi_n$ como $\vec\phi$." Nadie se confundirá ni olvidará lo que significa. Mi sugerencia $V_\mathscr{I}(\phi_{1\ldots n})$ no es estándar. No importa; el significado es claro.

Sugerencias ortogonales

1. No estás utilizando TeX correctamente. No necesitas seguir repitiendo \defs. Una vez que defines un nuevo conjunto de control con \def, la definición sigue vigente hasta el final del grupo o del documento. Define los macros importantes una vez, al principio del archivo, o en un archivo \included.

2. Define macros mejores. La estructura de los macros debe seguir la estructura sintáctica de tus fórmulas. En lugar de escribir

   \def\aa{\p_1,\,\p_2,\,\ldots,\,\p_n\s\q}
   \def\ab{\p_1,\,\p_2,\,\ldots,\,\p_n\ns\q}
   \def\ba{\s\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))}  
   \def\bb{\ns\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\q)\cdots))

   inténtalo de esta manera:

   \def\ps{\p_1,\,\p_2,\,\ldots,\,\p_n}
   \def\aa{\ps\s\psi}
   \def\ab{\ps\ns\psi}
   \def\pformn{\p_n\to(\p_{n-1}\to(\cdots\to(\p_1\to\psi)\cdots))}
   % ahora no necesitas \ba o \bb, solo usa \s\pformn y \ns\pformn