21/01/2020, 07:51:41 am *
Bienvenido(a), Visitante. Por favor, ingresa o regístrate.

Ingresar con nombre de usuario, contraseña y duración de la sesión
Noticias: Puedes practicar LATEX con el cómodo editor de Latex online
 
 
Páginas: [1]   Ir Abajo
  Imprimir  
Autor Tema: Número 2. (2013) - 3 Lógica de primer orden  (Leído 19573 veces)
0 Usuarios y 1 Visitante están viendo este tema.
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« : 04/03/2013, 11:21:40 am »

Como es habitual en este tipo de hilos, para facilitar el seguimiento del texto los comentarios que puedan surgir deben dirigirse a este hilo auxiliar de comentarios.



¿Qué es la lógica? Para formarnos una primera idea de cómo hay que entender la palabra "lógica" en el contexto de este artículo, creo que será ilustrativo considerar el silogismo siguiente:

Toda palabra properispómena es barítona,
[texx]\delta\tilde\omega\rho\omicron\nu[/texx] es una palabra properispómena,
luego [texx]\delta\tilde\omega\rho\omicron\nu[/texx] es una palabra barítona.


Tenemos ahí tres afirmaciones, y cualquiera que sepa algo de gramática griega podrá asegurarnos que las tres son verdaderas. Ahora bien, lo interesante desde el punto de vista lógico es que, sin saber absolutamente nada de gramática griega, podemos afirmar sin riesgo a equivocarnos que si las dos primeras afirmaciones son verdaderas, entonces la tercera también lo es.

Más detalladamente: Si toda palabra properispómena (signifique esto lo que signifique) es barítona (signifique esto lo que signifique) y [texx]\delta\tilde\omega\rho\omicron\nu[/texx] (sea esto lo que sea) es una palabra properispómena (sea esto lo que sea), podemos afirmar sin riesgo a equivocarnos que [texx]\delta\tilde\omega\rho\omicron\nu[/texx] (aunque no sepamos lo que es eso) es una palabra barítona (aunque no sepamos lo que es eso).

¡Pues esto es la lógica formal! ¡Esto es razonar formalmente! Consiste en concluir que determinadas afirmaciones son necesariamente ciertas bajo el supuesto de que otras lo sean, y llegar a tal conclusión sin atender en ningún momento al posible significado de las afirmaciones, sino meramente a su "forma". El razonamiento anterior tiene la forma siguiente:

Todo P es Q,
X es P,
luego X es Q.


y sólo por tener esa forma, podemos asegurar que es lógicamente válido, es decir, que si las dos primeras afirmaciones son verdaderas, entonces la tercera también tiene que serlo, y da igual que P signifique "palabra properispómena" o "bailarina de ballet".

La lógica formal determina qué razonamientos son válidos en este sentido (de que llevan necesariamente de afirmaciones verdaderas a afirmaciones verdaderas) atendiendo únicamente a la "forma", a la sintaxis, de las afirmaciones involucradas, y nunca a su posible significado. Esto no significa que no vayamos a estudiar y tener en cuenta los posibles significados de las afirmaciones que consideremos, sino únicamente que nuestro objetivo es tener en cuenta tales significados posibles sólo para acabar confirmando que hemos logrado nuestro propósito, es decir, que tenemos ciertamente la garantía de que nuestras conclusiones serán válidas independientemente cuáles sean tales significados posibles.

Para lograr este objetivo necesitamos sustituir el castellano por un lenguaje alternativo lo suficientemente simple como para ser estudiado teóricamente, pero a la vez lo suficientemente potente como para que pueda expresar cualquier razonamiento en el que podamos estar interesados.

El problema es que el castellano (como cualquier otra lengua natural) presenta ambigüedades que sólo pueden ser resueltas por el contexto, lo cual a menudo significa tener en cuenta el significado de las afirmaciones que estamos haciendo. Por ejemplo, recordemos lo que un desdichado amante le decía a su amada:

¿Cómo quieres que venga a verte, si el perro de tu padre sale a morderme?

Ésta es una frase que respeta totalmente la sintaxis castellana y, sin embargo, es inevitablemente ambigua. Podemos leerla una y mil veces y nada nos permitirá concluir con seguridad si quien afirmó esto estaba diciendo que su suegro tenía un perro o más bien que su suegro era un perro. Más concretamente, la expresión castellana "el perro de tu padre", puede significar "el perro que tiene tu padre" y también "el perro que es tu padre" (y, paralelamente, "morderme" puede tener un sentido literal o figurado).

Para estar en condiciones de estudiar la lógica con precisión necesitamos un lenguaje en el que estas cosas no puedan suceder, en el que cada afirmación tenga, no un significado, pero sí una forma precisa e inequívoca. El problema de la frase anterior no es que no sepamos el significado exacto de "te" en "verte" (no importa si la amada es fulana o mengana), ni que no sepamos quién es su padre (quién sea en concreto sería irrelevante para entender la lógica de la frase). Lo que hace que la frase no tenga una "lógica", una "forma" definida es que no sabemos si "perro" y "padre" se refieren al mismo objeto o a objetos distintos.

Sin embargo, sería injusto decir, por culpa de ejemplos como éste, que el castellano es un lenguaje inapropiado para razonar con precisión. Tal prejuicio lleva necesariamente a absurdos epistemológicos. La realidad es que en castellano se puede razonar con absoluta precisión (y cualquier ambigüedad que surja siempre se puede resolver en cuanto sea detectada) siempre y cuando hablemos de objetos cuyo significado sea totalmente preciso, hasta el punto de que no tengamos dificultades en determinar objetivamente el significado exacto de cada afirmación que consideremos.

La necesidad de la lógica formal, es decir, de la posibilidad de razonar mediante un lenguaje libre de ambigüedades sin tener en cuenta el significado posible de las palabras que empleemos, surge desde el momento en que pretendemos razonar con objetos a los que no somos capaces de dar un significado preciso. El caso más representativo es el concepto de "conjunto". Aunque todos tengamos una idea más o menos vaga de qué entendemos por "conjunto", lo cierto es que no es posible precisar su significado hasta el punto de poder hablar con seguridad sobre conjuntos controlando lo que decimos en función del significado de nuestras afirmaciones. La única forma conocida de razonar con rigor sobre conjuntos arbitrarios, como hacen los matemáticos, es manejar la palabra "conjunto" como alguien que no sepa griego puede manejar la palabra "properispómeno" para convencerse de que el silogismo anterior era correcto. Se trata de decir: si los "conjuntos" (sean lo que sean) cumplen tales axiomas, entonces los conjuntos "sean lo que sean" cumplen tales teoremas.

Así pues, nuestro propósito es, por una parte, diseñar lenguajes (no uno solo, sino que podemos considerar lenguajes distintos adaptados a cada contexto que queramos describir) con una gramática precisa y libre de ambigüedades (que impida que algunas expresiones como "el perro de tu padre" se puedan entender de formas lógicamente distintas), por otra parte estudiar la relación entre dichos lenguajes y los significados posibles de sus palabras (o, más precisamente, de sus signos) y finalmente mostrar que es posible manipular tales lenguajes sin atender para nada a los significados posibles de sus signos, pero con la garantía de que si, de acuerdo con un significado establecido, partimos de afirmaciones verdaderas, las conclusiones formales que obtendremos serán también verdaderas.

Este proyecto nos lleva inevitablemente a la necesidad de distinguir con sumo cuidado los signos y sus posibles significados. Nuevamente el castellano deja estas distinciones a cargo del contexto de una forma demasiado vaga para nuestras necesidades. Consideremos por ejemplo las dos frases siguientes:

España está en Europa                España tiene tres sílabas.

Cualquiera que las lea las entiende correctamente y reconoce que ambas son verdaderas, pero para ello ha tenido que interpretar la palabra "España" de dos formas completamente distintas, sin que nada en las frases advierta explícitamente de la necesidad de hacer tal distinción. En la primera frase "España" se interpreta como un país, mientras que en la segunda frase "España" se interpreta como una palabra.

El país España es un objeto completamente distinto de la palabra España. Para distinguir ambos conceptos (cosa que el castellano no obliga a hacer) adoptaremos el convenio de poner una palabra entre comillas cuando no queramos referirnos a su significado, sino a la palabra en sí. Con este criterio deberíamos escribir:

España está en Europa                "España" tiene tres sílabas.

Así, por ejemplo, entre los signos de los lenguajes que vamos a definir, llamaremos constantes a los que pretenden nombrar objetos (los equivalentes de los sustantivos en castellano), de modo que si diseñamos un lenguaje formal en el que hay una constante [texx]N[/texx] que pretendemos usar para nombrar a Napoleón, entonces [texx]N[/texx] será el equivalente en nuestro lenguaje a la palabra "Napoleón" en castellano, mientras que usaremos una barra [texx]\overline N[/texx] para referirnos al significado de la constante [texx]N[/texx] (en este caso, Napoleón, sin comillas, o, más precisamente, el emperador Napoleón I de Francia).

La diferencia entre [texx]N[/texx] y [texx]\overline N[/texx] es exactamente la misma que hay entre "Napoleón" y Napoleón. Y confundir [texx]N[/texx] con [texx]\overline N[/texx] resultaría tan catastrófico como creer que una palabra ha sido emperador de Francia o que un emperador de Francia estuvo formado por ocho letras, en lugar de por carne, huesos, fluidos corporales, etc.)

Más concretamente, [texx]N[/texx] es una palabra (un signo) de nuestro lenguaje formal, de mismo modo en que "Napoleón" es una palabra castellana, mientras que [texx]\overline N[/texx] no es una palabra de nuestro lenguaje formal, sino un hombre que lleva mucho tiempo muerto.

Spoiler: Más vueltas sobre lo mismo (click para mostrar u ocultar)

Como decimos, la distinción cuidadosa entre [texx]N[/texx] y [texx]\overline N[/texx] va a marcar la diferencia entre entender qué estamos haciendo o no entender nada de nada. En particular hay que tener presente que definir un lenguaje formal que contenga una constante [texx]N[/texx] convierte a [texx]N[/texx] en un signo fijo e inamovible de dicho lenguaje, pero esto no nos obliga a fijarle de forma inamovible un significado [texx]\overline N[/texx]. Por el contrario, podemos trabajar con un lenguaje formal sin atribuir ningún significado concreto a sus signos, o bien podemos establecer en un momento dado que la constante [texx]N[/texx] significa Napoleón, pero también podemos más tarde considerar el mismo lenguaje formal pero interpretando [texx]N[/texx] de otra forma, digamos como Nabucodonosor, o como Beethoven. En resumen, nos va a interesar fijar lenguajes con unos signos específicos, como pueda ser una constante [texx]N[/texx], y luego comparar distintas interpretaciones de dichos signos, de modo que  [texx]\overline N[/texx] pueda ser Napoleón en un caso o Nabucodonosor en otro. De hecho, lo que nos interesará es poder decir cosas del estilo de "esto va a ser cierto sea lo que sea [texx]\overline N[/texx] ".

La idea subyacente en todo lo que vamos a exponer es la siguiente:

1) Tenemos diversas realidades de las que podemos hablar en buen castellano

2) Podemos diseñar lenguajes formales para hablar de dichas realidades de forma "controlada".

3) Los lenguajes que vamos a diseñar pueden ser manipulados con total precisión sin hacer referencia a ninguna realidad concreta (incluso si no somos capaces de precisar una realidad concreta que se ajuste a lo que afirmamos), pero con la garantía de que si partimos de afirmaciones verdaderas en una realidad cualquiera, las conclusiones a las que llegaremos serán verdaderas en esa misma realidad.

En el mensaje siguiente empezaremos a precisar debidamente estas ideas.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #1 : 04/03/2013, 17:13:16 pm »

En este mensaje presentaremos sin ánimo de ser rigurosos los conceptos básicos que vamos a manejar. Presentaremos "mezclados" los conceptos sintácticos (relativos a los signos) y los semánticos (relativos a los significados de los signos) porque resulta más natural. Luego, en el mensaje siguiente los separaremos cuidadosamente y precisaremos todo lo que aquí haya podido quedar "en el aire".



El universo de una interpretación Como hemos dicho en el mensaje anterior, cada lenguaje formal se diseña para describir una realidad. También hemos señalado que al final no será obligatorio explicar cuál es esa realidad de la que queremos hablar, sino que los lenguajes formales terminarán siendo "autónomos" y podremos razonar con ellos sin necesidad de especificar qué son los objetos de los que presuntamente estamos hablando. Ahora bien, si, pese a no estar obligados a ello, queremos especificar cuál es la "realidad" de la que estamos hablando con un lenguaje dado, lo primero que tendremos que especificar es la colección de objetos que integran dicha realidad. Dicha colección de objetos será lo que llamaremos el universo de la interpretación.

Por ejemplo, vamos a construir un lenguaje formal y le vamos a asignar a la vez una interpretación, y establecemos aquí que el universo de dicha interpretación será la colección [texx]U[/texx] de todos los seres humanos que han vivido o viven en la Tierra desde el año 1 hasta el año 2012.

Spoiler: Colecciones (click para mostrar u ocultar)



Constantes Definir un lenguaje formal supone especificar unos signos. No vamos a poner restricciones sobre la forma que puedan adoptar los signos de un lenguaje formal. Cada signo podrá ser una letra (latina, griega, hebrea, etc.), una combinación de letras o cualquier "garabatito" con el único requisito de que podamos diferenciar clara e inequívocamente un signo de otro.

Pero, al establecer que un signo forma parte de un determinado lenguaje formal, estamos obligados a especificar su "función sintáctica" (el equivalente en castellano a ser un sustantivo, un adjetivo, un verbo, un pronombre, una conjunción, etc). Por ejemplo, en el mensaje precedente ya hemos hablado de las constantes. Son los nombres propios de los lenguajes formales. Una constante es un signo al que, en caso de que decidamos especificarle un significado, éste será un objeto concreto (perteneciente a un universo prefijado).

Por ejemplo, podemos empezar a construir un lenguaje formal estableciendo que va a tener tres constantes, [texx]N[/texx], [texx]J[/texx] y [texx]n[/texx]. Y además podemos atribuirles un significado. Por ejemplo, considerando el universo [texx]U[/texx] especificado anteriormente, podemos establecer que [texx]\overline N[/texx] (el significado de la constante [texx]N[/texx]) sea el emperador Napoleón I, mientras que [texx]\overline J[/texx] (el significado de [texx]J[/texx]) sea la emperatriz Josefina Beauharnais y que [texx]\overline n[/texx] sea Napoleón II, el hijo de ambos.

Aquí es crucial recordar que [texx]N[/texx] es un signo de un lenguaje formal y [texx]\overline N[/texx] es un emperador de Francia.



Relatores Fijado un universo, entre sus objetos podemos seleccionar las relaciones que nos interesen. En general, una relación [texx]n[/texx]-ádica [texx]R[/texx] en un universo [texx]U[/texx] es cualquier criterio que, a cada [texx]n[/texx] objetos [texx]x_1,\ldots, x_n[/texx] de [texx]U[/texx], repetidos o no y en un cierto orden, les asigna un "verdadero" o "falso". Cuando la relación [texx]R[/texx] es verdadera sobre [texx]x_1,\ldots, x_n[/texx] escribimos (a modo de taquigrafía) [texx]R(x_1,\ldots, x_n)[/texx].

Por ejemplo, en nuestro universo [texx]U[/texx] tenemos la relación monádica "ser un hombre", que es verdadera sobre los objetos de [texx]U[/texx] que son hombres y es falsa sobre los que son mujeres (donde podemos definir "hombre" como "tener al menos un cromosoma Y").

Un ejemplo de relación diádica en [texx]U[/texx] sería por ejemplo "estar casados".

Los relatores son los signos de un lenguaje formal que, en caso de ser interpretados, su significado es una relación. Un relator monádico es un relator que debe ser interpretado por una relación monádica, un relator diádico es un relator que debe ser interpretado por una relación diádica, etc.

Por ejemplo, en nuestro lenguaje formal podemos incluir dos relatores monádicos [texx]H[/texx] y [texx]M[/texx] y asignarles como significado las relaciones [texx]\overline H[/texx] y [texx]\overline M[/texx] en [texx]U[/texx] dadas por "ser un hombre" y "ser una mujer", respectivamente.

En estos términos las cadenas de signos [texx]HN, MJ, Hn[/texx] serían verdaderas, pues significan que Napoleón I es un hombre, que Josefina es una mujer y que Napoleón II es un hombre. En cambio [texx]HJ[/texx] sería una afirmación falsa.

También podemos introducir un relator diádico [texx]C[/texx] y asignarle como significado la relación diádica [texx]\overline C[/texx] tal que [texx]\overline C(x,y)[/texx] se cumple cuando [texx]x[/texx] e [texx]y[/texx] están casados (para cualesquiera objetos [texx]x[/texx], [texx]y[/texx] del universo [texx]U[/texx].

En estos términos, [texx]CNJ[/texx] es una afirmación verdadera en nuestro lenguaje formal, de acuerdo con la interpretación fijada. En cambio, [texx]CNn[/texx] es falsa.

Podemos considerar también un relator triádico [texx]\rm Pd[/texx] y asignarle como significado la relación [texx]\overline{\rm Pd}[/texx] en [texx]U[/texx] tal que [texx]\overline {\rm Pd}(x,y,z)[/texx] se cumple si [texx]x[/texx] e [texx]y[/texx] son los padres de [texx]z[/texx].

Así, [texx]{\rm Pd}NJn[/texx] es una afirmación verdadera, y [texx]{\rm Pd}NnJ[/texx] es falsa.

Cuando definimos un lenguaje formal, debemos especificar sus signos, así como a qué categoría pertenece cada signo (si es una constante, o un relator, o pertenece a cualquiera de las otras categorías que aún tenemos que introducir) y, en caso de que sea un relator, debemos especificar su rango, es decir, si se trata de un relator monádico, o diádico, o triádico, etc. No estamos obligados a asignarle un significado a un relator, pero si lo hacemos, la relación asignada a un relator monádico debe ser monádica (es decir, debe requerir un complemento), la asignada a un relator diádico debe ser diádica (debe requerir dos complementos), etc.

Spoiler: Observaciones (click para mostrar u ocultar)

Cada lenguaje formal puede tener las constantes que queramos (incluso ninguna) y los relatores que queramos, pero exigiremos que todo lenguaje formal tenga al menos un relator diádico que representaremos por [texx]=[/texx] (y que llamaremos igualador) y al que siempre asignaremos el mismo significado, a saber la relación diádica [texx]\equiv[/texx] de identidad (de modo que [texx]x\equiv y[/texx] se cumple si y sólo si [texx]x[/texx] e [texx]y[/texx] son el mismo objeto).



Funtores En un universo dado [texx]U[/texx], además de relaciones, podemos considerar funciones [texx]n[/texx]-ádicas, es decir, criterios [texx]f[/texx] que a cada [texx]n[/texx] objetos de [texx]U[/texx] repetidos o no y en un cierto orden les asigne un nuevo objeto de [texx]U[/texx] que representaremos por [texx]f(x_1,\ldots, x_n)[/texx].

Los signos de un lenguaje formal que, en caso de ser interpretados, deben tener asignado como significado una función [texx]n[/texx]-ádica se llaman funtores [texx]n[/texx]-ádicos.

Por ejemplo, podemos añadir a nuestro lenguaje un funtor monádico [texx]P[/texx] cuyo significado sea la función monádica [texx]\overline P[/texx] dada por

[texx]\overline P(x)=\left\{\begin{array}{cl}\text{el padre de } x & \text{si el padre de } x \text{ está en } U\\ x&\text{en caso contrario.}\end{array}\right.[/texx]

De este modo, [texx]N=Pn[/texx] es una afirmación verdadera en nuestro lenguaje formal (siempre respecto de la interpretación fijada), pues significa que Napoleón I es el padre de Napoleón II.

Como en el caso de los relatores, exigiremos que cada funtor tenga un rango definido (no admitiremos funtores que admitan una cantidad indeterminada de argumentos). Notemos que los funtores [texx]0[/texx]-ádicos serían simplemente las constantes.



Conectores lógicos Los conectores lógicos son signos de naturaleza diferente a las constantes, los relatores y los funtores, porque van a tener siempre la misma interpretación y no admitiremos que se modifique. Además, el significado de un conector lógico no será un objeto, una relación o una función, sino una tabla de verdad.

Por ejemplo, un conector lógico es el negador, al que le reservaremos siempre el signo [texx]\lnot[/texx], y su significado es la tabla:

[texx]\begin{array}{|c|c|}
p&\lnot p\\
\hline
V&F\\
F&V
\end{array}[/texx]

Esto significa que si [texx]p[/texx] es una afirmación de nuestro lenguaje formal, entonces [texx]\lnot p[/texx] es otra afirmación que es falsa cuando [texx]p[/texx] es verdadera y viceversa. Esto se abrevia diciendo que el significado de [texx]\lnot[/texx] es el mismo que el de la palabra castellana "no".

Por ejemplo, [texx]MN[/texx] significa que Napoleón es una mujer, y es una afirmación falsa, mientras que [texx]\lnot MN[/texx] significa que Napoleón no es una mujer, y es una afirmación verdadera.

Los restantes conectores lógicos requieren dos argumentos. Son [texx]\land, \lor, \rightarrow, \leftrightarrow[/texx], se llaman conjuntor, disyuntor, implicador y coimplicador, y sus significados vienen dados por las tablas de verdad:

[texx]\begin{array}{|cc|c|c|c|c|}
p&q&p\land q&p\lor q&p\rightarrow q&p\leftrightarrow q\\
\hline
V&V&V&V&V&V\\
V&F&F&V&F&F\\
F&V&F&V&V&F\\
F&F&F&F&V&V
\end{array}[/texx]

Estas tablas se resumen en que [texx]\land[/texx] significa "y", [texx]\lor[/texx] significa "o", [texx]\rightarrow[/texx] significa "si... entonces" y [texx]\leftrightarrow[/texx] significa "si y sólo si".

Por ejemplo, la afirmación [texx]HJ\rightarrow MN[/texx] es verdadera, pues su significado es "Si Josefina es un hombre entonces Napoleón es una mujer", y esto es cierto, porque la tabla de verdad del implicador asigna el valor "verdadero" al caso en que ambas afirmaciones son falsas.



Variables y cuantificadores Las variables son signos similares a las constantes, pero a los que en ningún caso se asignará un significado fijo. Son el equivalente a los pronombres indefinidos en castellano, como "todo", "alguno", etc.

Así, por ejemplo, [texx]Hx[/texx] significa que "x" es un hombre, y no podemos decir que sea una afirmación verdadera o falsa, pues no está especificado el significado de la variable [texx]x[/texx]. La afirmación [texx]x={\rm Pd}n[/texx] significa que "x" es el padre de Napoleón II, y ahora podemos decir que será verdadera si la variable [texx]x[/texx] se interpreta como Napoleón I, y falsa en cualquier otro caso.

Las variables están pensadas para ser usadas en combinación con los cuantificadores, que son otros dos signos con un significado fijo. Les reservaremos los signos [texx]\forall[/texx] y [texx]\exists[/texx]. El primero se llama cuantificador universal o generalizador y el segundo cuantificador existencial o particularizador.

Cada cuantificador debe ir seguido de una variable, e indica que para que la afirmación sea verdadera, debe serlo para toda interpretación posible de la variable (en el caso del generalizador) o al menos para alguna interpretación posible de la variable (en el caso del particularizador).

Por ejemplo, la afirmación [texx]\exists x\ Hx[/texx] significa que existe al menos un hombre, y es una afirmación verdadera, mientras que [texx]\forall x(Hx\rightarrow \lnot Mx)[/texx] significa que todo [texx]x[/texx] que sea un hombre no puede ser una mujer, y también es una afirmación verdadera.



Los signos lógicos de un lenguaje formal serán aquellos cuya presencia es obligada y su significado es fijo, a saber, los conectores lógicos, el igualador y los cuantificadores. Además, también consideraremos a las variables como signos lógicos.  Los demás signos de un lenguaje formal serán sus signos opcionales, es decir, los signos que un lenguaje puede tener o no y que, en caso de existir, requieren que se les asigne una interpretación si queremos interpretar las afirmaciones en las que aparezcan, ya que no tienen ningún significado fijo asignado. Los signos opcionales son, pues, las constantes, los relatores distintos de igualador y los funtores. Las variables las consideraremos como signos lógicos pues, por una parte, son obligatorios (exigiremos que todo lenguaje formal tenga infinitas variables) y, por otra parte, no hay que fijarles ninguna interpretación.

Ejemplo Vamos a definir ahora otro lenguaje formal distinto del que acabamos de construir. Sus signos opcionales serán dos relatores monádicos [texx]P[/texx] y [texx]B[/texx] y una constante [texx]D[/texx]. En este lenguaje formal podemos considerar las afirmaciones siguientes:

[texx]\forall x(Px\rightarrow Bx)[/texx]
[texx]PD[/texx]
[texx]BD[/texx]

Se trata de la formalización del silogismo del mensaje anterior. Mejor dicho, la formalización de dicho silogismo sería lo que más adelante expresaremos así:

[texx]\forall x(Px\rightarrow Bx), PD\vdash BD[/texx]

Según veremos, aquí dice que la tercera afirmación es consecuencia lógica de las dos primeras. La lógica nos permitirá probar que esto es así sin necesidad de considerar ninguna interpretación de los signos opcionales. No obstante, hay muchas interpretaciones posibles. La que es fiel al significado en castellano del silogismo del mensaje anterior tiene por universo la colección [texx]U[/texx] de todas las palabras griegas, la interpretación del relator [texx]P[/texx] es la relación monádica [texx]\overline P[/texx] en [texx]U[/texx] que cumplen las palabras llamadas properispómenas (que son cierta clase de palabras griegas, como en castellano hay palabras agudas, llanas y esdrújulas), la interpretación del relator [texx]B[/texx] es la relación monádica [texx]\overline B[/texx] que cumplen las palabras barítonas (que son otra clase de palabras griegas) y la interpretación de la constante [texx]D[/texx] es la palabra griega [texx]\overline D\equiv \delta\tilde\omega\rho\omicron\nu[/texx].

Con esta interpretación, el [texx]\forall x[/texx] de la primera afirmación se interpreta como "para toda palabra griega" (pues hemos fijado como universo la colección de las palabras griegas), y la afirmación significa "para toda palabra griega x, si x es properispómena, entonces x es barítona" o, lo que es lo mismo, "toda palabra (griega) properispómena es barítona".

Ahora bien, nada nos impide cambiar completamente la interpretación, tomar como universo la colección de las personas vivas en 2012, interpretar [texx]P[/texx] como "ser español", interpretar [texx]B[/texx] como "ser europeo" e interpretar [texx]D[/texx] como "El rey Juan Carlos I". Entonces, exactamente las mismas afirmaciones del mismo lenguaje formal (que no hemos modificado en nada) se interpretan como el silogismo:

Todo español (vivo en 2012) es europeo,
El rey Juan Carlos I es español (vivo en 2012),
luego el rey Juan Carlos I es europeo.

Este silogismo tiene exactamente la misma forma lógica que el considerado en el mensaje anterior. Esto significa que ambos silogismos son interpretaciones particulares de las mismas fórmulas de un mismo lenguaje formal.

Como hemos dicho al principio de este mensaje, nuestro objetivo aquí era únicamente el de presentar los conceptos principales que vamos a manejar. En los mensajes sucesivos precisaremos todos los conceptos que aquí hemos empleado sin más explicaciones, como el de "afirmación", el de "verdadero", etc.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #2 : 04/03/2013, 22:10:00 pm »

En este mensaje empezaremos a precisar y separar por completo los conceptos sintácticos y semánticos que en el mensaje anterior hemos presentado conjuntamente. Empezamos dando una definición de lenguaje formal que no haga absolutamente ninguna referencia al posible significado de los signos que lo componen:

Definición Un lenguaje formal es una colección de signos arbitrarios divididos arbitrariamente en las categorías que especificamos a continuación:

Variables: Un lenguaje formal debe tener infinitas variables, y cada una de ellas debe tener asociado un único número natural al que llamaremos su índice. Recíprocamente, todo número natural es el índice de una única variable.

Spoiler: Notas (click para mostrar u ocultar)

Constantes: Un lenguaje formal puede tener cualquier cantidad de constantes, desde ninguna hasta infinitas. Si hay un número finito [texx]n[/texx] de ellas, a cada una le corresponderá un número natural (un índice) de [texx]0[/texx] a [texx]n-1[/texx], mientras que si hay infinitas entonces habrá una para cada índice natural.

Relatores: Cada signo clasificado como relator debe tener asociado un número natural no nulo llamado su rango. Los relatores de rango [texx]n[/texx] se llaman relatores [texx]n[/texx]-ádicos. Un lenguaje formal puede tener cualquier cantidad de relatores [texx]n[/texx]-ádicos, desde ninguno hasta infinitos, pero si los hay cada uno de ellos debe estar identificado por un índice, que varíe entre los primeros números naturales (si hay un número finito de relatores [texx]n[/texx]-ádicos) o en todos los números naturales, si hay infinitos.

La única excepción a lo dicho es que todo lenguaje formal debe tener el relator diádico de índice [texx]0[/texx], al que llamaremos igualador y representaremos por [texx]=[/texx].

Funtores: Todo lo dicho para los relatores vale igualmente para los funtores, salvo que no hay ningún funtor obligatorio.

Conectores lógicos: Todo lenguaje formal debe tener dos signos llamados conectores lógicos, a saber, el negador [texx]\lnot[/texx] y el implicador [texx]\rightarrow[/texx].

Spoiler: Nota (click para mostrar u ocultar)

Generalizador: Todo lenguaje formal debe tener un signo llamado generalizador y que representaremos por [texx]\forall[/texx].

Se entiende que cada signo de un lenguaje formal debe estar clasificado en una única de estas categorías y cumplir los requisitos indicados.

Observemos que en la definición anterior no hay la menor alusión al significado posible de los signos de un lenguaje formal. Por ejemplo, no decimos que [texx]\forall[/texx] significa "para todo". Simplemente especificamos que [texx]\forall[/texx] es un signo obligatorio en todo lenguaje formal.

Ejemplo: Para definir un lenguaje formal basta especificar sus signos opcionales (sus constantes, relatores y funtores) Por ejemplo, podemos llamar [texx]\mathcal L_0[/texx] al lenguaje formal cuyos signos opcionales son una constante [texx]D[/texx] (que tendrá índice [texx]0[/texx]) y dos relatores monádicos [texx]P[/texx] y [texx]B[/texx] (de índices [texx]0[/texx] y [texx]1[/texx] respectivamente).

Con esto [texx]\mathcal L_0[/texx] queda completamente determinado. Sus signos son los indicados además de las variables [texx]x_0, x_1, x_2, \ldots[/texx] y los signos lógicos [texx]=, \lnot, \rightarrow, \forall[/texx].



Una vez definido el concepto de lenguaje formal sin hacer referencia a los posibles significados de los signos, podemos definir el concepto de modelo de un lenguaje formal, que es una asignación de significados:

Definición: Un modelo [texx]M[/texx] de un lenguaje formal [texx]\mathcal L[/texx] está determinado por:

Un universo [texx]U[/texx], es decir, una colección no vacía bien definida de objetos cualesquiera.

Un criterio que a cada constante [texx]c[/texx] de [texx]\mathcal L[/texx] le asigna un objeto [texx]\overline c[/texx] de [texx]U[/texx], al que llamaremos objeto denotado por [texx]c[/texx] respecto a [texx]M[/texx] o, simplemente, el significado de la constante [texx]c[/texx] (en el modelo [texx]M[/texx]).

Un criterio que a cada relator [texx]n[/texx]-ádico [texx]R[/texx] de [texx]\mathcal L[/texx] le asigne una relación [texx]n[/texx]-ádica [texx]\overline R[/texx] en el universo [texx]U[/texx], que será el significado del relator [texx]R[/texx] en el modelo [texx]M[/texx]. La relación asociada al igualador [texx]=[/texx] será obligatoriamente la relación [texx]\equiv[/texx] de identidad en [texx]U[/texx], es decir, la relación tal que [texx]a\equiv b[/texx] se cumple exactamente cuando [texx]a[/texx] y [texx]b[/texx] son el mismo objeto.

Un criterio que a cada funtor [texx]n[/texx]-ádico [texx]f[/texx] de [texx]\mathcal L[/texx] le asigne una función [texx]n[/texx]-ádica [texx]\overline f[/texx] en el universo [texx]U[/texx], que será el significado del funtor [texx]f[/texx] en el modelo [texx]M[/texx].

Ejemplo: Un modelo para el lenguaje formal [texx]\mathcal L_0[/texx] que hemos definido antes puede ser el especificado como sigue: el universo del modelo es el conjunto de personas vivas en el año 2012, el objeto denotado por la constante [texx]D[/texx] es el rey de España, la relación [texx]\overline P[/texx] asociada al relator [texx]P[/texx] es la relación "ser español" y la relación [texx]\overline B[/texx] asociada al relator [texx]B[/texx] es la relación "ser europeo".

Spoiler: Nota (click para mostrar u ocultar)



Términos y fórmulas Cuando escribimos consecutivamente un número finito de signos de un lenguaje formal [texx]\mathcal L[/texx] tenemos lo que se llama una cadena de signos de [texx]\mathcal L[/texx]. Por ejemplo, una cadena de signos del lenguaje que hemos definido más arriba es:

[texx]==\forall\lnot BBP\rightarrow[/texx]

Concretamente, se trata de una cadena de longitud 8 (la longitud de una cadena de signos es simplemente el número de signos que contiene, contando varias veces los signos repetidos).

De entre todas las cadenas de signos posibles, vamos a especificar las que llamaremos términos y fórmulas. En términos imprecisos, un término es una cadena de signos que nombra a un objeto, mientras que una fórmula es una cadena de signos que afirma algo, pero estas "definiciones" aparte de que no son suficientemente específicas, hacen referencia al posible significado de las cadenas de signos, y eso las vuelve completamente inaceptables. Queremos una definición de "término" y "fórmula" que no use más que los conceptos que aparecen en la definición de lenguaje formal, sin hacer referencia para nada a los significados que aporta un modelo dado.

Definición Diremos que una cadena de signos [texx]t[/texx] de un lenguaje formal [texx]\mathcal L[/texx] es un término si existe una sucesión de cadenas de signos [texx]t_1,\ldots, t_m[/texx] tal que [texx]t\equiv t_m[/texx] y cada [texx]t_i[/texx] es una variable, una constante, o bien se obtiene yuxtaponiendo un funtor [texx]n[/texx]-ádico [texx]f[/texx] de [texx]\mathcal L[/texx] con [texx]n[/texx] elementos anteriores de la sucesión.

De este modo: toda variable y toda constante de [texx]\mathcal L[/texx] es un término, y si [texx]t_1,\ldots, t_n[/texx] son términos de [texx]\mathcal L[/texx] y [texx]f[/texx] es un funtor [texx]n[/texx]-ádico, se cumple que [texx]ft_1\cdots t_n[/texx] también es un término de [texx]\mathcal L[/texx] (pues podemos construirlo encadenando las sucesiones de términos que definen a cada [texx]t_i[/texx] y luego añadiendo [texx]ft_1\cdots t_n[/texx]. La sucesión así obtenida satisface la definición precedente).

Ejemplo: Llamaremos lenguaje de la aritmética al lenguaje [texx]\mathcal L_a[/texx] cuyos signos opcionales son una constante [texx]0[/texx], un funtor monádico [texx]S[/texx] y dos funtores diádicos [texx]f_+[/texx] y [texx]f_\times[/texx].

Adoptamos el convenio de notación consistente en que, en lugar de escribir [texx]f_+t_1t_2[/texx] o [texx]f_\times t_1t_2[/texx], como exige la definición de término, escribiremos [texx](t_1+t_2)[/texx] y [texx](t_1\cdot t_2)[/texx] respectivamente.

Entonces, algunos ejemplos de términos de [texx]\mathcal L_a[/texx] son las cadenas de signos siguientes:

[texx]0,\quad S0, \quad SS0,\quad (S0+SS0),\quad (SS0\cdot(S0+SS0))[/texx].

Por ejemplo, la primera de estas cadenas es un término porque es una constante, la segunda es un término porque consta del funtor monádico [texx]S[/texx] seguido del término [texx]0[/texx], la tercera es un término porque consta del funtor monádico [texx]S[/texx] seguido del término [texx]S0[/texx], la cuarta es un término porque consta del funtor diádico [texx]f_+[/texx] seguido de los términos [texx]S0[/texx] y [texx]SS0[/texx]. (Sólo que, según hemos acordado, en lugar de escribir [texx]f_+S0SS0[/texx] escribimos [texx](S0+SS0)[/texx]) y la última cadena es un término porque consta del funtor diádico [texx]f_\times[/texx] seguido de los términos [texx]SS0[/texx] y [texx](S0+SS0)[/texx].

Definición: Una cadena de signos [texx]\alpha[/texx] de un lenguaje formal [texx]\mathcal L[/texx] es una fórmula si existe una sucesión de cadenas de signos [texx]\alpha_1,\ldots, \alpha_m[/texx] tal que [texx]\alpha\equiv \alpha_m[/texx] y cada cadena de la sucesión es de una de estas formas:

a) [texx]Rt_1,\ldots, t_n[/texx], donde [texx]R[/texx] es un relator [texx]n[/texx]-ádico de [texx]\mathcal L[/texx] y [texx]t_1,\ldots, t_n[/texx] son términos de [texx]\mathcal L[/texx]. (En la práctica escribiremos [texx](t_1=t_2)[/texx] en lugar de [texx]=t_1t_2[/texx].)

b) [texx]\lnot \beta[/texx], donde [texx]\beta[/texx] es una cadena anterior en la sucesión. (En la práctica escribiremos [texx](t_1\neq t_2)[/texx] en lugar de [texx]\lnot(t_1=t_2)[/texx].)

c) [texx]\rightarrow \beta\gamma[/texx], donde [texx]\beta[/texx] y [texx]\gamma[/texx] son cadenas anteriores de la sucesión. (En la práctica escribiremos [texx](\beta \rightarrow \gamma)[/texx] en lugar de [texx]\rightarrow \beta\gamma[/texx].)

d) [texx]\forall x\beta[/texx], donde [texx]x[/texx] es una variable y [texx]\beta[/texx] es una cadena anterior de la sucesión.

Spoiler: Nota técnica (click para mostrar u ocultar)
Por lo tanto:

Al escribir un relator [texx]n[/texx]-ádico seguido de [texx]n[/texx] términos obtenemos una fórmula (aunque cuando el relator sea el igualador lo escribiremos en medio de los términos, y no delante).

Si [texx]\beta[/texx] es una fórmula, [texx]\lnot \beta[/texx] también es una fórmula (porque si prolongamos con [texx]\lnot\beta[/texx] la sucesión que justifica que [texx]\beta[/texx] es una fórmula obtenemos una justificación de que [texx]\lnot\beta[/texx] es una fórmula).

Si [texx]\beta[/texx] y [texx]\gamma[/texx] son fórmulas, también lo es [texx]\rightarrow\beta\gamma[/texx] (aunque en la práctica escribiremos [texx](\beta\rightarrow \gamma)[/texx]. Esto es porque si encadenamos las sucesiones que justifican que [texx]\beta[/texx] y [texx]\gamma[/texx] son fórmulas y luego escribimos  [texx](\beta\rightarrow \gamma)[/texx] tenemos una sucesión que justifica que  [texx](\beta\rightarrow \gamma)[/texx] es una fórmula.

Si [texx]\beta[/texx] es una fórmula y [texx]x[/texx] es una variable, entonces [texx]\forall x\beta[/texx] es una fórmula, pues si prolongamos con [texx]\forall x\beta[/texx]  la sucesión que justifica que [texx]\beta[/texx] es una fórmula obtenemos una sucesión que justifica que [texx]\forall x\beta[/texx] también lo es.

Ejemplo: La sucesión siguiente de cadenas de signos justifica que la última de ellas (y, de hecho, también todas las anteriores) es una fórmula del lenguaje [texx]\mathcal L_a[/texx]:

[texx]x=Sy[/texx] (un relator diádico actuando sobre dos términos).

[texx]x=0[/texx] (ídem)

[texx]x\neq 0[/texx] (negación de la fórmula precedente)

[texx](x=Sy\rightarrow x\neq 0)[/texx] (implicación de dos fórmulas precedentes)

[texx]\forall y(x=Sy\rightarrow x\neq 0)[/texx] (generalización de una fórmula precedente)

[texx]\forall x\forall y(x=Sy\rightarrow x\neq 0)[/texx] (generalización de una fórmula precedente).

En la práctica, cuando haya varios cuantificadores seguidos, como en la última fórmula, los abreviaremos escribiendo [texx]\forall xy(x=Sy\rightarrow x\neq 0)[/texx].



Hemos definido el lenguaje de la aritmética [texx]\mathcal L_a[/texx], pero no le hemos asociado ningún modelo. El modelo natural de [texx]\mathcal L_a[/texx] es el modelo que tiene por universo el conjunto de los números naturales, en el que el significado de la constante [texx]0[/texx] es el número natural cero, el significado del relator [texx]S[/texx] es la función que a cada número natural le asigna el número siguiente, y los significados de los funtores diádicos [texx]f_+[/texx] y [texx]f_\times[/texx] son las funciones de suma y producto de números naturales, respectivamente.

En este modelo "está claro" que la fórmula [texx]\forall xy(x=Sy\rightarrow x\neq 0)[/texx] significa que si un número natural es el siguiente de otro, entonces no puede ser el número natural cero. En el mensaje siguiente explicitaremos este "hecho claro", es decir, veremos cómo asociar un significado a cada término y a cada fórmula de un lenguaje formal respecto a un modelo prefijado. Sin embargo, es un hecho fundamental que aquí hemos definido los conceptos de "término" y "fórmula" sin hacer referencia en ningún momento a posibles modelos de un lenguaje formal.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #3 : 05/03/2013, 20:29:52 pm »

Antes de seguir adelante hagamos un resumen de lo que tenemos hasta ahora. Cualquiera que vea estas dos cadenas de signos:

[texx]\forall\forall \lnot\rightarrow xy=[/texx],    [texx]\forall xy(x=Sy\rightarrow x\neq 0)[/texx]

se da cuenta de forma inmediata que la primera es un galimatías, mientras que la segunda tiene sentido.

Lo que hemos visto en el mensaje anterior es que

1) Esa distinción que sabemos hacer a simple vista, incluso sin saber explicar en qué notamos la diferencia, puede describirse mediante unas reglas muy simples, que pueden ser fácilmente programadas para que un ordenador distinga entre cadenas con y sin sentido (es decir, entre términos y fórmulas y galimatías).

2) La distinción entre cadenas con y sin sentido puede hacerse sin hacer referencia para nada al sentido (el significado posible) de las cadenas de signos, atendiendo únicamente a la forma en que están ordenados los distintos signos (es decir, formalmente, atendiendo a la forma y no al significado).

En particular hemos descrito la estructura formal de los términos y las fórmulas, que se resume en lo siguiente:

1) Cada término de un lenguaje formal es una variable, una constante o un funtor n-ádico seguido de n términos.

2) Cada fórmula de un lenguaje formal es un relator n-ádico seguido de n términos, o bien un negador seguido de una fórmula, o bien un implicador seguido de dos fórmulas (aunque en la práctica escribimos el implicador en medio de ambas) o bien un generalizador seguido de una variable y una fórmula (aunque en la práctica simplifiquemos a veces la escritura, como al escribir [texx]\forall xy[/texx] en lugar de [texx]\forall x\forall y[/texx]).

Para acabar de sentar las bases más elementales de la lógica nos falta ver que otra acción que sabemos hacer instintivamente puede ser descrita también de forma "entendible para ordenadores". Me refiero a "leer", "entender el significado". Por ejemplo, cuando vemos la fórmula escrita más arriba, si suponemos una interpretación de su lenguaje formal cuyo universo sea el conjunto de los números naturales y en la que el objeto denotado por la constante [texx]0[/texx] sea el número cero y la función denotada por el funtor [texx]S[/texx] sea la operación sucesor, inmediatamente "entendemos" que la fórmula dice que el sucesor de un número natural no puede ser el cero. Más precisamente, ¿qué relación hay entre estas dos afirmaciones?:

[texx]\color{blue} \forall xy(x=Sy\rightarrow x\neq 0)[/texx]

El sucesor de un número natural no puede ser el cero.

La respuesta es que la relación entre la primera y la segunda es la misma que entre la segunda y ésta otra:

The successor of a natural number cannot be zero.

Las tres son versiones de la misma afirmación en tres idiomas diferentes: un cierto lenguaje formal, el castellano y el inglés. Las tres tienen perfecto sentido en su propio lenguaje, y las tres tienen el mismo significado, pasar de una a otra cualquiera es lo que se conoce como "traducir". Ahora bien, así como traducir del castellano al inglés es un arte que los ordenadores distan mucho de dominar, traducir de un lenguaje formal al castellano es una labor puramente mecánica que ahora vamos a describir.

Cabe señalar que no toda afirmación castellana puede traducirse a un determinado lenguaje formal, pues un lenguaje formal puede tener únicamente signos específicos para hablar de conceptos muy concretos, mientras que toda afirmación de un lenguaje formal puede traducirse al castellano (supuesto que se haya fijado un modelo del lenguaje formal). Cuando una afirmación castellana puede traducirse a un lenguaje formal decimos que es formalizable en dicho lenguaje, y formalizar afirmaciones castellanas es el primer paso para poder estudiarlas desde el punto de vista de la lógica.

En definitiva, lo que nos preguntamos ahora es ¿qué es exactamente el significado de un término o de una fórmula (respecto de un modelo)?

Para responder a esta pregunta necesitamos asignar un significado provisional a las variables de un lenguaje formal, que, precisamente por ser "variables" no tienen asignado en principio ningún significado fijo:

Definición: Sea [texx]\mathcal L[/texx] un lenguaje formal y sea [texx]M[/texx] un modelo de [texx]\mathcal L[/texx]. Una valoración de [texx]\mathcal L[/texx] en [texx]M[/texx] es cualquier criterio [texx]v[/texx] que a cada variable [texx]x[/texx] de [texx]\mathcal L[/texx] le asigne un objeto [texx]v(x)[/texx] del universo de [texx]M[/texx].

En definitiva, una valoración asigna a cada variable un "significado provisional", como hemos dicho.

Si [texx]v[/texx] es una valoración, [texx]x[/texx] es una variable y [texx]a[/texx] es un objeto del universo de [texx]M[/texx], representaremos por [texx]v_x^a[/texx] la valoración que coincide con [texx]v[/texx] salvo que [texx]v_x^a(x)\equiv a[/texx], independientemente de lo que valga [texx]v(x)[/texx].

Ahora ya podemos definir el objeto denotado por (es decir, el significado de) un término:

Definición: Sea [texx]\mathcal L[/texx] un lenguaje formal, sea [texx]M[/texx] un modelo de [texx]\mathcal L[/texx] y sea [texx]v[/texx] una valoración en [texx]M[/texx]. Cada término [texx]t[/texx] de [texx]\mathcal L[/texx] tiene asignado un objeto [texx]\overline t[/texx] del universo de [texx]M[/texx] (al que llamaremos objeto denotado por [texx]t[/texx], respecto de [texx]M[/texx] y [texx]v[/texx]) mediante las reglas siguientes:

Si [texx]x[/texx] es una variable, entonces el objeto que denota es [texx]\bar x = v(x)[/texx].

Si [texx]c[/texx] es una constante, entonces el objeto [texx]\overline c[/texx] que denota es el fijado por el modelo [texx]M[/texx].

Si [texx]t = ft_1\ldots t_n[/texx] es un término compuesto por un funtor [texx]n[/texx]-ádico seguido de [texx]n[/texx] términos, entonces su objeto denotado es [texx]\overline t = \overline f(\overline{t_1},\ldots, \overline{t_n})[/texx], es decir, es el objeto que resulta de aplicar la función denotada por [texx]f[/texx] (dada por el modelo) sobre los objetos denotados por los términos [texx]t_1,\ldots, t_n[/texx].

Cuando queramos indicar que [texx]\overline t[/texx] depende de [texx]M[/texx] y [texx]v[/texx] escribiremos [texx]\overline t = M(t)[v][/texx].

Notemos que el cálculo de el objeto denotado por un término requiere calcular previamente los objetos denotados por los términos menores que contenga, pero como éstos son necesariamente un número finito, es claro que el proceso para calcular dicho objeto denotado es siempre finito.

Ejemplo: Consideremos el término [texx]SS0+S0[/texx] del lenguaje [texx]\mathcal L_a[/texx] de la aritmética y vamos a calcular el objeto que denota respecto de su modelo natural.

Para ello observamos que [texx]\overline 0[/texx] es el número natural cero, pues el objeto denotado por una constante es el que le asigna el modelo, y el modelo natural de [texx]\mathcal L_a[/texx] establece que la constante [texx]0[/texx] denota al cero.

A continuación calculamos [texx]\overline{S0} = \overline S(\overline 0)[/texx]. Como la función [texx]\overline S[/texx] es la función sucesor (por la definición del modelo) y ya sabemos que [texx]\overline 0[/texx] es el cero, concluimos que [texx]\overline{S0}[/texx] es el sucesor del número cero, es decir, el número uno.

Igualmente concluimos que [texx]\overline{SS0}[/texx] es el número dos.

Por último, el término [texx]SS0+S0[/texx] es lo que, sin el abuso de notación de poner el funtor en medio, sería [texx]f_+SS0S0[/texx], es decir, el funtor diádico [texx]f_+[/texx] (que denota en el modelo a la función suma de números naturales) seguido de los términos [texx]SS0[/texx] y [texx]S0[/texx]. Por lo tanto [texx]\overline{SS0+S0}[/texx] es el número que resulta de aplicar la función suma [texx]\overline{f_+}[/texx] a los números [texx]\overline{SS0}[/texx] y [texx]\overline{S0}[/texx], es decir, la suma de dos más uno, o sea, tres. Concluimos que  [texx]\overline{SS0+S0}[/texx] es el número natural tres.

Ahora pasamos a definir el significado de una fórmula o, equivalentemente, qué significa exactamente que una fórmula dada sea verdadera o falsa (respecto de un modelo). La presencia de valoraciones hace que evitemos de momento las palabras "verdadero" y "falso" y hablemos más bien de si una fórmula es satisfecha o no por una valoración en un modelo.

Definición:  Sea [texx]\mathcal L[/texx] un lenguaje formal, sea [texx]M[/texx] un modelo de [texx]\mathcal L[/texx] y sea [texx]v[/texx] una valoración en [texx]M[/texx]. Diremos que una fórmula [texx]\alpha[/texx] de [texx]\mathcal L[/texx] es satisfecha en [texx]M[/texx] por la valoración [texx]v[/texx] (y lo representaremos [texx]M\vDash \alpha[v][/texx]) si se cumple lo siguiente, según la estructura de [texx]\alpha[/texx]:

1) [texx]M\vDash Rt_1\cdots t_n[v][/texx] si y sólo si [texx]\overline R(\overline{t_1},\ldots, \overline{t_n})[/texx], es decir, una fórmula del tipo "relator seguido de términos" es satisfecha si la relación asociada al relator por el modelo se cumple sobre los objetos denotados por los términos. En particular, [texx]M\vDash (t_1=t_2)[v][/texx] equivale a que los objetos denotados por [texx]t_1[/texx] y [texx]t_2[/texx] sean el mismo (porque la relación denotada por [texx]=[/texx] es la identidad).

2) [texx]M\vDash \lnot \alpha [v][/texx] si y sólo si no [texx]M\vDash \alpha[v][/texx], es decir, una fórmula de tipo [texx]\lnot \alpha[/texx] es satisfecha si y sólo si la fórmula [texx]\alpha[/texx] no es satisfecha.

3) [texx]M\vDash (\alpha\rightarrow \beta) [v][/texx] si y sólo si no [texx]M\vDash \alpha[v][/texx] o bien [texx]M\vDash \beta[v][/texx] o, equivalentemente, [texx]\alpha\rightarrow \beta[/texx] es satisfecha salvo si [texx]\alpha[/texx] es satisfecha y [texx]\beta[/texx] no lo es.

4) [texx]M\vDash \forall x\alpha[v][/texx] si y sólo si para todo objeto [texx]a[/texx] del universo de [texx]M[/texx] se cumple que [texx]M\vDash \alpha[v_x^a][/texx], es decir, si la fórmula [texx]\alpha[/texx] es satisfecha, no sólo por la valoración [texx]v[/texx], sino también por cualquier valoración en la que la variable [texx]x[/texx] denote cualquier objeto [texx]a[/texx] posible. En otras palabras, [texx]\forall x\alpha[/texx] es satisfecha si y sólo si [texx]\alpha[/texx] es satisfecha cualquiera que sea la interpretación de la variable [texx]x[/texx].

Spoiler: Nota (click para mostrar u ocultar)

Ejemplo: Considerando el modelo natural de [texx]\mathcal L_a[/texx] y una valoración cualquiera [texx]v[/texx], nos preguntamos a qué equivale exactamente

[texx]M\vDash \forall xy(x=Sy\rightarrow x\neq 0)[v][/texx]

Ya sabemos la respuesta: equivale a que un número natural que sea el sucesor de otro no puede ser cero, pero vamos a comprobar que esto es precisamente lo que obtenemos cuando aplicamos la definición precedente.

Por el punto 4) sabemos que [texx]M\vDash \forall xy(x=Sy\rightarrow x\neq 0)[v][/texx] equivale a que, para todo objeto [texx]a[/texx] del universo de [texx]M[/texx], es decir, para todo número natural [texx]a[/texx], se cumpla

[texx]M\vDash \forall y(x=Sy\rightarrow x\neq 0)[v_x^a][/texx].

De nuevo por 4) sabemos que esto equivale a que para todo número natural [texx]b[/texx] se cumpla que

[texx]M\vDash (x=Sy\rightarrow x\neq 0)[v_{xy}^{ab}][/texx].

Por 3) esto equivale a que para todos los números naturales [texx]a[/texx] y [texx]b[/texx], o bien no se cumple [texx]M\vDash(x=Sy)[v_{xy}^{ab}][/texx], o bien [texx]M\vDash (x\neq 0)[v_{xy}^{ab}][/texx]. Equivalentemente, esto es tanto como afirmar que si se cumple [texx]M\vDash(x=Sy)[v_{xy}^{ab}][/texx], también se ha de cumplir [texx]M\vDash (x\neq 0)[v_{xy}^{ab}][/texx].

Por 1) y 2) esto equivale a que, para todo par de números naturales [texx]a[/texx] y [texx]b[/texx], supuesto que cumplan [texx]M(x)[v_{xy}^{ab}]\equiv M(Sy)[v_{xy}^{ab}][/texx], también deben cumplir que no [texx]M\vDash (x=0)[v_{xy}^{ab}][/texx].

Ahora tenemos en cuenta que el objeto denotado por [texx]x[/texx] respecto a la valoración [texx]v_{xy}^{ab}[/texx] es [texx]v_{xy}^{ab}(x)\equiv a[/texx], mientras que el objeto denotado por [texx]Sy[/texx] es el siguiente del número denotado por [texx]y[/texx], que es [texx]v_{xy}^{ab}(y)\equiv b[/texx]. Por lo tanto tenemos:

Para todo par de números naturales [texx]a[/texx] y [texx]b[/texx], si [texx]a[/texx] es el siguiente de [texx]b[/texx], entonces no se cumple que [texx]M(x)[v_{xy}^{ab}]\equiv M(0)[v_{xy}^{ab}][/texx]. En definitiva:

Para todo par de números naturales [texx]\color{blue} a[/texx] y [texx]\color{blue} b[/texx], si [texx]\color{blue} a[/texx] es el siguiente de [texx]\color{blue} b[/texx], entonces [texx]\color{blue} a[/texx] no es cero.

Así pues, lo que obtenemos después de morirnos de asco aplicando metódicamente la definición de satisfacción es lo que cualquiera capta de un golpe de vista al mirar la fórmula de partida. Obviamente, en la práctica es absurdo seguir todo este camino para llegar a lo evidente. El interés de la definición de satisfacción es que nos permite estudiar el concepto teóricamente con la garantía de que estamos hablando de lo mismo que hacemos en la práctica cuando "entendemos" el significado de una fórmula.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #4 : 09/03/2013, 18:54:18 pm »

Nuestra descripción básica de los lenguajes formales no puede estar completa si no introducimos de algún modo los "signos perdidos" que hemos omitido en la definición bajo la promesa de recuperarlos más tarde, a saber, el conjuntor, el disyuntor, el coimplicador y el cuantificador existencial.

Si tenemos dos fórmulas [texx]\alpha[/texx] y [texx]\beta[/texx], definimos

[texx]\alpha\lor \beta\equiv \lnot\alpha\rightarrow \beta[/texx]

Aquí hay que destacar que esta definición no es "caprichosa" o arbitraria. Por el contrario, esta definición es la que tiene que ser para que el conjuntor [texx]\lor[/texx] que acabamos de definir tenga por tabla de verdad la correspondiente a la disyunción, es decir, a la conjunción "o" (no exclusiva) castellana.

En efecto, Si fijamos un modelo [texx]M[/texx] de un lenguaje formal y una valoración [texx]v[/texx], tenemos que

[texx]M\vDash(\alpha\lor \beta)[v][/texx] es lo mismo que [texx]M\vDash(\lnot\alpha\rightarrow \beta)[v][/texx], lo cual sucede si y sólo si no [texx]M\vDash \lnot\alpha[v][/texx] o [texx]M\vDash \beta[v][/texx], lo cual sucede si y sólo si [texx]M\vDash \alpha[v][/texx] o [texx]M\vDash \beta[v][/texx].

Puesto que los conectores [texx]\lnot[/texx] y [texx]\rightarrow[/texx] tienen siempre la misma interpretación en todos los modelos (la dada por sus respectivas tablas de verdad) acabamos de probar que [texx]\lor[/texx] tiene siempre la misma interpretación en todos los modelos, de modo que una fórmula [texx]\alpha\lor\beta[/texx] es satisfecha cuando y sólo cuando lo es al menos una de las dos fórmulas [texx]\alpha[/texx] y [texx]\beta[/texx].

Si hubiéramos optado por introducir el disyuntor [texx]\lor[/texx] como un signo lógico obligatorio más de todo lenguaje formal (en igualdad de condiciones que el negador y el implicador), en la definición de satisfacción habríamos tenido que añadir que una fórmula [texx]\alpha\lor \beta[/texx] es satisfecha si y sólo si al menos una de las dos [texx]\alpha[/texx] o [texx]\beta[/texx] lo es. Y en tal caso las fórmulas [texx]\alpha\lor \beta[/texx] y [texx]\lnot\alpha\rightarrow \beta[/texx] no serían la misma fórmula (como lo son según el convenio que hemos adoptado), sino que serían un ejemplo de un par de fórmulas lógicamente equivalentes, es decir, dos fórmulas tales que una es satisfecha por una valoración en un modelo si y sólo si lo es la otra.

Análogamente podemos definir el conjuntor mediante:

[texx]\alpha\land \beta\equiv \lnot(\lnot\alpha\lor\lnot\beta)[/texx].

Si ahora analizamos cuándo sucede [texx]M\vDash (\alpha\land\beta)[v][/texx], según la definición de satisfacción y el resultado que acabamos de probar para la satisfacción del disyuntor, concluiremos fácilmente que [texx]M\vDash (\alpha\land\beta)[v][/texx] se cumple cuando y sólo cuando [texx]M\vDash \alpha[v][/texx] y [texx]M\vDash \beta[v][/texx], lo que demuestra que la tabla de verdad asociada al conjuntor es precisamente la que corresponde a la conjunción castellana "y".

Igualmente podemos (o, mejor, debemos) definir el coimplicador como

[texx]\alpha\leftrightarrow \beta \equiv (\alpha\rightarrow\beta)\land (\beta\rightarrow \alpha)[/texx].

Nuevamente, esta definición no es "caprichosa", sino que es la necesaria para que la tabla de verdad del coimplicador sea la esperada.

Consideremos por último el caso del cuantificador existencial o particularizador:

[texx]\exists x\alpha\equiv\lnot \forall x\lnot \alpha[/texx].

Veamos con detalle su interpretación. Si fijamos un modelo [texx]M[/texx] y una valoración [texx]v[/texx] tenemos que [texx]M\vDash \exists x\alpha[v][/texx] es lo mismo que [texx]M\vDash \lnot \forall x\lnot \alpha[v][/texx], lo cual, por definición de satisfacción, equivale a que no [texx]M\vDash \forall x\lnot \alpha[v][/texx]. Esto, a su vez equivale a que no se cumpla para todo [texx]a[/texx] en el universo del modelo,  [texx]M\vDash \lnot\alpha[v_x^a] [/texx].

Decir que esto no se ha de cumplir para todo [texx]a[/texx] es lo mismo que decir que existe un [texx]a[/texx] en el universo del modelo que no cumple [texx]M\vDash \lnot\alpha[v_x^a] [/texx], o también que existe un [texx]a[/texx] en el universo del modelo que cumple [texx]M\vDash \alpha[v_x^a] [/texx].

Ésta es la interpretación del cuantificador existencial: se cumple [texx]M\vDash \exists x\alpha[v][/texx] si y sólo si existe un objeto [texx]a[/texx] en el universo del modelo tal que [texx]\alpha[/texx] es satisfecha si modificamos la valoración para que la variable [texx]x[/texx] se interprete como [texx]a[/texx].

Dicho más laxamente, [texx]\exists x\alpha[/texx] es satisfecha si existe una posible interpretación para la variable [texx]x[/texx] que hace que [texx]\alpha[/texx] sea satisfecha.

Así, la definición de [texx]\exists[/texx] no es caprichosa, sino que es la necesaria para que [texx]\exists x[/texx] signifique "existe un [texx]x[/texx]". Si hubiéramos introducido el cuantificador existencial como un signo más de los lenguajes formales (en lugar de definirlo luego a partir del cuantificador universal), entonces habría que haber añadido a la definición de satisfacción que [texx]M\vDash \exists x\alpha[v][/texx] equivale a lo que acabamos de probar, y entonces las fórmulas [texx]\exists x\alpha[/texx] y [texx]\lnot\forall x\lnot\alpha[/texx] no serían la una una abreviatura de la otra, sino que serían dos fórmulas distintas, pero lógicamente equivalentes.

Para terminar destacamos que las definiciones

[texx]\alpha\lor \beta\equiv \lnot\alpha\rightarrow \beta[/texx], [texx]\alpha\land \beta\equiv \lnot(\lnot\alpha\lor\lnot\beta)[/texx], [texx]\alpha\leftrightarrow \beta \equiv (\alpha\rightarrow\beta)\land (\beta\rightarrow \alpha)[/texx] y [texx]\exists x\alpha\equiv\lnot \forall x\lnot \alpha[/texx]

son puramente sintácticas, es decir, que no dependen para nada de ningún posible modelo del lenguaje formal. Una vez dadas podemos determinar (como hemos hecho) el significado de los nuevos signos lógicos en cualquier modelo, pero todos ellos están definidos sin hacer referencia a modelos (ni, por lo tanto, a su posible significado).
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #5 : 12/03/2013, 18:34:48 pm »

Consideremos una fórmula como

[texx]\exists y\ x = Sy[/texx].

En esta fórmula la variable [texx]x[/texx] está libre, mientras que la variable [texx]y[/texx] está ligada. En general, se dice que una variable está libre en una fórmula cuando aparece en ella, pero no está afectada por ningún cuantificador, mientras que en caso contrario se dice que está ligada. Hay que tener en cuenta que una misma variable puede estar a la vez libre y ligada en una fórmula. Es el caso, por ejemplo, de la variable [texx]x[/texx] en

[texx]x= 0\land \exists x\ x = S0[/texx]

Aquí la primera [texx]x[/texx] está libre, mientras que la segunda está ligada. Estas indicaciones bastan para que cualquiera sepa distinguir qué variables están libres o ligadas en una fórmula cualquiera. No obstante, a efectos de hacer demostraciones conviene observar que estos conceptos satisfacen las relaciones recurrentes siguientes:

1) Las variables libres de un término son exactamente las que aparecen en él. Un término no tiene variables ligadas.

2) Las variables libres de una fórmula de tipo [texx]Rt_1\ldots t_n[/texx] son exactamente las que aparecen en ella, y no tiene variables ligadas.

3) Las variables libres/ligadas de una fórmula de tipo [texx]\lnot \alpha[/texx] son las mismas que las de [texx]\alpha[/texx].

4) Las variables libres/ligadas de una fórmula de tipo  [texx]\alpha\rightarrow \beta[/texx]  son las que están libres/ligadas en [texx]\alpha[/texx] o en [texx]\beta[/texx].

5) Las variables libres en una fórmula de tipo [texx]\forall x\,\alpha[/texx] son las variables libres de [texx]\alpha[/texx] distintas de [texx]x[/texx]; las variables ligadas son las variables ligadas de [texx]\alpha[/texx] y además [texx]x[/texx].

Teniendo en cuenta las definiciones introducidas en el mensaje anterior, de estas reglas se deduce que las variables libres/ligadas en una fórmula de tipo [texx]\alpha\lor\beta[/texx], [texx]\alpha\land \beta[/texx] o [texx]\alpha\leftrightarrow \beta[/texx] son las que están libres/ligadas en [texx]\alpha[/texx] o en [texx]\beta[/texx], así como que la regla 5) es válida si cambiamos [texx]\forall x[/texx] por [texx]\exists x[/texx].

La interpretación semántica del concepto de variable libre es que las variables libres de un término o fórmula son las únicas (a lo sumo) a las que necesitamos asignar una interpretación para determinar el objeto denotado por el término o si la fórmula es o no satisfecha en un modelo. Éste es el contenido de los dos teoremas siguientes:

Teorema: Sea [texx]M[/texx] un modelo de un lenguaje formal [texx]\mathcal L[/texx], sean [texx]v[/texx] y [texx]w[/texx] dos valoraciones en [texx]M[/texx] y sea [texx]t[/texx] un término de [texx]\mathcal L[/texx]. Si [texx]v[/texx] y [texx]w[/texx] coinciden sobre las variables libres en [texx]t[/texx], entonces [texx]M(t)[v]\equiv M(t)[w][/texx].

En otras palabras, que para calcular el objeto denotado [texx]M(t)[v][/texx] sólo necesitamos saber cómo actúa [texx]v[/texx] sobre las variables libres en [texx]t[/texx]. Su actuación sobre las variables que no aparezcan en [texx]t[/texx] es irrelevante.

Spoiler: Demostración (click para mostrar u ocultar)

Teorema: Sea [texx]M[/texx] un modelo de un lenguaje formal [texx]\mathcal L[/texx], sean [texx]v[/texx] y [texx]w[/texx] dos valoraciones en [texx]M[/texx] y sea [texx]\alpha[/texx] una fórmula de [texx]\mathcal L[/texx]. Si [texx]v[/texx] y [texx]w[/texx] coinciden sobre las variables libres en [texx]\alpha[/texx], entonces [texx]M\vDash \alpha[v][/texx] es equivalente a [texx]M\vDash \alpha[w][/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Es útil usar la notación [texx]\alpha(x_1,\ldots, x_n)[/texx] para indicar que las variables libres de [texx]\alpha[/texx] están entre [texx]x_1,\ldots, x_n[/texx] y, en tal caso, escribir [texx]M\vDash \alpha[a_1,\ldots, a_n][/texx] para indicar que se cumple [texx]M\vDash \alpha[v][/texx], donde [texx]v[/texx] es cualquier valoración que cumpla [texx]v(x_i)\equiv a_i[/texx], es decir, que la fórmula [texx]\alpha[/texx] es satisfecha por cualquier valoración que interprete la variable [texx]x_i[/texx] como [texx]a_i[/texx]. Según el teorema anterior, las posibles interpretaciones que dé la valoración a las demás variables es irrelevante.

Definición: Se dice que un término es abierto si tiene variables libres. En caso contrario se dice que es cerrado, o que es un designador. Se dice que una fórmula es [texx]abierta[/texx] si tiene variables libres. En caso contrario se dice que es [texx]cerrada[/texx] o que es una sentencia.

Los dos teoremas anteriores se traducen en que un designador designa a un mismo objeto en cada modelo, que no depende de la valoración que se considere, e igualmente una sentencia es satisfecha o no en un modelo, sin que importe la valoración que se considere.

El tratamiento de las variables libres nos plantea un problema técnico, y es que los matemáticos, en su uso cotidiano, tratan a veces las variables libres como que representan a objetos arbitrarios (y sus conclusiones valen entonces para todo valor de las variables) y a veces como que representan a objetos particulares (y sus conclusiones valen entonces para un cierto valor de las variables). La diferencia depende del contexto. Si un matemático ha empezado un razonamiento diciendo "tomemos un número real arbitrario [texx]x[/texx]", entonces la variable [texx]x[/texx] es genérica, mientras que si la introduce en la forma "podemos asegurar que esta ecuación tiene al menos una solución [texx]x[/texx]", en lo sucesivo "recuerda" que la variable [texx]x[/texx] es particular.

De momento no estamos en condiciones de tener en cuenta estos contextos, así que vamos a adoptar una interpretación "por defecto" de las variables libres (la genérica), pero teniendo en cuenta que más adelante nos las ingeniaremos para considerar variables particulares sin contradecir estrictamente nada de lo que vamos a decir ahora.

Definición: Diremos que una fórmula [texx]\alpha[/texx] es verdadera en un modelo [texx]M[/texx], y lo representaremos por [texx]M\vDash \alpha[/texx], si [texx]M\vDash \alpha[v][/texx] para toda valoración [texx]v[/texx] en el modelo. Diremos que es falsa si no  [texx]M\vDash \alpha[v][/texx] para toda valoración [texx]v[/texx] en el modelo.

En otras palabras, una fórmula [texx]\alpha[/texx] es verdadera si es satisfecha con cualquier valoración o, equivalentemente, con cualquier asignación de significados para sus variables libres, y es falsa si no es satisfecha con ninguna valoración (con cualquier asignación de significados a sus variables libres). Con esta definición se cumple:

Teorema: Si [texx]\alpha[/texx] es una fórmula de un lenguaje formal y [texx]M[/texx] es un modelo de dicho lenguaje, entonces [texx]M\vDash \alpha[/texx] si y sólo si [texx]M\vDash \forall x\alpha[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Por ejemplo, la fórmula [texx]x+y=y+x[/texx] del lenguaje de la aritmética es verdadera en su modelo natural, pues es satisfecha sean cuales sean los números naturales con los que se interpreten las variables [texx]x[/texx] e [texx]y[/texx], y esto es equivalente a que sea verdadera la sentencia [texx]\forall xy(x+y=y+x)[/texx]. Por el contrario, la fórmula [texx]x=Sy[/texx] no es ni verdadera ni falsa, pues es satisfecha con ciertas valoraciones (las que asignan a la variable [texx]x[/texx] el número siguiente al que asignan a la variable [texx]y[/texx]) y no es satisfecha por otras.

Insistimos en que la equivalencia entre

[texx]M\vDash x+y=y+x[/texx] y [texx]M\vDash \forall xy(x+y=y+x)[/texx]

sólo expresa un convenio arbitrario que acabamos de adoptar: que, a efectos de que una fórmula se considere verdadera, debe ser satisfecha con cualquier valoración o, lo que es lo mismo, las variables libres se deben considerar cuantificadas universalmente.

Observemos que si [texx]\alpha[/texx] es una sentencia, entonces, o bien es satisfecha en un modelo por todas las valoraciones o bien no lo es por ninguna, pues hemos demostrado que de la valoración considerada solo influye su actuación sobre las variables libres, y en este caso no las hay. Por lo tanto:

Teorema: Toda sentencia es verdadera o falsa en un modelo dado.

Está claro que las fórmulas:

[texx]\alpha_1\equiv \exists x\ y = Sx[/texx],   [texx]\alpha_2\equiv \exists z\ y = Sz[/texx],   

son equivalentes, en el sentido de que, fijado un modelo y una valoración, [texx]M\vDash \alpha_1[v][/texx] es equivalente a [texx]M\vDash \alpha_2[v][/texx]

Observemos en general que si en una fórmula cambiamos sistemáticamente una variable ligada (y no libre) por otra nueva (es decir, por otra que no esté presente en la fórmula) esto no altera su significado, es decir, que la formula inicial y la final serán ambas satisfechas o no por una valoración dada en un modelo.  La razón es que al interpretar una fórmula no tenemos en cuenta la interpretación que asigna la valoración a una variable ligada, sino que consideramos todas sus interpretaciones posibles (para ver si todas cumplen lo requerido, en el caso de un cuantificador universal, o si alguna lo cumple, en el caso existencial). Esto debería bastar para que uno se convenza de lo dicho, de manera que la demostración tediosa siguiente no debería aportar gran cosa a nadie.

Spoiler: Demostración tediosa (click para mostrar u ocultar)

Esto hace que en cualquier momento podemos cambiar una variable ligada por otra (nueva) sin cambiar el significado de una fórmula. Por ello, se considera "de mal gusto" escribir fórmulas como

[texx]x= 0\land \exists x\ x = S0[/texx]

En su lugar, es preferible escribir

[texx]x= 0\land \exists y\ y = S0[/texx],

para evitar que la variable [texx]x[/texx] deba ser interpretada de dos formas distintas (primero como una variable libre que requiere, para que la fórmula sea satisfecha, una valoración que le asigne como interpretación el cero, y luego como una variable ligada que puede ajustarse como haga falta para que se cumpla la segunda parte, de modo que la interpretación "correcta" en la segunda parte no tiene nada que ver con la interpretación de la variable en la primera parte). Decimos "de mal gusto" porque no hay nada de incorrecto en ella, pero los matemáticos prefieren que (en un mismo contexto) objetos que no son necesariamente el mismo estén representados por variables distintas. Fórmulas como [texx]x= 0\land \exists x\ x = S0[/texx] son técnicamente correctas y su uso no genera ningún problema, pero siempre es posible sustituirlas por fórmulas como [texx]x= 0\land \exists y\ y = S0[/texx], que significan lo mismo y son "más claras". De hecho, si uno no lo piensa mucho puede creer que la fórmula [texx]x= 0\land \exists x\ x = S0[/texx] no puede ser satisfecha en el modelo usual de la aritmética (parece que diga que [texx]x[/texx] tiene que ser cero y uno a la vez), y no es así. Es satisfecha por cualquier valoración para la que [texx]v(x)[/texx] sea el número cero.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #6 : 16/03/2013, 10:21:48 am »

Nos falta discutir un último aspecto sobre los lenguajes formales antes de poder usarlos para formalizar razonamientos. Se trata del concepto de sustitución. Es un concepto que los matemáticos usan cotidiana e instintivamente. Por ejemplo, cuando un matemático escribe

[texx]A = \{x\in \mathbb R\mid \alpha(x)\}[/texx]

y luego tiene que [texx]3\in A[/texx], de ahí deduce [texx]\alpha(3)[/texx]. Al escribir esto ha sustituido la variable [texx]x[/texx] por el término [texx]3[/texx] en la fórmula [texx]\alpha[/texx]. Parece una operación trivial que apenas requiere un comentario para ser definida, pero no es exactamente así, como vamos a ver ahora. En esencia es ciertamente trivial, pero hay una cuestión técnica que debemos tener presente a la hora de tratar con sustituciones.

Para empezar, a la hora de tratar teóricamente con la sustitución, es preferible usar una notación más explícita, en la que se vean todos los elementos involucrados. En lugar de escribir [texx]\alpha(x)[/texx] y [texx]\alpha(3)[/texx], escribiremos [texx]\alpha[/texx] (porque una fórmula puede tener varias variables libres, y cualquiera de ellas puede ser sustituida en cualquier momento por un término) y escribiremos [texx]S_x^3\alpha[/texx] para la sustitución (de modo que se indica claramente que estamos sustituyendo la variable [texx]x[/texx] por el término [texx]3[/texx] en la fórmula [texx]\alpha[/texx]). El objetivo de este mensaje es dar una definición precisa de [texx]S_x^t\theta[/texx], donde [texx]\theta[/texx] es un término o una fórmula, [texx]x[/texx] es una variable y [texx]t[/texx] es un término.

Como siempre en estos contextos, la idea subyacente al concepto que queremos definir se expresa de forma natural en términos semánticos, es decir, en términos de lo que pretendemos que signifique lo que queremos definir, supuesto que hayamos fijado un modelo para el lenguaje formal considerado, pero al final daremos una definición puramente sintáctica (formal) que no haga referencia a ningún modelo posible, pero de tal modo que cuando se fije un modelo se corresponda con lo que pretendíamos.

En términos semánticos, el propósito de la sustitución es el siguiente:

Si [texx]\color{blue} T[/texx] es un término, una sustitución [texx]\color{blue} S_x^tT[/texx] debe ser otro término con la propiedad de que el objeto que denote en un modelo dado sea el objeto que denota el término [texx]\color{blue} T[/texx] cuando la variable [texx]\color{blue} x[/texx] se interpreta como el objeto denotado por el término [texx]\color{blue} t[/texx]

Si [texx]\color{blue} \alpha[/texx] es una fórmula, una sustitución [texx]\color{blue} S_x^t\alpha[/texx] debe ser otra fórmula que sea satisfecha en un modelo si [texx]\color{blue} \alpha[/texx] es satisfecha interpretando la variable [texx]\color{blue} x[/texx] como el objeto denotado por [texx]\color{blue} t[/texx].


Veamos algún ejemplo concreto con el lenguaje de la aritmética (y su modelo natural):

Si [texx]T= Sx[/texx], se trata de un término que significa "el siguiente del número natural [texx]x[/texx]". El objeto que denota en el modelo natural depende de la valoración [texx]v[/texx] que consideremos, pues será el siguiente del número natural [texx]v(x)[/texx].

¿Qué queremos que sea [texx]S_x^{SS0}Sx[/texx]? Queremos que sea un término que signifique lo mismo que [texx]T[/texx], es decir, "el siguiente de [texx]x[/texx]", pero cuando la variable [texx]x[/texx] se interpreta concretamente como el objeto denotado por [texx]SS0[/texx], es decir, como el número natural dos. Así pues, [texx]S_x^{SS0}Sx[/texx] debe denotar al siguiente del número natural dos, es decir, el tres. Por lo tanto, lo natural es tomar [texx]S_x^{SS0}Sx\equiv SSS0[/texx], que es simplemente lo que resulta de quitar la variable [texx]x[/texx] y poner en su lugar el término [texx]SS0[/texx], es decir, lo que vulgarmente se entiende por "sustituir".

Veamos ahora un ejemplo con una fórmula: tomemos

[texx]\alpha\equiv \forall y(\exists z\ x=y\cdot z\land y\neq S0\rightarrow \exists w\ y=w\cdot SS0)[/texx]

Esta fórmula dice que todo divisor de [texx]x[/texx] distinto de [texx]1[/texx] es par. Más precisamente, esta fórmula es satisfecha en el modelo natural del lenguaje de la aritmética si y sólo si el objeto denotado por [texx]x[/texx], es decir, [texx]v(x)[/texx], tiene todos sus divisores no triviales pares o, equivalentemente, si y sólo si [texx]v(x)[/texx] es potencia de dos.

¿Qué queremos que sea [texx]S_x^{SSSx}\alpha[/texx]? Tiene que ser una fórmula que ya no sea satisfecha cuando [texx]v(x)[/texx] sea potencia de dos, sino cuando el objeto denotado por [texx]SSSx[/texx] sea potencia de dos, es decir, cuando [texx]v(x)+3[/texx] sea potencia de dos. La fórmula obvia que cumple esto es:

[texx]S_x^{SSSx}\alpha\equiv \forall y(\exists z\ SSSx=y\cdot z\land y\neq S0\rightarrow \exists w\ y=w\cdot SS0)[/texx].

Una vez más, se trata de la fórmula que se obtiene quitando [texx]x[/texx] y poniendo en su lugar [texx]SSSx[/texx], es decir, "sustituyendo", en el sentido usual de la palabra.

Esto podría llevarnos a pensar que una definición puramente sintática de [texx]S_x^t\theta[/texx] (sin hacer referencia a modelos) es definirlo como la expresión (término o fórmula, según lo sea [texx]\theta[/texx]) que resulta de cambiar cada [texx]x[/texx] que aparezca en [texx]\theta[/texx] por el término [texx]t[/texx]. Sin embargo, dar esa definición no sería una buena idea, al menos sin tener presentes un par de cuestiones técnicas.

1) En primer lugar tenemos las "fórmulas de mal gusto" en las que una misma variable puede aparecer a la vez libre y ligada. La fórmula siguiente es lógicamente equivalente a la que hemos puesto como ejemplo, en el sentido de que será satisfecha en cualquier modelo y con cualquier valoración si y sólo si lo es la que hemos dado:

[texx]\alpha^*\equiv \forall y(\exists z\ x=y\cdot z\land y\neq S0\rightarrow \exists x\ y=x\cdot SS0)[/texx]

Cuando interpretamos esta fórmula en un modelo con una valoración, la primera [texx]x[/texx] que aparece se interpretará como [texx]v(x)[/texx], mientras que la segunda [texx]x[/texx], al estar ligada por el cuantificador [texx]\exists x[/texx], se interpretará como convenga (si es posible) para que se cumpla la fómrula que sigue al cuantificador, y no será necesario asignarle precisamente el valor [texx]v(x)[/texx].

Según explicábamos en otro mensaje, los matemáticos evitan este tipo de fórmulas, y en lugar de expresar así la propiedad "tener sólo divisores pares", la expresan con la fórmula inicial, donde la variable [texx]x[/texx] no representa dos papeles distintos. Pero lo cierto es que estas fórmulas existen, y nuestra definición debe dar cuenta de ellas, y si seguimos al pie de la letra nuestra propuesta de definición de sustitución obtendríamos este "engendro" que ni siquiera es una fórmula:

[texx]S_x^{SSSx}\alpha^*\equiv \forall y(\exists z\ SSSx=y\cdot z\land y\neq S0\rightarrow \exists SSSx\ y=SSSx\cdot SS0)[/texx]

Observemos que esto no es una fórmula porque las reglas sintácticas no permiten escribir [texx]\exists SSSx[/texx], sino que detrás de un cuantificador sólo puede ir una variable. Pero aunque corrigiéramos nuestra definición para no tocar las variables que siguen a los cuantificadores y calculáramos esto:

[texx]S_x^{SSSx}\alpha^*\equiv \forall y(\exists z\ SSSx=y\cdot z\land y\neq S0\rightarrow \exists x\ y=SSSx\cdot SS0)[/texx]

seguiríamos sin acertar, porque esta fórmula no significa que el objeto denotado por [texx]x[/texx] más tres es potencia de dos. Aquí dice que todo divisor de [texx]x[/texx] más tres distinto de [texx]1[/texx] es un número par mayor o igual que [texx]6[/texx], cosa que no cumple, por ejemplo, el [texx]1[/texx], a pesar de que [texx]1+3=4[/texx] es potencia de dos.

La sustitución correcta es:

[texx]S_x^{SSSx}\alpha^*\equiv \forall y(\exists z\ SSSx=y\cdot z\land y\neq S0\rightarrow \exists x\ y=x\cdot SS0)[/texx]

y la moraleja que extraemos de este ejemplo es que la sustitución [texx]S_x^t\alpha[/texx] debe definirse de modo que las apariciones ligadas de [texx]x[/texx] no se alteren en absoluto. Sustituir una variable por un término es sustituir únicamente las apariciones libres de la variable.

Sin embargo, esta precisión era la menor de las dos consideraciones que nos vemos obligados a hacer si queremos llegar a un concepto de "sustitución" que se corresponda realmente con nuestro objetivo en todos los casos.

2) Volvamos a nuestra fórmula [texx]\alpha[/texx] original, sin el doble papel "de mal gusto" que la [texx]x[/texx] tenía en la fórmula [texx]\alpha^*[/texx], pero supongamos ahora que queremos calcular [texx]S_x^{y+z}\alpha[/texx].

Puesto que [texx]\alpha[/texx] significa "[texx]x[/texx] es potencia de dos", queremos que [texx]S_x^{y+z}\alpha[/texx] signifique "[texx]y+z[/texx] es potencia de dos", pero si nos limitamos a sustituir cada [texx]x[/texx] (libre) que aparece en [texx]\alpha[/texx] por [texx]y+z[/texx] lo que nos sale es:

[texx]S_x^{y+z}\alpha\equiv \forall y(\exists z\ y+z=y\cdot z\land y\neq S0\rightarrow \exists w\ y=w\cdot SS0)[/texx]

y esto es un "enredo" que nada tiene que ver con que los divisores de [texx]y+z[/texx] sean pares. Ahí dice algo que es cierto, algo así como que, para todo número [texx]y[/texx], si existe un [texx]z[/texx] que cumple la ecuación [texx]y+z=yz[/texx] e [texx]y[/texx] no es uno, entonces [texx]y[/texx] es par (y es cierto porque la condición sólo se da cuando [texx]y=2,z=2[/texx]). ¿Qué ha fallado? Que las variables [texx]y, z[/texx] estaban libre en [texx]y+z[/texx], pero al meter este término en el lugar de [texx]x[/texx], han quedado en el radio de alcance de los cuantificadores [texx]\forall y\ \exists z[/texx], y se han mezclado con otras [texx]y, z[/texx] que ya estaban en la fórmula [texx]\alpha[/texx], y el resultado ha sido completamente imprevisible.

Los libros de lógica evitan estas sustituciones incontroladas de dos formas distintas:

A) Quizá la solución más aceptada sea prohibir que se realice la sustitución en este caso. Para ello definen que una variable [texx]x[/texx] es sustituible por un término [texx]t[/texx] en una fórmula [texx]\alpha[/texx] si ninguna variable que está (libre) en [texx]t[/texx] aparece ligada en [texx]\alpha[/texx], y sólo consideran definida la sustitución [texx]S_x^t\alpha[/texx] cuando se cumple esta condición.

En nuestro ejemplo, la variable [texx]x[/texx] no es sustituible por el término [texx]y+z[/texx] en la fórmula [texx]\alpha[/texx] porque las variables [texx]y, z[/texx] están en [texx]y+z[/texx] y están ligada en [texx]\alpha[/texx].

La solución A), con ser, como decimos, la más habitual y totalmente operativa, tiene dos defectos. Uno es que obliga a poner como hipótesis en todos los teoremas que involucren una sustitución que tal o cual variable debe ser sustituible por tal o cual término en tal o cual fórmula, lo cual supone mantener en un constante primer plano lo que es una mera anécdota que nunca se encuentra uno en la práctica.

El segundo inconveniente es que esto de que ciertas variables no puedan ser sustituidas por ciertos términos es algo totalmente ajeno a la práctica habitual del matemático que razona competentemente sin conocer los tecnicismos de la lógica. Si un matemático ve [texx]\alpha(x)[/texx] y tiene un [texx]t[/texx] a mano y le interesa decir que [texx]t[/texx] cumple [texx]\phi(x)[/texx], no concibe que no pueda escribir [texx]\phi(t)[/texx]. ¿Qué hace en la práctica un matemático? La realidad es que lo que hace es evitar que se le den casos como el que nos ocupa eligiendo prudentemente las variables, pero imaginemos que, por un descuido, un matemático ha escrito la fórmula [texx]\alpha[/texx] como nosostros lo hemos hecho y, en el curso de un razonamiento está trabajando con una [texx]y[/texx] y una [texx]z[/texx] y se ve en la necesidad de decir que [texx]y+z[/texx] cumple la propiedad [texx]\alpha[/texx]. ¿Qué haría?

El matemático vería [texx]\alpha[/texx]:

[texx]\forall y(\exists z\ x=y\cdot z\land y\neq S0\rightarrow \exists w\ y=w\cdot SS0)[/texx],

se daría cuenta de que no puede meter ahí [texx]y+z[/texx] sin hacer un estropicio y, en lugar de detenerse, corregiría la fórmula [texx]\alpha[/texx], cambiándola por

[texx]\forall u(\exists v\ x=u\cdot v\land u\neq S0\rightarrow \exists w\ u=w\cdot SS0)[/texx],

pues sabe que las [texx]y, z[/texx] que aparecen ligadas en la fórmula no tienen nada que ver con las [texx]y,z[/texx] concretas que está manejando y que le aparecen en su término [texx]y+z[/texx], y sabe que si en la fórmula cambia las [texx]y, z[/texx] ligadas por unas [texx]u,v[/texx] ligadas pasa a otra fórmula que significa lo mismo, que le vale igual, y ahora puede sustituir con tranquilidad y escribir que

[texx]S_x^{y+z}\alpha\equiv \forall u(\exists v\ y+z=u\cdot v\land u\neq S0\rightarrow \exists w\ u=w\cdot SS0)[/texx]

Así obtiene una fórmula que realmente significa "[texx]y+z[/texx] es potencia de dos".

En definitiva, la solución B) al problema consiste en definir la sustitución incluyendo instrucciones para sustituir variables ligadas cuando éstas entran en conflicto con variables del término que queremos sustituir. Con esto complicamos la definición de sustitución, pero eso afecta únicamente a los tres o cuatro resultados que hay que demostrar basándose en la definición de sustitución y, a partir de ahí, como las sustituciones se tratarán apelando a esos tres o cuatro resultados ya demostrados, en la práctica usual este caso patológico no deja rastro alguno. Ni hace falta añadir hipótesis a los teoremas recordando siempre lo que no es más que un caso extraño, ni hace falta contradecir la idea natural de que cualquier variable es sustituible en cualquier fórmula por cualquier término si uno tiene dos dedos de frente a la hora de hacerlo.

Naturalmente, adoptaremos la solución B), y tras esta discusión ya estamos en condiciones de dar una definición sintáctica no ingenua de sustitución de una variable por un término. En el próximo mensaje daremos dicha definición y demostraremos que cumple lo requerido.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #7 : 18/03/2013, 12:12:56 pm »

Ahora estamos en condiciones de definir el concepto de sustitución, teniendo en cuenta los requisitos apuntados por la discusión del hilo precedente.

La sustitución de una variable por un término en otro término no tiene ninguna complicación. Simplemente [texx]S_x^tT[/texx] es el término que resulta de cambiar cada [texx]x[/texx] por una [texx]T[/texx]. Una definición recurrente es esta:

[texx]S_x^t y\equiv \left\{\begin{array}{lll} t & \mbox{si}& y\equiv x\\ y & \mbox{si}& y\not\equiv x\end{array}\right.[/texx]

Spoiler: Observación (click para mostrar u ocultar)

Si [texx]c[/texx] es una constante, [texx]S_x^tc \equiv c[/texx].

[texx]S_x^t ft_1\cdots t_n\equiv fS_x^tt_1\cdots S_x^tt_n[/texx].

La última relación indica que para sustituir [texx]x[/texx] por [texx]t[/texx] en un término de la forma [texx]ft_1\cdots t_n[/texx] basta dejar el funtor como está y sustituir la variable en cada uno de los términos que le siguen.

Estas reglas permiten calcular en la práctica cualquier sustitución en un término en un número finito de pasos. Más aún, nos muestran (por si alguien no lo consideraba evidente) que al sustituir una variable por un término en un término, lo que sale sigue siendo un término, pues vemos que es siempre una variable, el término sustituido, una constante o una cadena de la forma funtor n-ádico seguido de n términos.

Spoiler: Observación (click para mostrar u ocultar)

Es en la definición de una variable por un término en una fórmula donde las consideraciones del hilo anterior nos llevan a dar una definición algo más sofisticada de lo que uno podría esperar:

[texx]S_x^tRt_1\cdots t_n\equiv RS_x^tt_1\cdots S_x^tt_n[/texx]

(es decir, la sustitución de [texx]x[/texx] por [texx]t[/texx] en una fórmula atómica se define dejando el relator como está y sustituyendo [texx]x[/texx] por [texx]t[/texx] en cada uno de los términos.

[texx]S_x^t\lnot\alpha\equiv \lnot S_x^t\alpha[/texx]

[texx]S_x^t(\alpha\rightarrow \beta)\equiv S_x^t\alpha\rightarrow S_x^t\beta[/texx]

(Estas dos condiciones implican a su vez que [texx]S_x^t(\alpha\lor \beta)\equiv S_x^t\alpha\lor S_x^t\beta[/texx], [texx]S_x^t(\alpha\land \beta)\equiv S_x^t\alpha\land S_x^t\beta[/texx], [texx]S_x^t(\alpha\leftrightarrow \beta)\equiv S_x^t\alpha\leftrightarrow S_x^t\beta[/texx]. Basta sustituir cada conector por su definición y aplicar las reglas que acabamos de dar.)

[texx]S_x^t\forall y\alpha\equiv \left\{\begin{array}{lll} \forall y\alpha & \mbox{ si } x \text{ no está libre en } \forall y\alpha\\ \forall yS_x^t\alpha & \mbox{si }  x \text{ está libre en }\forall y\alpha \text{ e } y \text{ no está libre en } t\\
\forall z S_x^tS_y^z\alpha&\mbox{si } x \text{ está libre en } \forall x\alpha,\ y \text{ está libre en } t.\end{array}\right.[/texx]

En el tercer caso, [texx]z[/texx] es la variable de menor índice que no está ni en [texx]\forall y\alpha[/texx] ni en [texx]t[/texx]. De la definición del cuantificador existencial se sigue fácilmente que la misma regla vale cambiando [texx]\forall[/texx] por [texx]\exists[/texx].

Spoiler: Nota conceptual importante (click para mostrar u ocultar)

Teorema: Consideremos un lenguaje formal,  un modelo [texx]M[/texx] y una valoración [texx]v[/texx]. Sean [texx]x, t, T y \alpha[/texx] una variable, dos términos y una fórmula del lenguaje. Entonces:

[texx]M(S_x^tT)[v]\equiv M(T)[v_x^{M(t)[v]}][/texx]

[texx]M\vDash (S_x^t\alpha)[v][/texx] se cumple si y sólo si  [texx]M\vDash \alpha[v_x^{M(t)[v]}][/texx]


La primera parte dice que el objeto denotado por [texx]S_x^tT[/texx] es el objeto denotado por [texx]T[/texx] cuando la variable [texx]x[/texx] se interpreta como el objeto denotado por [texx]t[/texx]. La segunda parte dice que [texx]S_x^t\alpha[/texx] es satisfecha si y sólo si [texx]\alpha[/texx] es satisfecha cuando la variable [texx]x[/texx] se interpreta como el objeto denotado por [texx]t[/texx]. Son estos hechos los que nos permiten decir que la sustitución está "bien definida" en el sentido de que es una expresión definida "como haga falta" para que al final signifique lo que tiene que significar.

Spoiler: Demostración (click para mostrar u ocultar)

En la prueba anterior se ve la utilidad de haber introducido los signos [texx]\lor, \land, \leftrightarrow, \exists[/texx] como signos definidos y no primitivos. Si fueran signos primitivos tendríamos que haber añadido a la prueba un caso más para cada uno de ellos. Ahora sabemos (con la prueba tal como la hemos presentado) que el resultado es cierto para toda fórmula, luego en particular para las que contienen los signos definidos.

Como explicábamos en el mensaje anterior, los matemáticos no usan la notación [texx]S_x^t\alpha[/texx], sino que en su lugar prefieren escribir [texx]\alpha(x)[/texx] sin que esto indique nada en especial (la variable [texx]x[/texx] puede estar o no libre en [texx]\alpha[/texx] y aparte puede haber otras variables libres), pero cuando luego escriben [texx]\alpha(t)[/texx] eso es una forma de escribir [texx]S_x^t\alpha[/texx].

Un ejemplo de sustitución aparece en la definición de existencia con unicidad. Definimos:

[texx]\exists! x\alpha(x)\equiv \exists x\alpha(x)\land \forall xy(\alpha(x)\land \alpha(y)\rightarrow x=y)[/texx],

donde [texx]y[/texx] es la variable de menor índice que no está en [texx]\exists x\alpha[/texx].

Escrito con la notación [texx]S[/texx] para la sustitución sería:

[texx]\exists! x\alpha \equiv \exists x\alpha \land \forall xy(\alpha \land S_x^y\alpha\rightarrow x=y)[/texx].

El teorema que justifica que esta definición no es caprichosa, sino que realmente formaliza la existencia con unicidad es el siguiente:

Teorema: Dado un lenguaje formal y fijado un modelo [texx]M[/texx] y una valoración [texx]v[/texx], se cumple [texx]M\vDash \exists!x\alpha[v][/texx] si y sólo si existe un único [texx]a[/texx] en el universo del modelo tal que [texx]M\vDash \alpha[v_x^a][/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Dejamos como ejercicio probar que el teorema anterior se cumple también con esta definición alternativa de la existencia con unicidad (que no involucra el concepto de sustitución)

[texx]\exists! x\alpha\equiv \exists y\forall x(\alpha\leftrightarrow x=y)[/texx],

donde [texx]y[/texx] es la menor variable que no está en [texx]\exists x\alpha[/texx].

Las dos definiciones posibles que hemos dado son ejemplos de fórmulas lógicamente equivalentes, es decir, de fórmulas tales que una es satisfecha en un modelo cualquiera si y sólo si lo es la otra.

Con esto ya tenemos suficientes resultados sobre lenguajes formales para empezar (a partir del hilo siguiente) a utilizarlos en nuestro proyecto de formalizar el razonamiento.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #8 : 18/03/2013, 20:47:20 pm »

Definición: Usaremos la notación [texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx] para indicar que [texx]\alpha_1,\ldots, \alpha_n, \alpha[/texx] son fórmulas de un lenguaje formal [texx]\mathcal L[/texx] tales que es posible demostrar que cuando [texx]M[/texx] es un modelo de [texx]\mathcal L[/texx] y se cumple [texx]M\vDash \alpha_1,\ldots, \alpha_n[/texx] necesariamente se cumple también  [texx]M\vDash \alpha[/texx].

En palabras: el hecho de que [texx]\alpha_1,\ldots, \alpha_n, \alpha[/texx] sean verdaderas en un modelo hace que necesariamente [texx]\alpha[/texx] también lo sea.

Ejemplo: Si [texx]\alpha[/texx] y [texx]\beta[/texx] son fórmulas arbitrarias de un lenguaje formal, se cumple

[texx]\alpha\rightarrow\beta,\ \alpha\vDash \beta[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Se dice que una expresión de la forma [texx]\alpha\rightarrow\beta,\ \alpha\vDash \beta[/texx] es una regla de inferencia semántica, es decir, un criterio que nos garantiza que si sabemos que unas fórmulas son verdaderas (en un modelo cualquiera) otra tiene que serlo necesariamente. También se dice que [texx]\beta[/texx] es una consecuencia lógica de [texx]\alpha[/texx] y [texx]\alpha\rightarrow\beta[/texx].

Es costumbre dar nombre a las reglas de inferencia. La del ejemplo anterior se llama modus ponendo ponens (en latín, la regla que afirmando ([texx]\alpha[/texx]) afirma ([texx]\beta[/texx])), aunque se suele abreviar en modus ponens.

Otro ejemplo es el modus tollendo ponens (la regla que negando ([texx]\alpha[/texx]) afirma [texx](\beta)[/texx]):

[texx]\alpha\lor\beta,\lnot\alpha\vDash\beta[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

El modus tollendo tollens (la regla que niega negando) es

[texx]\alpha\rightarrow\beta,\ \lnot\beta\vDash \lnot\alpha[/texx].

Dejamos la comprobación al lector.

Definición: Una clase particular de reglas de inferencia semánticas son las de la forma [texx]\vDash \alpha[/texx]. Esto significa que podemos razonar que la fórmula [texx]\alpha[/texx] es verdadera en cualquier modelo. Entonces se dice también que [texx]\alpha[/texx] es una fórmula lógicamente válida.

Por ejemplo, es fácil comprobar que [texx]\vDash \alpha\lor\lnot \alpha[/texx]. Esta regla recibe el nombre de tercio excluido o, en latín, tertium non datur. Demostrarla equivale a comprobar que en su tabla de verdad sólo puede tomar el valor V, cosa que se comprueba trivialmente.

Veamos ahora alguna regla de inferencia que no puede demostrarse mediante tablas de verdad. Por ejemplo la de transitividad de la igualdad:

[texx]t_1=t_2,\ t_2=t_3\vDash t_1=t_3[/texx],
donde [texx]t_1,t_2,t_3[/texx] son términos cualesquiera.

Spoiler: Demostración (click para mostrar u ocultar)

Tampoco podemos usar tablas de verdad cuando hay cuantificadores involucrados. Por ejemplo en la regla de eliminación del generalizador:

[texx]\forall x\alpha\vDash S_x^t\alpha[/texx],

donde [texx]x, t, \alpha[/texx] son una variable, un término y una fórmula arbitrarios de un lenguaje formal dado.

Spoiler: Demostración (click para mostrar u ocultar)

Veamos un ejemplo más sofisticado que involucra al igualador y a un cuantificador. Si la variable [texx]x[/texx] no está libre en el término [texx]t[/texx], entonces:

[texx]\vDash (\forall x(x=t\rightarrow \alpha)\leftrightarrow S_x^t\alpha)[/texx].

Observemos que los dos miembros de la fórmula afirman (cada cual a su manera) que [texx]t[/texx] cumple lo que dice [texx]\alpha[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Hay una regla de inferencia que involucra el cuantificador universal que requiere especial atención. Es la de introducción del generalizador:

[texx]\alpha\vDash \forall x\alpha[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

Su peculiaridad es que se cumple en virtud del convenio que hemos adoptado de considerar que una fórmula es verdadera cuando es satisfecha por cualquier valoración, lo cual equivale a que se cumple si y sólo si se cumple para toda posible interpretación de sus variables libres, y en particular si y sólo si se cumple "para todo x". Ahora bien, ya hemos comentado que los matemáticos no siempre entienden que lo que dice una fórmula hay que entenderlo como que vale para cualquier interpretación de sus variables, sino que distinguen (según el contexto) variables que representan objetos generales y variables que representan objetos particulares. Al adoptar el convenio sobre interpretación de las variables libres nos hemos apartado ligeramente de los hábitos matemáticos y la regla de introducción del generalizador pone de manifiesto esa divergencia. Más adelante veremos cómo podemos "congraciarnos" de nuevo con la práctica usual de los matemáticos sin desdecirnos de lo dicho.

Las reglas de inferencia nos permiten desglosar los razonamientos complejos en razonamientos más simples y reducirlos a "piezas" ya chequeadas y que no es necesario volver a chequear. Por ejemplo, consideremos de nuevo el silogismo que pusimos de ejemplo al inicio del hilo (el de las palabras properispómenas y barítonas). Su formalización es:

[texx]\forall x(Px\rightarrow Bx),\ PD\vDash BD[/texx]

Ya comentamos que estas fórmulas pueden interpretarse en un modelo cuyo universo sean todas las palabras griegas, en el que los relatores [texx]P[/texx] y [texx]B[/texx] se interpretan como dos propiedades de las palabras griegas que los gramáticos griegos sabrán qué demonios significan, y donde la constante [texx]D[/texx] se interpreta como una cierta palabra griega. Pero el hecho de que el silogismo sea lógicamente válido significa que todo eso es irrelevante, que se cumple lo que acabamos de escribir ahora, es decir, que si las dos premisas son verdaderas en un modelo cualquiera (no importa si su universo son palabras griegas o animales microscópicos) entonces la conclusión también tiene que serlo. Podríamos razonar esto con la misma clase de razonamientos que hemos venido usando en este mensaje, pero, en su lugar, podemos encadenar reglas de inferencia ya demostradas, así:

[texx]\begin{array}{lll}
1)&\forall x(Px\rightarrow Bx)&\mbox{Premisa}\\
2)&PD&\mbox{Premisa}\\
3)& PD\rightarrow BD&\mbox{Eliminación del generalizador 1}\\
4)&BD&\mbox{Modus Ponens 2,3}
\end{array}[/texx]

¿Cómo hay que entender esto? Supongamos que las dos premisas son verdaderas en un modelo [texx]M[/texx]. Entonces podemos asegurar que la fórmula 3) también será verdadera en [texx]M[/texx], porque resulta de aplicar la regla de inferencia de eliminación del generalizador, que ya hemos demostrado (notemos que la fórmula 3 resulta de calcular [texx]S_x^{D}[/texx] sobre la fórmula tras [texx]\forall x[/texx] en 1). A su vez 4) tiene que ser verdadera en [texx]M[/texx] porque se obtiene de 2 y 3 por la regla Modus Ponens, que también está demostrada.

Así hemos reducido un razonamiento que podríamos haber improvisado directamente a la aplicación de unas reglas de inferencia, que no son sino razonamientos ya comprobados y que no hace falta comprobar cada vez. Más aún, para construir la sucesión de fórmulas precedente no ha hecho falta considerar para nada ningún modelo. Sólo ha sido un problema de encajar las reglas oportunas adecuadamente, como un puzzle.

Ahora estamos en condiciones de precisar nuestro objetivo inmediato: ¿es posible seleccionar un número finito de reglas de inferencia semánticas (lo cual supone demostrarlas) de modo que siempre que queramos probar una afirmación del tipo [texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx] (es decir, que el hecho de que unas premisas sean verdaderas en un modelo obliga a que también lo sea la conclusión) podamos hacerlo aplicando oportunamente a las premisas las reglas de inferencia seleccionadas, de modo que no sea necesario mencionar modelos para nada?

La respuesta es afirmativa (pero no es nada trivial que así sea, y esto es una de las joyas que nos regala la lógica), y eso es formalizar el razonamiento, es decir, reducir cualquier razonamiento (que, en su versión no formalizada, significa justificar racionalmente que la verdad de unas premisas en un modelo fuerza a la verdad de la conclusión) a una concatenación de un número finito (fijo) de reglas de inferencia semánticas previamente demostradas, de modo que el razonamiento se reduce a una sucesión de fórmulas enlazadas por unas reglas fijas (que han sido verificadas razonando con modelos, pero que ya no necesitan volver a ser verificadas y, por consiguiente, en la demostración formal no queda referencia alguna a modelos).

En el mensaje siguiente empezaremos a desarrollar este programa de formalización. De momento terminamos con una observación sobre el concepto de regla de inferencia semántica.

Observación: Si en lugar de trabajar metamatemáticamente estuviéramos trabajando en una teoría formal, habríamos dado una definición de regla de inferencia ligeramente distinta, a saber:

[texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx] significa que para todo modelo [texx]M[/texx] del lenguaje formal considerado, si [texx]M\vDash \alpha_1,\ldots, \alpha_n[/texx] entonces [texx]M\vDash \alpha[/texx].

¿Cuál es la diferencia? Que aquí decimos "si las premisas son verdaderas, la conclusión también lo es", mientras que en la definición al principio del hilo hemos dicho "se puede demostrar que si las premisas son verdaderas..."

No es lo mismo. ¿No podría suceder que tuviéramos unas premisas y una presunta conclusión pero, por una parte no se nos ocurriera (o, peor aún, no hubiera) ningún razonamiento que justificara que la conclusión tiene que ser verdadera cuando lo son las premisas y, al mismo tiempo, no se nos ocurriera cómo construir (o, peor aún, no hubiera forma de construir) un modelo [texx]M[/texx] en el que las premisas fueran verdaderas pero la conclusión falsa?

Si se diera ese caso, ¿tendría sentido decir que la regla de inferencia es válida o no lo es, aunque no sepamos cuál es el caso? Si no hubiera forma de razonar que la regla es válida ni de construir un modelo que sirva de contraejemplo, ¿tendría sentido decir que hay tal modelo pero no podemos encontrarlo? ¿o habría que decir que no hay tal modelo y la regla es válida pero no hay un razonamiento que lo justifique?

Volveremos sobre estas preguntas más adelante, pero de momento, para evitar esa situación embarazosa, recordemos que hemos definido [texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx] como que existe un razonamiento que justifica la regla.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #9 : 19/03/2013, 13:30:31 pm »

En este mensaje empezamos a materializar el proyecto esbozado al final del mensaje anterior. Se trata de seleccionar un número finito de reglas de inferencia semánticas para considerar todas las deducciones que pueden realizarse únicamente con ellas, donde una deducción es una sucesión de fórmulas en la que sólo admitimos las premisas que se quieran considerar y las consecuencias lógicas de esas premisas que se obtienen por aplicación de alguna de las reglas de inferencia seleccionadas. Las deducciones obtenidas de esta forma serán lógicamente válidas en el sentido de que tendremos la garantía de que todas las consecuencias a las que lleguemos de este modo serán verdaderas en todo modelo en el que las premisas sean verdaderas. Lo realmente interesante es que, según veremos, eligiendo adecuadamente las reglas de inferencia, todo razonamiento podrá obtenerse a partir de ellas, es decir, siempre que podamos razonar (por cualquier medio) que se cumple [texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx], podremos obtener [texx]\alpha[/texx] a partir de las premisas dadas aplicando oportunamente las reglas de inferencia seleccionadas a las premisas.

Concretamente, vamos a necesitar ocho reglas de inferencia, seis de las cuales serán de la forma [texx]\vDash \alpha[/texx], para fórmulas [texx]\alpha[/texx] con cierta estructura prefijada. En tal caso, en lugar de decir que [texx]\vDash \alpha[/texx] es una regla de inferencia (o, equivalentemente, que [texx]\alpha[/texx] es una fórmula lógicamente válida) diremos que [texx]\alpha[/texx] es un axioma lógico, es decir, una fórmula que puede escribirse en cualquier momento en una deducción independientemente de lo que hayamos escrito hasta el momento.

Introducimos primero los seis axiomas lógicos que vamos a considerar. Con más precisión debemos decir que hay infinitos axiomas lógicos, pero que son de seis tipos concretos, fácilmente reconocibles, que constituyen lo que se llama seis esquemas axiomáticos:

Definición: Dado un lenguaje formal [texx]\mathcal L[/texx], llamaremos axiomas lógicos en [texx]\mathcal L[/texx] a las fórmulas de [texx]\mathcal L[/texx] que sean de uno de los seis tipos siguientes (donde [texx]\alpha,\beta,\gamma[/texx] representan fórmulas arbitrarias, [texx]t[/texx] representa un término arbitrario y [texx]x[/texx] representa una variable arbitraria):

K1) [texx]\alpha\rightarrow (\beta\rightarrow\alpha)[/texx]

K2) [texx](\alpha\rightarrow (\beta\rightarrow\gamma))\rightarrow ((\alpha\rightarrow\beta)\rightarrow (\alpha\rightarrow\gamma))[/texx]

K3) [texx](\lnot\alpha\rightarrow\lnot\beta)\rightarrow (\beta\rightarrow\alpha)[/texx]

K4) [texx]\forall x\alpha\rightarrow S_x^t\alpha[/texx]

K5) [texx]\forall x(\alpha\rightarrow\beta)\rightarrow (\alpha\rightarrow \forall x\beta)[/texx]     si [texx]x[/texx] no está libre en [texx]\alpha[/texx].

K6) [texx]\forall x(x=t\rightarrow \alpha)\leftrightarrow S_x^t\alpha[/texx]     si [texx]x[/texx] no está libre en [texx]t[/texx].

Las condiciones en K5) y K6) significan que si una fórmula tiene la forma indicada pero no cumple esas condiciones adicionales no se considera (por definición) un axioma lógico.

Estos axiomas se eligen con ciertos grados de libertad, pero no de forma arbitraria. Para que lo que hacemos tenga sentido es necesario, por una parte, que todos ellos sean fórmulas lógicamente válidas, es decir, que sean verdaderas en cualquier modelo (para que [texx]\vDash \alpha[/texx] sea realmente una regla de inferencia semántica) y por otra parte se eligen para que (junto con las dos reglas de inferencia que nos falta por introducir) sean suficientes para formalizar cualquier razonamiento.

Empecemos comprobando que en efecto se cumple una parte de estos requisitos:

Teorema: Todos los axiomas lógicos son fórmulas lógicamente válidas.

Spoiler: Demostración (click para mostrar u ocultar)

Ahora introducimos el concepto de deducción lógica junto con las dos reglas de inferencia que nos falta seleccionar:

Definición: Una deducción lógica en un lenguaje formal a partir de unas premisas [texx]\alpha_1,\ldots, \alpha_n[/texx] es una sucesión finita de fórmulas del lenguaje tal que cada fórmula de la sucesión es una premisa, un axioma lógico o bien es consecuencia inmediata de fórmulas anteriores de la sucesión, donde consecuencia inmediata significa que puede obtenerse por la aplicación de una de las dos reglas de inferencia primitivas siguientes:

Modus Ponens: De [texx]\alpha[/texx] y [texx]\alpha\rightarrow\beta[/texx] es consecuencia inmediata [texx]\beta[/texx].

Introducción del generalizador De [texx]\alpha[/texx] es consecuencia inmediata [texx]\forall x\alpha[/texx].

Escribiremos [texx]\alpha_1,\ldots, \alpha_n\vdash \alpha[/texx] para indicar que existe una deducción con premisas [texx]\alpha_1,\ldots, \alpha_n[/texx] cuya última fórmula es [texx]\alpha[/texx].

De este modo, tenemos dos conceptos distintos que hemos expresado mediante las notaciones

[texx]\alpha_1,\ldots, \alpha_n\vDash \alpha,\qquad \alpha_1,\ldots, \alpha_n\vdash \alpha[/texx]

El primero significa que [texx]\alpha[/texx] tiene que ser verdadera en todos los modelos en los que las premisas sean verdaderas, mientras que el segundo significa que [texx]\alpha[/texx] puede obtenerse en un número finito de pasos a partir de las premisas y de axiomas lógicos aplicando oportunamente las dos reglas de inferencia a las que hemos llamado primitivas. El primer concepto tiene un sentido muy claro, mientras que el segundo no es en principio más que un cúmulo de arbitrariedades ¿por qué esos axiomas lógicos y no otros? ¿por qué esas reglas de inferencia y no otras? Lo que da sentido al segundo concepto de deducción es que es equivalente al primero, aunque la prueba dista mucho de ser inmediata.

Queda, pues, claro que los axiomas y las reglas de inferencia no se eligen arbitrariamente, pero no es menos cierto que tenemos un margen para elegir los axiomas y las reglas. Hay otras elecciones posibles distintas de las que hemos hecho que dan lugar a un concepto de deducción formal igualmente equivalente al de consecuencia lógica en el sentido semántico. Para recoger estas distintas posibilidades igualmente válidas conviene introducir un concepto general de sistema deductivo formal:

Definición: Dado un lenguaje formal [texx]\mathcal L[/texx], un sistema deductivo formal [texx]F[/texx] sobre [texx]\mathcal L[/texx] está determinado por una colección de fórmulas de [texx]\mathcal L[/texx] a las que se llama axiomas de [texx]F[/texx] y un conjunto finito de reglas primitivas de inferencia, que son criterios que especifican cuándo una fórmula se considera consecuencia inmediata en [texx]F[/texx] de otra u otras fórmulas de [texx]\mathcal L[/texx].

Una deducción en [texx]F[/texx] a partir de unas premisas [texx]\alpha_1,\ldots, \alpha_n[/texx] es cualquier sucesión finita de fórmulas de [texx]\mathcal L[/texx] de modo que cada una de ellas sea una premisa, un axioma de [texx]F[/texx] o sea consecuencia inmediata en [texx]F[/texx] de fórmulas anteriores de la sucesión (es decir, que resulte de aplicar una de las reglas de inferencia de [texx]F[/texx]).

Escribiremos [texx]\alpha_1,\ldots, \alpha_n\vdash_F\alpha[/texx] para indicar que [texx]\alpha[/texx] es la última línea una deducción en [texx]F[/texx] con premisas [texx]\alpha_1,\ldots, \alpha_n[/texx].

En estos términos, hemos asociado un sistema deductivo formal a cada lenguaje formal [texx]\mathcal L[/texx] al que llamaremos [texx]K_{\mathcal L}[/texx], aunque escribiremos [texx]\vdash[/texx] en lugar de [texx]\vdash_{K_{\mathcal L}}[/texx], porque es el único que vamos a usar.

En principio, cualquiera puede tomar las fórmulas más pintorescas y diseñar reglas de inferencia estrafalarias y decir que ha definido un sistema deductivo formal, pero que sus elecciones arbitrarias satisfagan la definición de sistema deductivo formal no ponen al engendro en pie de igualdad con nuestro [texx]K_{\mathcal L}[/texx], pues éste ha sido diseñado teniendo en cuenta unos requisitos muy específicos:

Definición: Un sistema deductivo formal es correcto si sus axiomas son lógicamente válidos y sus reglas de inferencia son reglas de inferencia semánticas.

Sabemos que [texx]K_{\mathcal L}[/texx] es correcto, pues hemos demostrado que sus axiomas son lógicamente válidos y en el mensaje anterior vimos que sus dos reglas de inferencia primitivas son reglas de inferencia semánticas. Esto tiene una consecuencia importante:

Teorema: Si [texx]F[/texx] es un sistema deductivo formal correcto y [texx]\alpha_1,\ldots, \alpha_n\vdash_F\alpha[/texx], entonces [texx]\alpha_1,\ldots, \alpha_n\vDash \alpha[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Diseñar sistemas deductivos formales correctos es muy fácil. Sólo hay que tener cuidado de elegir axiomas y reglas de inferencia correctas, y hay muchos donde elegir y es fácil verificar que en efecto lo son. Lo que ya requiere cierto arte es elegir esos axiomas y esas reglas de inferencia para que el sistema sea semánticamente completo, en el sentido siguiente:

Definición: Un sistema deductivo formal [texx]F[/texx] sobre un lenguaje formal [texx]\mathcal L[/texx] es semánticamente completo si para todas las fórmulas [texx]\alpha_1,\ldots, \alpha_n, \alpha[/texx] de [texx]\mathcal L[/texx] se cumple que

[texx]\alpha_1,\ldots, \alpha_n\vdash_F\alpha[/texx]      si y sólo si      [texx]\alpha_1,\ldots, \alpha_n\vDash\alpha[/texx]

Veremos que [texx]K_{\mathcal L}[/texx] es semánticamente completo y, desde el momento en que existen sistemas deductivos formales semánticamente completos, sería absurdo trabajar con uno que no lo fuera. Se pueden tomar otros axiomas y otras reglas de inferencia, pero dichas alternativas estarán bien elegidas si al final dan lugar a un sistema completo. Notemos que si [texx]F[/texx] y [texx]G[/texx] son dos sistemas deductivos semánticamente completos sobre un mismo lenguaje formal, por muy diferentes que sean sus axiomas y sus reglas de inferencia, al final se tiene que

[texx]\alpha_1,\ldots, \alpha_n\vdash_F\alpha[/texx]      si y sólo si     [texx]\alpha_1,\ldots, \alpha_n\vdash_G\alpha[/texx]

para fórmulas cualesquiera de su lenguaje, ya que ambas afirmaciones equivalen a [texx]\alpha_1,\ldots, \alpha_n\vDash\alpha[/texx], y esta afirmación es independiente de cualquier convenio arbitrario. Ser una consecuencia lógica de unas premisas significa simplemente que si las premisas son verdaderas en un modelo la consecuencia también tiene que serlo, y esto es así o no es así, pero no depende de si hemos elegido definir "razonar" de esta o de aquella manera. Podemos definir sistemas deductivos formales con unos criterios u otros, pero no se define "razonar", lo que está bien razonado está bien razonado y lo que no está bien razonado no lo está. O bien un sistema deductivo formal formaliza sólo razonamientos correctos (es decir, es correcto) o no lo es, y o bien puede formalizar todos los razonamientos correctos (es decir, es completo) o no lo es.

Spoiler: Nota filosófica (click para mostrar u ocultar)

El interés de formalizar el razonamiento es evidente (dejando de lado las necesidades técnicas de fundamentar una teoría de conjuntos). En principio, afirmar que [texx]\alpha_1,\ldots, \alpha_n\vDash\alpha[/texx] tiene un significado muy concreto, pero es algo muy amplio. Razonar es razonar. No se puede acotar a priori qué argumentos son correctos y cuales son falaces. Si uno argumenta que [texx]\alpha[/texx] tiene que ser verdadera si lo son las premisas, su razonamiento puede estar bien o puede estar mal, y distinguir los razonamientos correctos de los falaces es precisamente la característica que se llama "racionalidad". Si uno ve un razonamiento de otro y considera que está mal, tendrá que advertirle su error y, o bien el otro reconoce el error, o a su vez considerará que es erróneo el razonamiento que afirma que hay un error. Y no hay unas reglas a priori por las que se pueda decir quién tiene razón. Si un tercero hace de árbitro, podrán convencerle los argumentos de uno o los del otro o los de nadie, pero lo único objetivo es el hecho empírico de que los seres racionales suelen llegar a consensos en las discusiones racionales (las disensiones se producen cuando hay premisas dudosas o implícitas, no por razonamientos dudosos a partir de las premisas).

En cambio, si todos los seres racionales llegan a aceptar que los razonamientos que justifican que [texx]K_{\mathcal L}[/texx] es semánticamente completo son correctos, a partir de ese momento desaparece cualquier posibilidad de discrepancia sobre lo que es un razonamiento correcto (en el contexto de la lógica de primer orden, es decir, sobre cualquier problema que pueda expresarse como si una determinada afirmación de un lenguaje de primer orden es verdadera o falsa en un modelo). Sencillamente, si un razonamiento puede reducirse a una deducción en [texx]K_{\mathcal L}[/texx], entonces es correcto, y si no se puede, no es correcto. De este modo, la razón se concreta a sí misma. (Al menos en el contexto de los razonamientos matemáticos) no es necesario confiar en que dos seres racionales que discutan sobre si un razonamiento es válido o no lo es lleguen a un consenso sin saber a qué atenerse más que a su capacidad de raciocinio, sino que si los dos llegan a consensuar que el razonamiento que prueba que [texx]K_{\mathcal L}[/texx] es semánticamente completo, a partir de ahí tienen garantizado que pueden consensuar cualquier otra discrepancia: si estamos de acuerdo en esto, estamos de acuerdo en todo (en el sentido de que podemos dilucidar sistemáticamente cualquier futura discrepancia estableciendo que sólo tendrá razón quien pueda formalizar su razonamiento en [texx]K_{\mathcal L}[/texx]). Por supuesto, uno puede equivocarse al formalizar un argumento igual que puede equivocarse al razonar "en el aire", pero la diferencia es que la corrección de una demostración en [texx]K_{\mathcal L}[/texx] es algo que puede ser comprobado mecánicamente, incluso por un ordenador que no entienda nada, pero sepa distinguir qué es un axioma y qué es una regla de inferencia bien aplicada.

Hay que advertir que esto tiene un poco de utópico, porque trabajar en [texx]K_{\mathcal L}[/texx] "a bajo nivel" sería muy tedioso y nadie lo hace en la práctica, sino que las demostraciones matemáticas se dejan normalmente a un nivel "semiformalizado", en el sentido de un nivel que no tiene el detalle suficiente como para que uno pueda decir que aquí se aplica MP y allá se aplica IG, pero sí lo suficientemente detallado como para que pasar de ahí a una prueba completamente detallada sea una mera rutina sin interés y que cualquiera podría hacer sin dificultad si tuviera un par de eras geológicas libres, pero en la práctica surgen inconvenientes técnicos, como que unos teoremas se basan en otros, y es fácil que en un enunciado falte una pequeña hipótesis que se ha asumido tácitamente en la prueba pero que haga inválidas referencias posteriores en las que no se tiene tal hipótesis, etc.

Pese a todo, resulta indiscutible que poder "enlatar" toda la capacidad de razonamiento matemático en seis esquemas de axioma y dos reglas de inferencia tiene un gran valor tanto teórico (para estudiar el alcance y las limitaciones del razonamiento matemático) como práctico (para concretar lo que es un razonamiento válido y resolver discrepancias entre seres con uso de razón).

Para terminar, una reflexión: La idea de que uno puede definir un sistema deductivo formal como [texx]K_{\mathcal L}[/texx] con el propósito de "definir" el razonamiento lógico y limitarse a presentar unos axiomas y reglas de inferencia considerando que no está obligado a justificar nada es esencialmente perversa. Los axiomas y las reglas deben ser demostrados (cosa que nosotros ya hemos hecho) y aún demostrándolos nos quedamos cortos, pues todavía falta justificar que no nos falta ningún axioma o regla por añadir, sino que los que hemos dado son suficientes para extraer todas las consecuencias lógicas posibles de unas premisas dada (cosa que aún tenemos pendiente, y que es lo que se conoce como teorema de completitud semántica).
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #10 : 21/03/2013, 19:22:21 pm »

En este mensaje presentamos algunas reflexiones sobre el concepto de deducción lógica, para lo cual pondremos un ejemplo que nos sirva de referencia. Vamos a demostrar que, para cualquier fórmula [texx]\alpha[/texx] se cumple
[texx]\vdash \alpha\rightarrow \alpha[/texx].

Una deducción posible es la siguiente:

[texx]\begin{array}{lll}
(1)&(\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha))\rightarrow
((\alpha\rightarrow(\alpha\rightarrow\alpha))\rightarrow(\alpha\rightarrow\alpha))
&\mbox{(K2)}\\
(2)&\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha)&\mbox{(Axioma K1)}\\
(3)&(\alpha\rightarrow(\alpha\rightarrow\alpha))
\rightarrow(\alpha\rightarrow\alpha)&\mbox{(MP 1,2)}\\
(4)&\alpha\rightarrow(\alpha\rightarrow\alpha)&\mbox{(Axioma K1)}\\
(5)&\alpha\rightarrow\alpha&\mbox{(MP 3,4)}
\end{array}[/texx]

Lo primero que observa cualquiera a la vista de esto es que la prueba es horripilante. A nadie se le habría ocurrido recurrir a un "argumento" así para probar que  [texx]\alpha\rightarrow \alpha[/texx].

Si tratamos de precisar esta primera impresión tratando de expresarla de forma más objetiva, lo que podemos decir es que la conclusión es mucho más evidente que los axiomas que presuntamente la demuestran. Más concretamente, lo que a uno le convence de que [texx]\alpha\rightarrow \alpha[/texx] "es verdad" (más técnicamente, que es una fórmula lógicamente válida, verdadera en todo modelo) es considerar esta modesta tabla de verdad:

[texx]\begin{array}{c|c}
\alpha&\alpha\rightarrow \alpha\\
\hline
V&V\\
F&V
\end{array}[/texx]

En cambio, para probar que el primer axioma de la prueba es lógicamente válido, y por lo tanto un axioma legítimo, hay que construir esta tabla de verdad:

[texx]\begin{array}{c|c|c|c|c|c|c}
\alpha&\alpha\rightarrow\alpha&(\alpha\rightarrow\alpha)\rightarrow\alpha&(\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha))&\alpha\rightarrow(\alpha\rightarrow\alpha)&((\alpha\rightarrow(\alpha\rightarrow\alpha))\rightarrow(\alpha\rightarrow\alpha))&\alpha\rightarrow((\alpha\rightarrow\alpha)\rightarrow\alpha))\rightarrow
((\alpha\rightarrow(\alpha\rightarrow\alpha))\rightarrow(\alpha\rightarrow\alpha))\\
\hline
V&V&V&V&V&V&V\\
F&V&F&V&V&V&V
\end{array}[/texx]

En este sentido podemos decir objetivamente que los axiomas de esta deducción son mucho más complicados que la conclusión. Y la idea que inevitablemente debería venirnos a la mente es si no estaremos haciendo el ridículo con [texx]K_{\mathcal L}[/texx]. La respuesta es negativa, pero conviene entender por qué.

Una axiomática "tradicional" (por ejemplo una axiomática para la geometría euclídea) pretende reducir lógicamente afirmaciones complejas a otras lo más simples posibles que se toman como axiomas. De este modo, una deducción a partir de unos axiomas resulta explicativa. Por ejemplo, si demostramos el teorema de Pitágoras a partir de los axiomas de la geometría euclídea estamos reduciendo una afirmación que no puede tenerse por evidente (nadie puede ver un triángulo rectángulo y decir "se ve claramente que el cuadrado de la hipotenusa es igual a ...") a otras que sí lo son (como "por dos puntos pasa una única recta", etc.) Cuando decimos que los axiomas de la geometría euclídea son intuitivamente evidentes queremos decir que cualquiera que los examine se da cuenta de que se corresponden con hechos intuitivamente verdaderos y que, por consiguiente, todas sus consecuencias serán intuitivamente verdaderas (aunque no sean intuitivamente evidentes).

De todos modos, el carácter intuitivo de los axiomas de la geometría euclídea es aquí secundario. Lo que importa es que (normalmente) los axiomas de una teoría axiomática se toman lo más simples posibles para que alguien que los vea pueda formarse una idea clara de lo que supone admitirlos como tales axiomas. Ya que los axiomas no se pueden demostrar, se procura al menos que se puedan juzgar fácilmente y sea igualmente fácil determinar bajo qué condiciones podemos esperar que se cumplan.

En cambio, los criterios para definir [texx]K_{\mathcal L}[/texx] se han fijado siguiendo unos criterios que no tienen nada que ver con éstos. No hay necesidad de tomar axiomas simples porque los axiomas SÍ se demuestran (ya hemos demostrado que son lógicamente válidos), es decir, nadie necesita sopesarlos para decidir si "se los cree" o "no se los cree". (A lo sumo uno tendrá que decidir si quiere razonar como todo el mundo —clásicamente— o si quiere adherirse a alguna secta de razonamiento, pero si opta por lo primero puede razonar que los axiomas elegidos son lógicamente válidos, y eso los hace automáticamente aceptables como axiomas). Por ello, en lugar de la simplicidad, lo que se ha buscado en ellos es la potencia: que contengan la máxima información en el mínimo esfuerzo.

Podríamos haber elegido otra colección de axiomas para [texx]K_{\mathcal L}[/texx] que fueran mucho más simples y "naturales", como [texx]\alpha\rightarrow \alpha\lor \beta[/texx], [texx]\alpha\land \beta\rightarrow \alpha[/texx], etc., pero el precio sería que en lugar de bastarnos con seis esquemas de axioma habríamos necesitado unas dos docenas de ellos, más o menos. ¿Merece la pena comprimir el número de axiomas necesarios (de esquemas de axioma, en realidad) a costa de hacerlos "poco naturales"? La respuesta es afirmativa. Como ya hemos comentado, la naturalidad es poco importante, pues al fin y al cabo podemos demostrar que son lógicamente válidos, y eso los legitima como axiomas, y como contrapartida hay varios resultados de la lógica matemática (del tipo "si se puede demostrar tal cosa también se puede demostrar tal otra cosa") que requieren razonar sobre los esquemas de axioma de [texx]K_{\mathcal L}[/texx] uno por uno, y entonces es muy de agradecer que esa parte de la prueba pueda despacharse distinguiendo sólo seis casos en lugar de veintiocho.

Con este criterio para elegir los axiomas no podemos ver las deducciones en [texx]K_{\mathcal L}[/texx] como explicativas, es decir, la prueba anterior no es una explicación de por qué es cierto (es lógicamente válido) que [texx]\alpha\rightarrow\alpha[/texx], sino que es una deducción a partir de axiomas lógicamente válidos (pero no obviamente lógicamente válidos) de una conclusión obviamente lógicamente válida. ¿Qué aporta entonces? De la deducción anterior podemos aprender algo interesante y no trivial, que no es que alfa implica alfa (eso es trivial y, por eso mismo, de interés dudoso) sino que alfa implica alfa es deducible en [texx]K_{\mathcal L}[/texx]. Prueba de que esto no es trivial es que a pocos se les habría ocurrido cómo hacer la deducción. Y este hecho no trivial es sólo el primer paso en la prueba de otro hecho menos trivial aún, y es que todas las fórmulas lógicamente válidas son deducibles en [texx]K_{\mathcal L}[/texx].

Hemos presentado un conjunto extraño (pero comprimido) de axiomas, y queremos demostrar que esos "bichos raros" que hemos tomado como axiomas de entre todas las fórmulas lógicamente válidas son suficientes para deducir de ellas todas las demás.

Pero esto no significa que todas las deducciones en [texx]K_{\mathcal L}[/texx] vayan a ser "monstruos" como el ejemplo anterior. Por el contrario, un uso "sensato" de [texx]K_{\mathcal L}[/texx] pasa por dos fases:

1) En una primera fase, lo que procede es "desembalar" la lógica que está ingeniosamente "embalada" en los axiomas de [texx]K_{\mathcal L}[/texx]. Es como si alguien hubiera logrado embalar una mesa desmontada en piezas en un espacio tan pequeño y tan bien aprovechado que no deja un hueco libre y parece mentira que toda una mesa de ese tamaño quepa en una caja tan diminuta. Lo primero que procede hacer es abrir la caja, sacar las piezas y ensamblarlas para tener la mesa lista para ser usada (aunque luego nadie sabría volver a meterla en la caja sin dejar cuarenta piezas fuera). En la práctica, esto significa demostrar las dos docenas (o más) de resultados que habríamos tomado como axiomas o reglas de inferencia de [texx]K_{\mathcal L}[/texx] si no nos hubiera obsesionado reducir los axiomas a la mínima expresión. Tales demostraciones serán tremendamente "monstruosas" o, si se prefiere, tremendamente ingeniosas, pues son parte de la demostración de un teorema nada trivial, el que dice "toda la lógica cabe en esta reducidísima caja".

2) En segundo lugar, una vez demostrados esos resultados básicos que bien podrían haberse tomado como axiomas y reglas de inferencia de un sistema deductivo formal, lo que procede es olvidarse de los axiomas de [texx]K_{\mathcal L}[/texx] y de todas las demostraciones monstruosas, y no usarlos nunca más salvo para propósitos teóricos (es como tirar el embalaje de la mesa), y a partir de ese momento realizar las deducciones prácticas en [texx]K_{\mathcal L}[/texx] apoyándonos, no en los axiomas, sino en los resultados básicos deducidos de ellos que habrían sido axiomas si hubiéramos apostado por la naturalidad en vez de por la compacidad.

Insisto en esto porque no es raro encontrar libros y profesores de lógica que presentan sistemas deductivos formales como [texx]K_{\mathcal L}[/texx] y no sólo no se molestan en "desembalar la lógica", como aquí haremos, sino que plantean ejercicios a sus lectores / alumnos en los que tratan de entrenarlos para hacer deducciones "monstruosas" del tipo necesario en la fase 1), como si eso fuera "lo normal" en [texx]K_{\mathcal L}[/texx], y el efecto es que el lector / alumno se forma la imagen distorsionada de que razonar en lógica es algo que poco tiene que ver con razonar en matemáticas, porque en matemáticas uno hace cosas "naturales": si quiero probar que [texx]x\in A\rightarrow x\in B[/texx], supongo que [texx]x\in A[/texx] y argumento que tiene que estar en [texx]B[/texx], mientras que demostrar esto mismo "en lógica" es buscar la combinación adecuada de axiomas esotéricos que, debida e ingeniosamente combinados, añadiendo un poco de MP, otro poco de IG y un algo de "vendo mi alma y salvación a Satán a cambio del don de la lógica formal", lleven a la implicación deseada.

Es como si un profesor de análisis, en lugar de reservar la definición de derivada para probar las reglas de derivación y otros resultados teóricos y enseñar a sus alumnos a usar las reglas de derivación para calcular derivadas en la práctica, ocultara a sus alumnos que existen las reglas de derivación (o las presentara aisladamente en ejercicios sin darles importancia) y exigiera a sus alumnos que calcularan cualquier derivada "normal" aplicando la definición de derivada cada vez.

Aquí trataremos de distinguir cuidadosamente la fase 1) de la fase 2), es decir, primero demostraremos (mediante pruebas "diabólicas") que en [texx]K_{\mathcal L}[/texx] pueden probarse los principios elementales de argumentación que los matemáticos utilizan de forma natural sin pretender deducirlos de nada más elemental, y después mostraremos que, contando con tales principios elementales trabajar en [texx]K_{\mathcal L}[/texx] es hacer exactamente lo mismo que hace un matemático que jamás haya oído hablar de [texx]K_{\mathcal L}[/texx].

Es en los razonamientos de la fase 2) en los que un profesor de lógica debería ejercitar a sus alumnos (reservando los axiomas de [texx]K_{\mathcal L}[/texx] para los razonamientos teóricos, como hacen los analistas con la definición de derivada), y son esos razonamientos los que los alumnos deben considerar como "típicos". Los razonamientos de la fase 1) son simplemente parte de la prueba de un teorema no trivial, y es que bastan los axiomas de  [texx]K_{\mathcal L}[/texx] para fundamentar los principios en los que se apoyan los razonamientos de la fase 2. Es bueno que los alumnos conozcan la demostración de ese teorema, pero eso es una cosa, y otra muy distinta es tomar las técnicas ingeniosas que requiere la demostración del teorema y usarlas "cotidianamente", cuando es tonto usar tales técnicas para otra cosa que no sea demostrar ese teorema.
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #11 : 21/03/2013, 21:57:41 pm »

Vamos a presentar y analizar brevemente un ejemplo de deducción "natural" en [texx]K_{\mathcal L}[/texx], no de las correspondientes a lo que hemos llamado "fase 1", sino de las correspondientes a la "fase 2". Como aún no hemos desarrollado la "fase 1" no estamos en condiciones de justificar que lo que vamos a escribir es realmente una deducción en [texx]K_{\mathcal L}[/texx] (mejor dicho, es evidente que NO es una deducción en [texx]K_{\mathcal L}[/texx], pero más adelante será también evidente que se puede desarrollar hasta una deducción en [texx]K_{\mathcal L}[/texx]).

Consideramos el lenguaje de la aritmética, que ya hemos tratado otras veces, introducimos la abreviatura siguiente (que leeremos "x divide a y"):

[texx]x\mid y\equiv \exists u\ y=xz[/texx].

y vamos a probar lo siguiente:

[texx]\forall xyz((xy)z=x(yz))\vdash \forall xyz(x\mid y\land y\mid z\rightarrow x\mid z)[/texx].

Expresamos la deducción en tres columnas. A la izquierda ponemos lo que diría un matemático, en el centro la deducción propiamente dicha y a la derecha las indicaciones que bastan para justificar que la deducción es correcta (supuesto que hubiéramos desarrollado ya la fase 1) sin necesidad de la columna de la izquierda:



Como decíamos, las dos primeras columnas constituyen lo que un matemático reconocería como una demostración válida (muy detallada) de la conclusión a partir de la premisa. Aunque parece que sus explicaciones son suficientes para justificar la validez del razonamiento, lo cierto es que hay una serie de reglas que el matemático respeta implícitamente, incluso subconscientemente, y que, aunque no estén indicadas de forma explícita, son indispensables para que la prueba sea correcta.

Por ejemplo, el matemático distingue entre las variables [texx]x, y, z[/texx], que en la línea (2) usa para referirse a tres números arbitrarios, y las variables [texx]u[/texx] y [texx]v[/texx], que introduce en (5) y (8) para referirse a dos números particulares. El matemático usa subconscientemente que no puede hacer lo mismo con una variable que represente a un objeto arbitrario que con otra que represente a un objeto particular. Por ejemplo, en la línea (12) escribe [texx]\exists u[/texx] y jamás habría pensado en escribir [texx]\forall u[/texx], porque esa [texx]u[/texx] representa al número particular [texx]uv[/texx], que es particular porque [texx]u[/texx] y [texx]v[/texx] lo eran. En cierto sentido, la posibilidad de escribir [texx]\forall u[/texx] o sólo [texx]\exists u[/texx] depende de "la historia" de las variables, y no sólo de la línea (11), a partir de la cual se introduce el cuantificador.

Sin embargo, aunque, según decimos, el hecho de que  [texx]u[/texx] y [texx]v[/texx] sean variables particulares prohíbe al matemático ligarlas con un generalizador, el hecho de que [texx]x, y, z[/texx] sean variables generales no significa que pueda ligarlas en cualquier momento por un generalizador. Por ejemplo, al matemático jamás se le habría pasado por la cabeza escrbir (3)  [texx]\forall xyz(x\mid y\land y\mid z)[/texx]. Él lo razonaría así: [texx]x, y, z[/texx] son tres números arbitrarios de los que supongo que [texx]x\mid y\land y\mid z[/texx], pero eso no significa que tres números cualesquiera deban cumplir esto, por lo que sería absurdo introducir ahí un generalizador. Sólo cuando llego a la línea (14) y tengo que si [texx]x\mid y\land y\mid z[/texx] también se cumple que [texx]x\mid z[/texx], sólo entonces puedo decir que esto vale para tres números arbitrarios, y eso justifica el paso a (15).

Más en general: cuando queremos probar que todo [texx]x[/texx] que cumple A también cumple B, puedo tomar un [texx]x[/texx] genérico que cumpla A, pero dicha generalidad no me permite afirmar que todo x cumple A. Sólo cuando pruebo la implicación [texx]A\rightarrow B[/texx] es cuando puedo decir que dicha implicación vale para todo [texx]x[/texx]. Puedo generalizar respecto de [texx]x[/texx] después, pero no antes de llegar a la implicación.

Otro hecho que el matemático tiene en cuenta instintivamente es que, aunque en la línea (7) tiene un [texx]\exists u[/texx], al eliminar el cuantificador está obligado a sustituir la variable [texx]u[/texx] por otra variable nueva [texx]v[/texx], porque ya está usando la variable [texx]u[/texx] para referirse al número que cumple (5) y no tiene por qué ser el mismo que cumpla (8). En cambio, cuando elimina los cuantificadores de (1) para escribir (10), no le importa que ya esté usando la variable [texx]x[/texx] ni tampoco tiene inconveniente en sustituir las variables [texx]y, z[/texx] por las variables [texx]u, v[/texx] que ya está usando para nombrar otros objetos. La diferencia la marca que los cuantificadores de (1) son universales, por lo que las variables ligadas por ellos pueden sustituirse por cualquier objeto, aunque sea uno del que ya estemos hablando.

En general, podemos decir que el matemático aplica reglas "locales", es decir, reglas que dependen del punto de la demostración en el que estemos: no es lo mismo generalizar antes de haber probado la implicación que después, no es lo mismo quitar un [texx]\exists u[/texx] si antes ya hemos hablado de una [texx]u[/texx] que si no, etc. Por el contrario, las reglas de inferencia de [texx]K_{\mathcal L}[/texx] son globales: dadas una o dos fórmulas, o de ellas se deduce algo o no se deduce, no importa qué otras líneas haya en la deducción. Otro ejemplo de "localidad" es que el matemático tiene claro que, en caso de prolongar la deducción, no podría usar ya que [texx]x\mid y[/texx], porque esto no es una premisa de la deducción, sino una hipótesis local que ha usado para probar la implicación (15), en caso de seguir usando la línea (3) estaría convirtiendo en premisa de su deducción lo que no era más que una premisa local, y no sería cierto que sus consecuencias fueran realmente consecuencias de la línea (1), que es la única premisa declarada.

Esto podría hacernos sospechar que [texx]K_{\mathcal L}[/texx] no es suficientemente potente como para formalizar razonamientos como el anterior, puesto que le falta la "sensibilidad al contexto" en la que constante y casi inconscientemente se apoya el matemático. Pese a las apariencias, veremos que no es así. Eso sí, para formalizar este tipo de razonamientos en  [texx]K_{\mathcal L}[/texx] tendremos que explicitar todos los detalles como los que hemos comentado y que un matemático tiene en cuenta casi sin decirlo explícitamente, pues para que algo sea una auténtica deducción en [texx]K_{\mathcal L}[/texx] tiene que cumplir una serie de requisitos muy concretos totalmente explícitos, y eso es incompatibles con asumir condiciones tácitas que el "sentido común" dicte en cada momento improvisadamente.

En los próximos mensajes nos dedicaremos a mostrar que (una vez hecho el "trabajo sucio") en [texx]K_{\mathcal L}[/texx] es posible razonar siempre al estilo de la deducción anterior y que nunca será necesario deprimirse con deducciones como la que consideramos en el mensaje anterior.

* cic1.jpg (102.59 KB - descargado 1947 veces.)
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #12 : 22/03/2013, 19:56:12 pm »

El teorema de deducción afirma que (pese a las apariencias) en [texx]K_{\mathcal L}[/texx] es válida una técnica de razonamiento que usan constantemente los matemáticos. La hemos usado en la deducción que hemos puesto como ejemplo en el mensaje anterior. Allí la única premisa era (1), y queríamos demostrar la implicación [texx]x\mid y\land y\mid z\rightarrow x\mid z[/texx] que constituye la línea (14). Para ello hemos supuesto la hipótesis (2), contraviniendo la definición de deducción, pues (2) no es una premisa, ni un axioma, ni se deduce de líneas anteriores, y hemos llegado hasta (13).

Lo que dice el teorema de deducción es que esto es correcto, que si suponiendo (2) (aunque no sea una premisa de la deducción) llegamos a (13), podemos afirmar la implicación (14). El enunciado general es el siguiente:

Teorema de deducción Sea [texx]\mathcal L[/texx] un lenguaje formal y consideremos fórmulas de [texx]\mathcal L[/texx] tales que [texx]\alpha_1,\ldots, \alpha_n,\alpha\vdash \beta[/texx]. Si es posible deducir [texx]\beta[/texx] sin aplicar la regla de introducción del generalizador a variables libres en [texx]\alpha[/texx], entonces [texx]\alpha_1,\ldots, \alpha_n\vdash \alpha\rightarrow \beta[/texx].

En pocas palabras, lo que dice el teorema de deducción es que para deducir [texx]\alpha\rightarrow\beta[/texx] a partir de unas premisas, podemos añadir [texx]\alpha[/texx] como premisa y deducir [texx]\beta[/texx]. Lo que obtendremos así no será una deducción de [texx]\alpha\rightarrow\beta[/texx] en [texx]K_{\mathcal L}[/texx], pero la demostración del teorema de deducción muestra cómo a partir de esta deducción es posible obtener una auténtica deducción de [texx]\alpha\rightarrow\beta[/texx] a partir de las premisas indicadas.

Notemos la restricción (que no puede ser pasada por alto) de que en la deducción de [texx]\beta[/texx] no puede generalizarse respecto de variables libres en [texx]\alpha[/texx]. Esta limitación puede parecer extraña a un matemático, pero, como explicábamos en el mensaje anterior, en realidad es una limitación que todos los matemáticos se autoimponen inconscientemente cuando se ven en una situación concreta de las descritas por el teorema anterior.

Por ejemplo, en la deducción que poníamos como ejemplo, desde el momento en que suponemos [texx]x\mid y\land y\mid z[/texx] queda prohibido generalizar respecto de [texx]x, y, z[/texx], porque al hacerlo estaríamos afirmando que todos los números cumplen [texx]x\mid y\land y\mid z[/texx] y esto es falso. Desde el momento en que introducimos esta hipótesis, debemos romper nuestro convenio semántico de que una variable libre representa a un objeto arbitrario, y a partir de aquí [texx]x, y, z[/texx] representan números arbitrarios de entre los que cumplan la hipótesis (y si generalizáramos como si fueran números totalmente arbitrarios estaríamos afirmando que todos los números cumplen la hipótesis, lo cual no tiene por qué ser cierto). Una vez hemos aplicado el teorema de deducción para escribir (14) el teorema nos asegura que esta línea es consecuencia de la premisa (1), y a partir de aquí podemos "olvidarnos" de que hemos usado el teorema de deducción para probarlo (pues ya sabemos que existe una deducción "normal" de (14) a partir de (1), y podemos generalizar para pasar a (15).

Spoiler: Demostración (click para mostrar u ocultar)

De la demostración del teorema de deducción se sigue que en la deducción que se construye de [texx]\alpha_1,\ldots, \alpha_n\vdash \alpha\rightarrow \beta[/texx] se generaliza exactamente respecto de las mismas variables que en la deducción dada de  [texx]\alpha_1,\ldots, \alpha_n,\alpha\vdash \beta[/texx].

En la práctica podemos usar el teorema de deducción en una versión ligeramente más general. Imaginemos que estamos construyendo una deducción a partir de unas premisas [texx]\alpha_1,\ldots, \alpha_n[/texx], digamos [texx]\gamma_1,\ldots, \gamma_m[/texx], y a continuación queremos deducir una fórmula de tipo [texx]\alpha\rightarrow \beta[/texx]. Entonces escribimos [texx]\alpha[/texx] y la usamos como una premisa más hasta obtener [texx]\beta[/texx] (sin generalizar respecto de variables libres en [texx]\alpha[/texx]). Al llegar a [texx]\beta[/texx], lo que hemos probado es que [texx]\gamma_1,\ldots, \gamma_m,\alpha\vdash \beta[/texx] con una deducción en la que no se generalizan variables libres en [texx]\alpha[/texx], luego el teorema de deducción nos da que [texx]\gamma_1,\ldots, \gamma_n\vdash \alpha\rightarrow \beta[/texx], es decir, que existe una deducción de [texx]\alpha\rightarrow \beta[/texx] con premisas en [texx]\gamma_1,\ldots, \gamma_m[/texx]. Pero por otra parte sabemos que [texx]\gamma_1,\ldots, \gamma_m[/texx] se deducen de [texx]\alpha_1,\ldots, \alpha_n[/texx], luego también [texx]\alpha_1,\ldots, \alpha_n\vdash \alpha\rightarrow \beta[/texx]. (Para tener una deducción que prueba esto deducimos cada [texx]\gamma_i[/texx] de las premisas y luego deducimos [texx]\alpha\rightarrow \beta[/texx] de las [texx]\gamma_i[/texx]).

En la práctica marcaremos todas las líneas desde que suponemos [texx]\alpha[/texx] hasta que llegamos a [texx]\beta[/texx] con una línea vertical (tal y como se ve en el ejemplo del hilo anterior). Esta línea advierte de que las fórmulas abarcadas por ella no son consecuencia de las premisas de la deducción principal, sino de las premisas más una hipótesis auxiliar (la fórmula [texx]\alpha[/texx]) que sólo hemos aceptado provisionalmente para aplicar el teorema de deducción. Si una vez hemos añadido [texx]\alpha\rightarrow \beta[/texx] a la deducción la prosiguiéramos haciendo uso de las líneas marcadas, la deducción sería inválida, pues estaríamos haciendo uso de una premisa [texx]\alpha[/texx] que no forma parte de las premisas de la deducción.

La observación de que para obtener la deducción cuya existencia afirma el teorema de deducción sólo se generaliza respecto de variables generalizadas en la prueba dada es esencial para que estemos seguros de que no estamos generalizando en un momento dado respecto de una variable "prohibida". El uso del teorema de deducción oculta el uso de algunos axiomas y reglas de inferencia (las que aparecen en la demostración al construir la deducción de [texx]\alpha\rightarrow \beta[/texx]), pero no oculta ningún uso de IG.

Ejemplo Hemos explicado que la restricción sobre el uso de IG en el teorema de deducción es "razonable", pero ahora vamos a demostrar que es necesaria. Para ello veamos un ejemplo de falsa deducción en la que se usa el teorema de deducción sin respetar la restricción sobre el uso de IG. Concretamente, en la línea (2) generalizamos respecto de una variable libre en la hipótesis:



La línea (7) es deducible en [texx]K_{\mathcal L}[/texx] (sin premisas), aunque posponemos la prueba hasta más adelante (cuando "desenlatemos" la lógica del igualador). Aceptando este hecho, podemos incorporarla en nuestra deducción.

Si el teorema de deducción fuera válido sin la restricción sobre el uso de IG, la deducción anterior sería correcta y podríamos concluir que [texx]\vdash \forall xy\ x=y[/texx], luego, por el teorema de corrección, [texx]\vDash \forall xy\ x=y[/texx], pero esta fórmula no es lógicamente válida. Al contrario, es falsa en todos los modelos del lenguaje formal considerado cuyo universo tenga más de un objeto. Esta contradicción prueba que la hipótesis sobre IG es necesaria en el teorema de deducción.

Observemos que el teorema de deducción tiene un recíproco trivial:

Recíproco del teorema de deducción: Si [texx]\alpha_1,\ldots, \alpha_n\vdash\alpha\rightarrow\beta[/texx] entonces [texx]\alpha_1,\ldots, \alpha_n,\alpha\vdash \beta[/texx].

En efecto, para deducir [texx]\beta[/texx] deducimos primero [texx]\alpha\rightarrow \beta[/texx] y luego aplicamos MP.

Spoiler: Aclaración (click para mostrar u ocultar)

* cic2.jpg (27.65 KB - descargado 1910 veces.)
* cic15.jpg (12.8 KB - descargado 1863 veces.)
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #13 : 23/03/2013, 13:06:30 pm »

Llamaremos reglas de inferencia derivadas a cualquier resultado de la forma

[texx]\alpha_1,\ldots, \alpha_n\vdash \alpha[/texx]

y las llamamos así porque una vez hemos comprobado que esto es cierto (es decir, hemos encontrado una deducción de [texx]\alpha[/texx] a partir de las premisas correspondientes) podemos usarlas en las deducciones como reglas de inferencia en pie de igualdad con las dos reglas primitivas MP e IG. En efecto, si en una deducción hemos escrito ya (entre otras) las líneas [texx]\alpha_1,\ldots, \alpha_n[/texx], podemos escribir [texx]\alpha[/texx] en cualquier momento que nos interese, aunque no se deduzca ni por MP ni por IG. Con esto nuestra deducción tendrá un "agujero", pero sabemos que ese agujero se puede "llenar" intercalando las líneas de la deducción de [texx]\alpha[/texx] a partir de [texx]\alpha_1,\ldots, \alpha_n[/texx] que ya conocemos.

Por ejemplo, en la deducción sobre divisibilidad de números naturales que vimos dos mensajes atrás, para pasar de la línea (2) a la (3) usamos la regla de inferencia derivada de eliminación del conjuntor, que en realidad son dos reglas de inferencia a las que no merece la pena dar nombres distintos:

[texx]\alpha\land \beta\vdash \alpha[/texx]    y    [texx]\alpha\land\beta\vdash\beta[/texx].

Para que la deducción indicada estuviera completa haría falta (entre otras cosas) insertar la deducción en [texx]K_{\mathcal L}[/texx] de [texx]x\mid y[/texx] a partir de [texx]x\mid y\land y\mid z[/texx], pero si demostramos que las reglas anteriores valen en general para todas las fórmulas [texx]\alpha[/texx] y [texx]\beta[/texx] podemos omitir las líneas necesarias para ello en nuestras deducciones con la garantía de que si quisiéramos una deducción completa, sin que falte una sola línea, sabríamos cómo añadir lo que hemos omitido.

Esto es lo que hacen los matemáticos cada vez que citan un teorema ya demostrado. Una demostración que en un momento dado diga "por el teorema del valor medio podemos afirmar que..." está incompleta, y sólo estaría completa si antes de decir "por el teorema del valor medio" insertáramos una demostración del teorema del valor medio, pero no ganaríamos nada con ello, al contrario, sólo volveríamos ilegibles todas las demostraciones.

El teorema de completitud semántica (que todavía no hemos demostrado) garantizará que para toda regla de inferencia semática [texx]\alpha_1,\ldots, \alpha_n\vDash\alpha[/texx], es decir, que siempre que el hecho de que [texx]\alpha_1,\ldots, \alpha_n[/texx] sean verdaderas en un modelo es necesario (no necesario según ciertos convenios arbitrarios prefijados, sino necesario a secas) que [texx]\alpha[/texx] sea verdadera, entonces [texx]\alpha_1,\ldots, \alpha_n\vdash \alpha[/texx], es decir, existe una deducción de [texx]\alpha[/texx] a partir de los axiomas lógicos que hemos seleccionado en principio arbitrariamente y de las dos reglas de inferencia que hemos elegido en principio arbitrariamente.

Como aún no estamos en condiciones de probar esto, no podemos justificar una regla de inferencia constatando simplemente que es semánticamente válida, pues eso no nos garantiza que sea deducible en [texx]K_{\mathcal L}[/texx] y a menudo sucederá que la validez semántica es inmediata, mientras que la validez sintáctica, es decir, la existencia de una deducción, requiera utilizar los escasos recursos que proporciona [texx]K_{\mathcal L}[/texx] de forma retorcida y antinatural. Ya hemos explicado cómo debe entenderse esto y no entraremos aquí de nuevo en ello.

Una regla de inferencia muy tonta pero, pese a ello, muy útil, es la regla de repetición (R):

[texx]\alpha\vdash \alpha[/texx]

Es útil porque a menudo conviene cambiar el nombre con el que nos estamos refiriendo a una misma fórmula. Así lo hemos hecho, por ejemplo en la prueba sobre divisibilidad al pasar de la línea (3) a la (4) que son la misma fórmula, pues (3) es por definición una abreviatura taquigráfica de (4).

Spoiler: Nota (click para mostrar u ocultar)

Una regla de inferencia que admite una deducción "natural" gracias a que contamos ya con el teorema de deducción es la siguiente:

Modus Barbara (MB)  [texx]\alpha\rightarrow \beta,\beta\rightarrow\gamma\vdash\alpha\rightarrow\gamma[/texx]

La deducción sería la siguiente (llamamos hipótesis a las premisas adicionales que añadimos para emplear el teorema de deducción):





Reglas relacionadas con el negador y el implicador

Una regla muy especial es la siguiente:

Regla de la contradicción (C)   [texx]\alpha,\lnot\alpha\vdash \beta[/texx]

En palabras: a partir de una contradicción (es decir si contamos con una fórmula y su negación como premisas) podemos deducir cualquier otra fórmula. La versión semántica de esta regla es peculiar, pues se reduce a que si en un modelo [texx]M[/texx] son verdaderas a la vez [texx]\alpha[/texx] y [texx]\lnot\alpha[/texx] entonces en [texx]M[/texx] es verdadera cualquier fórmula, y esto es trivialmente cierto porque es imposible que en un modelo sean verdaderas a la vez [texx]\alpha[/texx] y [texx]\lnot\alpha[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

La deducción de la regla en [texx]K_{\mathcal L}[/texx] sugiere un argumento semántico algo más sofisticado: si en un modelo [texx]M[/texx] se cumple [texx]M\vDash \lnot\alpha[/texx], entonces se cumple claramente [texx]\vDash \alpha\rightarrow\beta[/texx] (porque una implicación con hipótesis falsa es verdadera), luego si se cumpliera [texx]\alpha[/texx] también tendría que cumplirse [texx]\beta[/texx].

Regla de la doble negación (DN)   [texx]\lnot\lnot\alpha\vdash \alpha[/texx],      [texx]\alpha\vdash\lnot\lnot\alpha[/texx]

Notemos que aplicando el teorema de deducción a estas reglas (lo cual es válido porque en su prueba no se usa para nada IG) obtenemos que [texx]\vdash \lnot\lnot\alpha\rightarrow \alpha[/texx] y [texx]\vdash\alpha\rightarrow \lnot\lnot\alpha[/texx]. También llamaremos DN a estos dos hechos, es decir, al insertar fórmulas de cualquiera de estos dos tipos en una deducción.

Notemos que [texx]\lnot\lnot\alpha\vDash \alpha[/texx] es inmediato. Si un modelo cumple [texx]M\vDash \lnot\lnot\alpha[/texx] eso es exactamente lo mismo que cumplir [texx]M\vDash \alpha[/texx]. Sin embargo, el hecho de que la regla sea semánticamente trivial no nos exime de justificar que [texx]K_{\mathcal L}[/texx] es lo suficientemente potente para demostrarla, y la prueba es horripilante:

Spoiler: Demostración (click para mostrar u ocultar)

Reglas de la negación de la implicación (NI)  [texx]\alpha\rightarrow\beta\vdash \lnot\beta\rightarrow\lnot\alpha[/texx],   [texx]\lnot\beta\rightarrow\lnot\alpha\vdash\alpha\rightarrow \beta[/texx],   [texx]\alpha\rightarrow\lnot\beta\vdash\beta\rightarrow\lnot\alpha[/texx],   [texx]\lnot\alpha\rightarrow \beta\vdash\lnot\beta\rightarrow\alpha[/texx]

Para la prueba remito al lector a mi libro de lógica (página 47). La prueba de las reglas NI es "menos horripilante" que la de las reglas DN, pero no por ello dejan de ser "antinaturales" en el sentido de que no pueden ser entendidas como una justificación de por qué son semánticamente válidas. (Pero esto no ha de entenderse como ninguna clase de crítica a la teoría, la teoría es exactamente la que tiene que ser y las pruebas son antinaturales porque así tienen que ser, no hay nada de erróneo en el planteamiento).

Modus tollendo tollens (MT)     [texx]\alpha\rightarrow\beta,\lnot\beta\vdash \lnot\alpha[/texx],    [texx]\alpha\rightarrow\lnot\beta, \beta\vdash \lnot\alpha[/texx].

Para deducir estas reglas basta aplicar el recíproco del teorema de deducción a NI.



Reglas relacionadas con el disyuntor

Reglas de equivalecia entre disyunción e implicación (EDI)   [texx]\alpha\lor\beta\vdash \lnot\alpha\rightarrow\beta[/texx],   [texx]\lnot\alpha\rightarrow \beta\vdash \alpha\lor \beta[/texx].

Estas reglas son un caso particular de la regla de repetición, pues las dos fórmulas que relacionan son de hecho la misma, por la definición que hemos dado del disyuntor.

Notemos que nos proporcionan una técnica que es útil a menudo para demostrar una disyunción: suponemos que no se cumple una de las fórmulas y usamos eso para demostrar la otra. El teorema de deducción nos da entonces [texx]\lnot\alpha\rightarrow \beta[/texx] y esto equivale a [texx]\alpha\lor\beta[/texx].

Recíprocamente, una forma de "aprovechar" una premisa que sea una disyunción (no es la única posible) consiste en llegar a que no se cumple una de las fórmulas y concluir que se tiene que cumplir la otra. Esto lo expresa de forma más explícita la regla siguiente:

Modus tollendo ponens (MTP)  [texx]\alpha\lor \beta,\lnot\alpha\vdash \beta[/texx],   [texx]\alpha\lor\beta,\lnot\beta\vdash \alpha[/texx].

La primera se deduce inmediatamente de EDI: si suponemos [texx]\alpha\lor\beta[/texx] y [texx]\lnot\alpha[/texx], tenemos que [texx]\lnot\alpha\rightarrow \beta[/texx] y basta aplicar MP. Para la segunda:

[texx]
\begin{array}{lll}
(1)&\alpha\lor\beta&\mbox{Premisa}\\
(2)&\lnot\beta&Premisa\\
(3)&\lnot\alpha\rightarrow\beta&\mbox{EDI 1}\\
(4)&\lnot\lnot\alpha&\mbox{MT 2, 3}\\
(5)&\alpha&\mbox{DN 4.}
\end{array}
[/texx]

Una regla con demostración inmediata es:

Regla del tercio excluso o tertium non datur (TND)  [texx]\vdash \alpha\lor\lnot\alpha[/texx]

Basta tener en cuenta que esta fórmula es la misma que [texx]\lnot\alpha\rightarrow\lnot\alpha[/texx], que ya sabemos que es deducible en [texx]K_{\mathcal L}[/texx].

En cambio, la regla siguiente es algo más complicada de probar:

Regla de eliminación del disyuntor (ED)   [texx]\alpha\lor\alpha\vdash\alpha[/texx]

Una prueba directa a partir de los axiomas de [texx]K_{\mathcal L}[/texx] es especialmente monstruosa. En cambio, se simplifica muchísimo si se demuestran primero las reglas relacionadas con el conjuntor, de las que hablaremos luego. Remito a mi libro de lógica para la prueba (página 49).

Con esta regla podemos probar otra técnica útil para sacarle partido a una disyunción en una deducción: si contamos con que [texx]\alpha\lor \beta[/texx], una forma de concluir de ahí que se cumple una fórmula [texx]\gamma[/texx] es probar que cada una de las dos fórmulas por separado implica [texx]\gamma[/texx], esto es lo que se suele llamar "distinguir casos":

Regla del dilema (Dil)  [texx]\alpha\rightarrow \gamma, \beta\rightarrow\gamma\vdash(\alpha\lor\beta)\rightarrow\gamma[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

Un caso particular de argumento "distinguiendo casos" consiste en tomar cualquier fórmula [texx]\alpha[/texx] que sea relevante en la discusión y probar que tanto [texx]\alpha\rightarrow \beta[/texx] como [texx]\lnot\alpha\rightarrow\beta[/texx]. Así, como tenemos [texx]\alpha\lor\lnot\alpha[/texx] por TND, podemos concluir [texx]\beta[/texx] por la regla anterior.

Regla de introducción del disyuntor (ID) [texx]\alpha\vdash \alpha\lor\beta[/texx],   [texx]\beta\vdash\alpha\lor\beta[/texx]

Una es trivial: aplicando el teorema de deducción a la regla de la contradicción obtenemos [texx]\alpha\vdash \lnot\alpha\rightarrow\beta[/texx], pero esto es exactamente lo mismo que [texx]\alpha\vdash \alpha\lor\beta[/texx], por la definición del disyuntor. Para la segunda usamos K1: [texx]\beta\rightarrow(\lnot\alpha\rightarrow\beta)[/texx], que con la premisa nos da [texx]\lnot\alpha\rightarrow\beta[/texx], que es lo mismo que [texx]\alpha\lor\beta[/texx].



Reglas relacionadas con el conjuntor

Las relaciones fundamentales entre el conjuntor y el disyuntor son las llamadas leyes de De Morgan, una de las cuales la hemos tomado como definición del conjuntor y, por consiguiente, su prueba es trivial (ya que se reduce a la regla de repetición):

Leyes de De Morgan (DM)

[texx]
\begin{array}{ll}
\phantom\lnot\alpha\land\beta\vdash\lnot(\lnot\alpha\lor\lnot\beta)&\lnot(\lnot\alpha\lor\lnot\beta)\vdash\alpha\land \beta\\
\phantom\lnot\alpha\lor\beta\vdash\lnot(\alpha\land\lnot\beta)&\lnot(\alpha\land\lnot\beta)\vdash\alpha\lor\beta\\
\lnot(\alpha\land\beta)\vdash \lnot\alpha\lor\lnot\beta&\lnot\alpha\lor\lnot\beta\vdash\lnot(\alpha\land\beta)\\
\lnot(\alpha\land\beta)\vdash \lnot\alpha\lor\lnot\beta&\lnot\alpha\lor\lnot\beta\vdash\lnot(\alpha\land\beta)
\end{array}[/texx]

Según ya hemos dicho, las dos primeras son casos particulares de la regla de repetición, pues las dos fórmulas involucradas son la misma por definición. Para la prueba de las restantes remito a mi libro de lógica (página 48).

Una consecuencia inmediata de las leyes de De Morgan es la regla de no contradicción:

Regla de no contradicción [texx]\vdash\lnot(\alpha\land\lnot\alpha)[/texx]

En efecto, un caso particular de TND es [texx]\lnot\alpha\lor\lnot\lnot\alpha[/texx], y de aquí se pasa a la fórmula que indica la regla por DM.

Regla de introducción del conjuntor (IC)  [texx]\alpha,\beta\vdash \alpha\land \beta[/texx]

La prueba es bastante artificial. Remito a mi libro de lógica (página 48).

Reglas de eliminación del conjuntor (EC) [texx]\alpha\land\beta\vdash\alpha[/texx],   [texx]\alpha\land \beta\vdash \beta[/texx]

También llamaremos (EC) a los resultados [texx]\vdash (\alpha\land\beta)\rightarrow \alpha[/texx],  [texx]\vdash(\alpha\land \beta)\rightarrow \beta[/texx], que resultan de aplicar el teorema de deducción.

Para la prueba de estas reglas remito a mi libro de lógica (página 49).



Reglas relacionadas con el bicondicionador

Para razonar de forma natural con el coimplicador o bicondicionador basta considerar las dos reglas que resultan de combinar su definición (que es una conjunción) con las reglas de introducción y eliminación del conjuntor:

Regla de introducción del bicondicionador (IB) [texx]\alpha\rightarrow\beta, \beta\rightarrow\alpha\vdash \alpha\leftrightarrow\beta[/texx]

Reglas de eliminación del bicondicionador (EB) [texx]\alpha\leftrightarrow\beta\vdash \alpha\rightarrow\beta[/texx],   [texx]\alpha\leftrightarrow\beta\vdash \beta\rightarrow\alpha[/texx]



Las reglas que hemos dado son suficientes para que, contando con ellas, cualquier deducción en [texx]K_{\mathcal L}[/texx] que no requiera tratar con cuantificadores o el igualador pueda realizarse de forma natural, es decir, sin tener que recurrir a combinar de forma "inspirada" axiomas lógicos aplicados a fórmulas elegidas "inspiradamente". En el mensaje siguiente introduciremos las reglas necesarias para poder trabajar del mismo modo con los cuantificadores y el igualador.

Conviene observar que en la deducción de todas las reglas derivadas que hemos visto hasta aquí sólo han intervenido los axiomas K1, K2 y K3 y la regla MP. En particular, como nunca hemos usado IG, todas las reglas pueden usarse libremente aunque estemos trabajando bajo hipótesis adicionales para aplicar el teorema de deducción, pues la aplicación de estas reglas nunca supondrá una generalización inadvertida sobre una variable libre en alguna hipótesis (ni sobre ninguna otra variable).

Las reglas de inferencia que hemos presentado bastan para justificar que una técnica de razonamiento muy habitual en matemáticas es formalizable en [texx]K_{\mathcal L}[/texx]:

Razonamiento por reducción al absurdo

Si en una deducción tomamos [texx]\lnot\alpha[/texx] como premisa adicional y, sin generalizar respecto de variables libres en [texx]\alpha[/texx], llegamos a una contradicción [texx]\beta\land\lnot\beta[/texx], podemos concluir [texx]\alpha[/texx].

Más precisamente, lo que estamos afirmando es que en esta situación:



si a partir del momento en que suponemos [texx]\lnot\alpha[/texx] no generalizamos respecto a variables libres en [texx]\alpha[/texx], la fórmula [texx]\alpha[/texx] escrita en la línea [texx](k+1)[/texx] es deducible en [texx]K_{\mathcal L}[/texx] a partir de las premisas, pero las líneas marcadas con la raya vertical a la izquierda no lo son, porque suponen la hipótesis adicional [texx]\lnot\alpha[/texx].

En efecto, lo que nos dice el teorema de deducción al llegar a la línea [texx](k)[/texx] es que [texx]\lnot\alpha\rightarrow (\beta\land\lnot\beta)[/texx] es deducible de las premisas, luego podríamos haber escrito esta fórmula en la línea [texx](k+1)[/texx], y la deducción podría haber continuado así:

[texx]\begin{array}{lll}
(k+1)&\lnot\alpha\rightarrow (\beta\land\lnot\beta)\\
(k+2)&\lnot (\beta\land\lnot\beta)&\mbox{NC}\\
(k+3)&\lnot\lnot\alpha&\mbox{MT $k+1, k+2$}\\
(k+4)&\alpha&\mbox{DN $k+3$}
\end{array}[/texx]

En la práctica suprimiremos estas líneas y escribiremos directamente [texx]\alpha[/texx] tras haber llegado a una contradicción. En suma:

Una forma válida de concluir [texx]\alpha[/texx] es suponer [texx]\lnot\alpha[/texx] como hipótesis adicional y llegar a una contradicción, con la condición de que a partir de ese momento no se generalice respecto de variables libres en [texx]\alpha[/texx].

Nuevamente, la restricción sobre la generalización es algo que todo matemático respetará de forma instintiva en cada caso concreto. Por ejemplo, supongamos que, en el curso de una prueba, un matematico quiere probar que un cierto [texx]p[/texx] que está considerando es un número primo y se propone hacerlo por reducción al absurdo. Jamás razonaría así:

(1) Supongamos (por reducción al absurdo) [texx]\lnot (p[/texx] es primo)

(2) [texx]\forall p\lnot (p[/texx] es primo) (generalización que viola la restricción sobre el uso de IG)

(3) [texx]\exists p\ (p[/texx] es primo) (resultado probado anteriormente)

(4) [texx]\lnot\forall p\ \lnot (p[/texx] es primo) (equivalencia lógica con 3 que veremos en el mensaje siguiente)

(5)  [texx]\forall p\lnot (p[/texx] es primo) [texx]\land \lnot\forall p\ \lnot(p[/texx] es primo) contradicción

(6) [texx]p[/texx] es primo, por reducción al absurdo.

Esto en realidad no prueba nada. Podemos suponer para llegar a un absurdo que [texx]p[/texx] no es primo, pero no podemos pasar de ahí a que ningún p es primo (que es lo que obtenemos si generalizamos ilegalmente respecto de p).

* cic3.jpg (14.05 KB - descargado 1878 veces.)
* cic4.jpg (21.38 KB - descargado 1911 veces.)
* cic5.jpg (20.93 KB - descargado 1910 veces.)
* cic10.jpg (19.59 KB - descargado 1860 veces.)
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #14 : 24/03/2013, 12:20:04 pm »

Aunque todavía nos falta por dar reglas que nos permitan trabajar de forma natural con los cuantificadores y con el igualador, podemos decir que en este punto "ya hemos desempaquetado la lógica", porque los únicos axiomas "pensados con ingenio" para contener mucha lógica en poco espacio son los axiomas K1, K2, K3 que ya hemos desarrollado, y el axioma K5, que hemos usado únicamente en la prueba del teorema de deducción y no volveremos a usarlo nunca más.

Más concretamente, K5 se usa para probar que el teorema de deducción es aplicable a deducciones que usen IG, pero como en el mensaje anterior sólo lo hemos usado para deducciones que no usaban IG, todo lo dicho hasta aquí es válido incluso sin K5, y ahora sólo lo vamos a usar indirectamente, cuando apliquemos el teorema de deducción a deducciones que usan IG.

Ahora sólo nos falta desarrollar los axiomas K4 y K6, que hasta ahora no hemos usado para nada, y ambos son bastante "naturales", así que ya nunca más vamos a necesitar demostrar nada mediante argumentos "retorcidos".

Reglas relacionadas con los cuantificadores

Las propiedades de los cuantificadores (sin tener en cuenta el uso indirecto de K5 que acabamos de explicar) se siguen todas del axioma K4, que recordamos aquí:

[texx]\forall x\alpha\rightarrow S_x^t\alpha[/texx]

Lo que afirma es muy natural y podemos expresarlo equivalentemente en forma de regla de inferencia:

Regla de eliminación del generalizador (EC) [texx]\forall x\alpha\vdash S_x^t\alpha[/texx]

Lo que afirma esta regla es que si contamos con que todo [texx]x[/texx] cumple lo que dice [texx]\alpha[/texx], entonces podemos afirmar que un término [texx]t[/texx] cualquiera cumple lo que dice [texx]\alpha[/texx].

No damos una regla de introducción del generalizador porque ésta es una de las dos reglas primitivas que hemos usado para definir [texx]K_{\mathcal L}[/texx].

La relación entre el cuantificador universal y el existencial son consecuencia esencialmente de la definición del segundo y de la regla de doble negación:

Reglas de negación del generalizador (NG) [texx]\lnot\forall x\lnot\alpha\vdash \exists x\alpha[/texx],   [texx]\exists x\alpha\vdash \lnot\forall x\lnot\alpha[/texx],     [texx]\lnot\forall x\alpha\vdash \exists x\lnot\alpha[/texx],   [texx]\exists x\lnot\alpha\vdash \lnot\forall x\alpha[/texx]

Las dos primeras son casos particulares de la regla de repetición, pues hemos definido [texx]\exists x\alpha[/texx] precisamente como [texx]\lnot\forall x\lnot\alpha[/texx], luego las dos fórmulas que involucran las reglas son la misma.

Las otras dos sólo requieren aplicar oportunamente la regla de doble negación, lo cual exige eliminar primero el cuantificador para luego volverlo a introducir:

Spoiler: Demostración (click para mostrar u ocultar)

Reglas de negación del particularizador (NP) [texx]\lnot\exists x\alpha\vdash \forall x\lnot\alpha[/texx],    [texx]\forall x\lnot\alpha\vdash \lnot\exists x\alpha[/texx],    [texx]\lnot\exists x\lnot\alpha\vdash \forall x\alpha[/texx],     [texx]\forall x\alpha\vdash \lnot\exists x\lnot\alpha[/texx].

Éstas se prueban más fácilmente incluso que las anteriores, porque al anteponer un negador al particularizador y aplicar la definición de éste, se juntan dos negadores que pueden ponerse o quitarse por DN, y no hacen falta reducciones al absurdo. Dejamos las pruebas al lector y, en todo caso, remito a mi libro de lógica (página 51).

Regla de introducción del particularizador (IP) [texx]S_x^t\alpha\vdash \exists x\alpha[/texx]

Esta regla afirma que si hemos probado que un cierto término [texx]t[/texx] cumple lo que dice [texx]\alpha[/texx], entonces podemos afirmar que existe un [texx]x[/texx] que cumple [texx]\alpha[/texx]. Tenemos un ejemplo de  su uso en la línea 12 de la deducción sobre divisibilidad que pusimos como ejemplo más arriba.

Spoiler: Demostración (click para mostrar u ocultar)

Por último nos falta una "regla de eliminación del particularizador", que es la que aplica un matemático cuando tiene que [texx]\exists x\alpha[/texx] y dice "tomemos un [texx]x[/texx] que cumpla [texx]\alpha[/texx]". Tenemos dos ejemplos en las líneas 5 y 8 de la deducción sobre divisibilidad que pusimos como ejemplo. Ahora bien, esta "regla" no es realmente una regla derivada de inferencia, sino un (meta)teorema análogo al teorema de deducción. Para probarlo necesitamos un hecho previo que tiene interés en sí mismo:

Teorema: Si la variable [texx]y[/texx] no está en la fórmula [texx]\forall x\alpha[/texx], entonces

[texx]\vdash\forall x\alpha\leftrightarrow \forall yS_x^y\alpha,\qquad \vdash \exists x\alpha\leftrightarrow \exists y S_x^y\alpha[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

Regla de eliminación del particularizador (EP):

En esta situación:

[texx]\begin{array}{lll}
(1)&\gamma_1\\
\ \ \vdots&&\mbox{deducción a partir de unas premisas $\alpha_1,\ldots, \alpha_n$}\\
(k)& \exists x\alpha&\\
\ \ \vdots\\
(m)&\gamma_m\\
(m+1)&S_x^y\alpha&\mbox{EP k}\\
\ \ \vdots&&\mbox{deducción a partir de las premisas, las líneas precedentes y $S_x^y\alpha$}\\
\end{array}[/texx]

Si la variable [texx]y[/texx] no está en [texx]\alpha[/texx] o bien [texx]y\equiv x[/texx] (en cuyo caso [texx]S_x^x\alpha\equiv \alpha[/texx]) y a partir de la línea [texx]m+1[/texx] no se generaliza respecto de variables libres en [texx]S_x^y\alpha[/texx], entonces toda línea posterior [texx]\beta[/texx] que no tenga libre la variable [texx]y[/texx] es una consecuencia de las premisas.

Spoiler: Demostración (click para mostrar u ocultar)

Es muy importante observar que en la deducción de [texx]\beta[/texx] a partir de las premisas se generaliza respecto de la variable [texx]y[/texx]. Esto significa que si aplicamos EP en un contexto en el que tenemos prohibido generalizar respecto de ciertas variables, debemos elegir la variable [texx]y[/texx] como una nueva variable sobre la que no exista prohibición de generalizar. Una vez más, esto es algo que el matemático hace instintivamente. Consideremos por ejemplo la deducción sobre divisibilidad que presentamos unos mensajes atrás:

Desde la línea 2, tenemos prohibido generalizar respecto de [texx]x, y, z[/texx]. En la línea 5 eliminamos un particularizador [texx]\exists u[/texx], y no cambiamos de variable porque no hay problema en generalizar respecto de [texx]u[/texx]. A partir de esa línea tenemos prohibido generalizar respecto de [texx]u[/texx], por lo que, cuando queremos eliminar el [texx]\exists u[/texx] de la línea 7 nos vemos obligados a sustituir la variable [texx]u[/texx] por una nueva variable [texx]v[/texx] que tiene que ser distinta de [texx]x, y, z, u[/texx], que son las variables respecto a las que tenemos prohibido generalizar. El matemático hace esto instintivamente cuando piensa que no puede tomar [texx]u[/texx] tal que [texx]z=yu[/texx] porque ya está llamando [texx]u[/texx] a otro número, y mucho menos se le ocurriría llamarlo [texx]x, y, z[/texx] por el mismo motivo, porque sabe que el [texx]u[/texx] que existe por 7 no tiene por qué ser el mismo que cualquiera de los números que está considerando hasta entonces.

Al introducir el particularizador en 12 dejamos de tener libres las variables [texx]u, v[/texx], por lo que todas las fórmulas que siguen son ya auténticas consecuencias de las premisas (y de la hipótesis 2), y podemos aplicar el teorema de deducción para pasar a 14 (hubiera sido incorrecto hacerlo con una fórmula que tuviera libre la variable [texx]u[/texx] o la variable [texx]v[/texx].

Nótese la sutileza: a partir del momento en que suponemos [texx]y=xu[/texx] queda prohibido generalizar respecto de [texx]u[/texx], pero la deducción de [texx]x\mid z[/texx] a partir de las premisas y la hipótesis (2) usa la regla IG respecto de [texx]u[/texx], es decir, tenemos prohibido generalizar, pero a la vez la prueba completa que elimina la premisa adicional [texx]y=xu[/texx] generaliza respecto de [texx]u[/texx]. En general:

Cuando aplicamos EP, debemos reemplazar la variable afectada por el particularizador por una variable respecto a la que sea lícito generalizar hasta ese momento, pero a partir de ese momento tenemos prohibido generalizar respecto de ella.

Como al eliminar un particularizador dejamos libre una variable que no puede quedar libre en la conclusión, la única forma de volver a ligarla es mediante la regla de introducción del particularizador (IP), porque la regla de introducción del generalizador la tenemos prohibida. Aquí es fundamental observar que en la demostración de IP no se generaliza respecto a la variable que particularizamos.

Notemos que es "de sentido común": si una variable procede de eliminar un [texx]\exists u[/texx], luego no podemos ligarla con un [texx]\forall u[/texx], sino que tendremos que volver a introducir un particularizador.

Reglas relacionadas con el igualador

Finalmente vamos a "desempaquetar" la lógica del igualador, que la tenemos toda "empaquetada" en el axioma K6. Si queremos expresar este axioma como reglas de inferencia tenemos trivialmente las dos reglas siguientes:

Reglas de introducción y eliminación del igualador (II, EI)

[texx]S_x^t\alpha\vdash \forall x(x=t\rightarrow \alpha)\qquad \forall x(x=t\rightarrow \alpha)\vdash S_x^t\alpha[/texx]

Estas reglas sólo son aplicables si la variable [texx]x[/texx] no está (libre) en [texx]t[/texx].

Lo que dice aquí es que es equivalente que [texx]t[/texx] cumpla [texx]\alpha[/texx] que cuando [texx]x=t[/texx] entonces [texx]x[/texx] cumple [texx]\alpha[/texx].

De aquí se deducen todas las propiedades que cabe esperar del igualador:

Regla de la identidad (I) [texx]\vdash t=t[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

Regla se la simetría de la identidad (SI) [texx]t_1=t_2\vdash t_2=t_1[/texx]

Regla se la transitividad de la identidad (TI) [texx]t_1=t_2,t_2=t_3\vdash t_1=t_3[/texx]

Para la prueba de las dos reglas precedentes remito a mi libro de lógica (página 52). Veamos la prueba de la propiedad más importante y la que se usa en todo momento cuando se trabaja con igualdades:

Regla de equivalencia entre términos idénticos (ETI) [texx]t_1=t_2, S_x^{t_2}\alpha\vdash S_x^{t_1}\alpha[/texx]

Lo que afirma esta regla es que si tenemos que [texx]t_1=t_2[/texx] y que [texx]t_2[/texx] cumple lo que afirma [texx]\alpha[/texx], entonces lo mismo vale para [texx]t_1[/texx] o, más en general, que si tenemos [texx]t_1=t_2[/texx] entonces todo lo que sepamos de [texx]t_2[/texx] vale también para [texx]t_1[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

* cic6.jpg (19.25 KB - descargado 1883 veces.)
* cic7.jpg (19.4 KB - descargado 1900 veces.)
* cic8.jpg (16.2 KB - descargado 1878 veces.)
* cic9.jpg (9.15 KB - descargado 1864 veces.)
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #15 : 24/03/2013, 22:42:58 pm »

Ahora estamos en condiciones de usar de forma natural el cálculo deductivo que hemos construido. Conviene enriquecer un poco el lenguaje que estamos empleando:

Definición Una teoría axiomática de primer orden [texx]T[/texx] sobre un lenguaje formal [texx]\mathcal L[/texx] es un sistema deductivo formal cuyos axiomas son los de [texx]K_{\mathcal L}[/texx] más quizá otros axiomas adicionales, a los que se les llama axiomas propios de la teoría, y cuyas reglas de inferencia son las de  [texx]K_{\mathcal L}[/texx].

Pese a lo que acabamos de decir, en la práctica es costumbre llamar axiomas de [texx]T[/texx] a sus axiomas propios, y axiomas lógicos de [texx]T[/texx] a los axiomas de [texx]K_{\mathcal L}[/texx].

Una demostración en una teoría axiomática [texx]T[/texx] es una deducción sin premisas (que es lo mismo que una deducción en [texx]K_{\mathcal L}[/texx] que tiene por premisas los axiomas (propios) de [texx]T[/texx]).

Esto hace que todos los resultados que hemos obtenido para deducciones en [texx]K_{\mathcal L}[/texx] son aplicables a toda teoría axiomática [texx]T[/texx], pues las deducciones en [texx]T[/texx] son también deducciones en [texx]K_{\mathcal L}[/texx], sólo que cuentan con premisas adicionales, a saber, los axiomas de [texx]T[/texx].

Las fórmulas demostrables en [texx]T[/texx] (es decir, deducibles sin premisas o deducibles en [texx]K_{\mathcal L}[/texx] tomando como premisas los axiomas de [texx]T[/texx])  se llaman teoremas de [texx]T[/texx].

Si [texx]\lnot\alpha[/texx] es demostrable en [texx]T[/texx] se dice que [texx]\alpha[/texx] es refutable en [texx]T[/texx], y una demostración de [texx]\lnot\alpha[/texx] se llama también una refutación de [texx]\alpha[/texx].

Así [texx]K_{\mathcal L}[/texx] es la teoría axiomática de primer orden más simple posible (la única que no tiene axiomas propios) y sus teoremas se llaman teoremas lógicos. El teorema de completitud semántica (que aún no hemos demostrado) implica que los teoremas lógicos son precisamente las fórmulas lógicamente válidas, es decir, las verdaderas en todos los modelos.

Una teoría axiomática de primer orden [texx]T[/texx] es contradictoria si en ella se puede demostrar una contradicción, es decir, si existe una fórmula [texx]\alpha[/texx] tal que [texx]\vdash_T\alpha\land\lnot\alpha[/texx]. En caso contrario se dice consistente.

Notemos que, por la regla de contradicción, en una teoría contradictoria se pueden demostrar todas las fórmulas, luego sus demostraciones no tienen valor alguno. Recíprocamente, una teoría es consistente si y sólo si hay al menos una fórmula que no sea un teorema.

Una teoría [texx]T[/texx] es completa si para toda sentencia [texx]\alpha[/texx] se cumple [texx]\vdash_T\alpha [/texx] o bien [texx]\vdash_T\lnot \alpha[/texx], es decir, si toda sentencia es demostrable o refutable en [texx]T[/texx].

Spoiler: Nota (click para mostrar u ocultar)

Ejemplo Una teoría axiomática de primer orden es la aritmética de Peano (de primer orden) AP, que es la teoría axiomática cuyo lenguaje formal es el lenguaje de la aritmética que ya hemos descrito (el que tiene una constante [texx]0[/texx], un funtor monádico [texx]S[/texx] y dos funtores diádicos [texx]+[/texx] y [texx]\cdot[/texx]) y cuyos axiomas (propios) son:

[texx]\forall x\ Sx\neq 0[/texx]

[texx]\forall xy(Sx=Sy\rightarrow x=y)[/texx]

[texx]\forall x(x+0=x)[/texx]

[texx]\forall xy(x+Sy=S(x+y))[/texx]

[texx]\forall x(x\cdot 0=0)[/texx]

[texx]\forall xy(x\cdot Sy = (x\cdot y)+x)[/texx]

[texx]\alpha(0)\land \forall x(\alpha(x)\rightarrow \alpha(Sx))\rightarrow \forall x\alpha(x)[/texx], para toda fórmula [texx]\alpha[/texx].

Notemos que usamos la notación [texx]\alpha(0)\equiv S_x^0\alpha[/texx],      [texx]\alpha(Sx)\equiv S_x^{Sx}\alpha[/texx].



Introducidos estos conceptos, nos centramos ahora en ilustrar el concepto de deducción formal. Tomemos este ejemplo:

[texx]\alpha\rightarrow \alpha',\beta\rightarrow \beta'\vdash (\alpha\lor \beta)\rightarrow (\alpha'\lor\beta')[/texx]

Lo importante es que estamos en condiciones de probar esto (y cualquier otra cosa) razonando exactamente como razonaría un matemático. Un matemático razonaría así:

Tenemos como premisas que [texx]\alpha\rightarrow \alpha'[/texx] y [texx]\beta\rightarrow \beta'[/texx]. Para probar [texx](\alpha\lor \beta)\rightarrow (\alpha'\lor\beta')[/texx] suponemos [texx]\alpha\lor\beta[/texx] y queremos probar [texx]\alpha'\lor\beta'[/texx]. Para probar una disyunción suponemos que no se cumple una de las partes y demostramos la otra. Suponemos, pues, [texx]\lnot\alpha'[/texx]. Entonces, por la primera premisa, [texx]\lnot\alpha[/texx] y como suponemos [texx]\alpha\lor \beta[/texx], tiene que ser [texx]\beta[/texx], luego por la segunda premisa [texx]\beta'[/texx], como queríamos probar.

Si ponemos esto en orden nos queda:



Si alguien lee esto y el razonamiento le parece artificial o enrevesado, significa que no está bien familiarizado con la lógica formal, y es con esto con lo que necesita familiarizarse, tiene que aprender a hacer deducciones formales como ésta y llegar a verlas naturales, no tiene que esforzarse por entender e imaginar deducciones kafkianas a partir de axiomas kafkianos, como las que hemos considerado en los mensajes anteriores para "desempaquetar" la lógica. El razonamiento formal es razonar así y no razonar como hemos tenido que hacer antes de poder llegar hasta aquí.

Por supuesto, las reglas de inferencia que hemos presentado en los mensajes precedentes no son las únicas posibles, ni forman ninguna especie de club selecto al que no se puede añadir nada más. Por el contrario, todos los resultados que demostremos y que puedan considerarse lo suficientemente generales como para que puedan ser de utilidad en diferentes contextos pueden y deben ser incorporados a la lista de resultados "utilizables" siempre que sea conveniente.

Por ejemplo, si tenemos [texx]\alpha\leftrightarrow \beta[/texx] y [texx]\alpha[/texx], podemos concluir [texx]\beta[/texx], esto no es exactamente MP porque tenemos una coimplicación, pero está claro que de la coimplicación podemos deducir la implicación (EB) y a ésta le podemos aplicar MP. En la práctica no hay ningún inconveniente en dar los dos pasos en uno si sabemos lo que estamos haciendo.

Vamos a enumerar aquí algunos resultados de utilidad general:

Resultados sobre coimplicaciones

[texx]\vdash \alpha\leftrightarrow \alpha[/texx]

[texx]\alpha\leftrightarrow\beta\vdash \beta\leftrightarrow \alpha[/texx]

[texx]\alpha\leftrightarrow \beta, \beta\leftrightarrow \gamma\vdash\alpha\leftrightarrow\gamma[/texx]

[texx]\alpha\leftrightarrow\beta\vdash \lnot\alpha\leftrightarrow \lnot\beta[/texx]

[texx]\alpha\leftrightarrow \alpha', \beta\leftrightarrow \beta'\vdash (\alpha\land\beta)\leftrightarrow (\alpha'\land \beta')[/texx]

[texx]\alpha\leftrightarrow \alpha', \beta\leftrightarrow \beta'\vdash (\alpha\lor\beta)\leftrightarrow (\alpha'\lor \beta')[/texx]

[texx]\alpha\leftrightarrow \alpha', \beta\leftrightarrow \beta'\vdash (\alpha\rightarrow \beta)\leftrightarrow (\alpha'\rightarrow \beta')[/texx]

[texx]\alpha\leftrightarrow \alpha', \beta\leftrightarrow \beta'\vdash (\alpha\leftrightarrow \beta)\leftrightarrow (\alpha'\leftrightarrow \beta')[/texx]

[texx]\alpha\leftrightarrow \alpha'\vdash \forall x\alpha\leftrightarrow \forall x\alpha'[/texx]

[texx]\alpha\leftrightarrow \alpha'\vdash \exists x\alpha\leftrightarrow \exists x\alpha'[/texx]

Spoiler: Demostración (click para mostrar u ocultar)

El álgebra del cálculo proposicional

A menudo es útil sustituir una fórmula por otra lógicamente equivalente con otra estructura, normalmente con intención de llegar a expresiones más simples o más manejables. Para ello ayudan las propiedades siguientes (donde usamos la notación [texx]\top[/texx] para nombrar cualquier fórmula que sea un teorema lógico y [texx]\bot[/texx] para representar cualquier fórmula cuya negación sea un teorema lógico:

[texx]\vdash (\alpha\land \beta)\land \gamma\leftrightarrow \alpha\land (\beta\land \gamma)[/texx]

[texx]\vdash (\alpha\lor \beta)\lor \gamma\leftrightarrow \alpha\lor (\beta\lor \gamma)[/texx]

[texx]\vdash (\alpha\land \beta)\leftrightarrow (\beta\land \alpha)[/texx]

[texx]\vdash (\alpha\lor \beta)\leftrightarrow (\beta\lor \alpha)[/texx]

[texx]\vdash \alpha\land (\beta\lor\gamma)\leftrightarrow (\alpha\land\beta)\lor (\alpha\land \gamma)[/texx]

[texx]\vdash \alpha\lor (\beta\land\gamma)\leftrightarrow (\alpha\lor\beta)\land (\alpha\lor \gamma)[/texx]

[texx]\vdash \alpha\lor \bot\leftrightarrow \alpha[/texx]

[texx]\vdash \alpha\land \top\leftrightarrow \alpha[/texx]

[texx]\vdash\alpha\lor\lnot\alpha\leftrightarrow \top[/texx]

[texx]\vdash\alpha\land\lnot\alpha\leftrightarrow \bot[/texx]

Los dos primeros resultados justifican que escribamos [texx]\alpha_1\land \cdots \land \alpha_n[/texx] y [texx]\alpha_1\lor \cdots \lor \alpha_n[/texx] sin paréntesis, porque las fórmulas resultantes son equivalentes sin que importe cómo se disponen los paréntesis.

Spoiler: Demostración (click para mostrar u ocultar)

El spoiler siguiente contiene una observación marginal:

Spoiler: El álgebra de Lindenbaum-Tarski (click para mostrar u ocultar)

Ejemplos de deducciones con cuantificadores

Para terminar veamos algunos ejemplos que involucren las reglas sobre cuantificadores:

[texx]\forall xy(Bxy\rightarrow Sy), \exists x(\lnot Bxa\rightarrow Cx), \forall x\lnot Cx\vdash \exists ySy[/texx]

(Aquí se entiende que [texx]B, S, C,[/texx] son relatores y que [texx]a[/texx] es una constante.)

Spoiler: Solución (click para mostrar u ocultar)

[texx]\exists y\forall x(Pxy\rightarrow Rxy), \forall yz\ Pyz\vdash \forall y\exists z\ Ryz[/texx]

Spoiler: Solución (click para mostrar u ocultar)

[texx]\exists x(Pxa\rightarrow Qx), \forall y\lnot Qy,\forall xy(\lnot Rxy\lor Pxy)\vdash \exists xy\lnot Rxy[/texx]

Spoiler: Solución (click para mostrar u ocultar)

* cic11.jpg (20.8 KB - descargado 1902 veces.)
* cic12.jpg (22.29 KB - descargado 1871 veces.)
* cic13.jpg (24.31 KB - descargado 1900 veces.)
* cic14.jpg (71.97 KB - descargado 1903 veces.)
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #16 : 03/04/2013, 07:56:39 am »

En este mensaje demostraremos finalmente que el cálculo deductivo que hemos definido es justo lo que tiene que ser, es decir, que permite deducir de unas premisas todas las consecuencias que cabe esperar que puedan deducirse. Aunque en este artículo pretendo centrarme en los aspectos prácticos de lo que supone realizar deducciones en el cálculo deductivo de primer orden, demostrar el teorema de completitud es obligado para terminar de justificar que lo que estamos haciendo es correcto. Por ello este mensaje tendrá un nivel mucho más técnico que los anteriores y que los siguientes, y en realidad nada de lo que veremos aquí será necesario para lo que diremos después, por lo que el lector puede pasar directamente al mensaje siguiente si así lo prefiere.

Aunque la tarea que pretendemos realizar aquí ya ha sido perfilada en los mensajes anteriores, no está de más acabar de centrarla:

Si nos fijamos en cómo razonan en la práctica los matemáticos, veremos que en realidad nunca se cuidan de comprobar si, en efecto, todo cuanto dicen puede justificarse paso a paso aplicando oportunamente las reglas de inferencia de [texx]K_{\mathcal L}[/texx], de si en tal paso tienen permitido aplicar o no IG, etc. Esto puede interpretarse de dos modos distintos: La interpretación más formal es que sus demostraciones son en realidad esbozos de demostración, lo suficientemente detallados como para que cualquiera que se lo proponga pueda desarrollarlos hasta convertirlos en auténticas demostraciones, paso a paso, en [texx]K_{\mathcal L}[/texx]. Pero la realidad es que cuando un matemático razona y valora si sus razonamientos son correctos o no, no tiene en cuenta para nada si tal o cual cosa se podrá justificar con EDI o con MB, sino que da por bueno un argumento si se convence de que si sus hipótesis son ciertas sus conclusiones también tienen que serlo. Pero ¿ciertas en qué sentido? El matemático no se plantea eso, pero no es difícil responder: se da por satisfecho cuando se convence de que si unos objetos (los que sean) cumplen sus hipótesis, necesariamente tienen que cumplir también sus conclusiones. Se puede decir que el matemático en la práctica razona semánticamente (es decir, preocupado de no pasar nunca de afirmaciones verdaderas a falsas) y no formalmente (preocupado de aplicar sólo unas reglas de razonamiento prefijadas).

El problema de razonar semánticamente (si uno quiere a la vez ser riguroso) es que en principio nos pone en la obligación de explicar de qué estamos hablando (es decir, de explicar qué objetos se supone que cumplen nuestras afirmaciones para que podamos decir con sentido ``si nuestras hipótesis son verdaderas\ldots") Lo que suele hacer el matemático si le piden este tipo de explicaciones es dar la respuesta fácil (y válida) de que, en realidad, se podría comprobar que todo cuanto razona puede ser formalizado en [texx]K_{\mathcal L}[/texx], y eso basta para que sus razonamientos sean rigurosos. En efecto, esto resuelve el problema de fundamentar su trabajo ``sin agujeros", porque razonar formalmente en [texx]K_{\mathcal L}[/texx] es un proceso objetivo y bien definido, pero, ¿de verdad hace falta recurrir al ``se podría comprobar"? ¿Es casualidad que todo lo que un matemático razona sin preocuparse de[texx]K_{\mathcal L}[/texx] al final resulta que, en efecto, puede formalizarse en [texx]K_{\mathcal L}[/texx]? ¿No puede justificarse que razonar semánticamente tiene sentido sin refugiarse en [texx]K_{\mathcal L}[/texx]?

En este mensaje responderemos afirmativamente a las dos últimas preguntas. De hecho, veremos que la respuesta a la segunda lleva fácilmente a la respuesta a la primera. Notemos en primer lugar que para que tenga sentido razonar formalmente no es necesario dar un modelo explícito de los axiomas aceptados, porque el argumento no es: ``tales objetos concretos cumplen lo que digo", sino ``si unos objetos (los que sean) cumplen mis axiomas, también tienen que cumplir mis teoremas", por lo que sólo necesitamos justificar que existen unos objetos (los que sean) que cumplan mis axiomas.

Eso es precisamente lo que afirma el teorema siguiente, debido a Gödel (aunque la prueba que daremos se debe a Henkin):

Teorema: Una teoría axiomática es consistente si y sólo si tiene un modelo.

(Un modelo de una teoría axiomática es un modelo en el que sus axiomas, y por consiguiente sus teoremas, son verdaderos.) Por lo tanto, el único requisito para que el razonamiento semántico tenga sentido es garantizar que sus axiomas son consistentes (requisito obviamente necesario, por otra parte). Ahora bien, una cosa es que tenga sentido y otra distinta que razonar semánticamente sea lo mismo que razonar formalmente. El teorema que garantiza esto es el que se conoce propiamente como teorema de completitud semántica de Gödel:

Teorema de completitud semántica Si [texx]\Gamma[/texx] es una colección de fórmulas de un lenguaje formal y [texx]\alpha[/texx] es una fórmula tal que [texx]\Gamma\vDash \alpha[/texx], es decir, tal que podemos razonar que [texx]\alpha[/texx] es necesariamente verdadera en todo modelo en el que las fórmulas de [texx]\Gamma[/texx] son verdaderas, entonces [texx]\Gamma\vdash \alpha[/texx].

Esto significa que todo razonamiento semántico (de tipo: si las premisas son verdad entonces la conclusión es verdad) es formalizable en [texx]K_{\mathcal L}[/texx].

Como el segundo teorema es una consecuencia sencilla del primero y el primero se usa bastante más que el segundo, es frecuente llamar también "teorema de completitud" al primero, aunque el nombre no le corresponde propiamente. Pasemos a demostrarlos.

Ante todo, es inmediato que si una teoría axiomática tiene un modelo entonces es consistente, pues en tal caso todos sus teoremas tienen que ser verdaderos en el modelo, luego hay sentencias que no pueden ser demostradas (las que son falsas en el modelo, recordemos que una sentencia y su negación no pueden ser ambas verdaderas en un modelo). El problema es demostrar el recíproco. Si llamamos [texx]\Gamma[/texx] a la colección de los axiomas de una teoría formal, se trata de probar que si [texx]\Gamma[/texx] es consistente (es decir, si de [texx]\Gamma[/texx] no se deducen contradicciones), entonces [texx]\Gamma[/texx] tiene un modelo.

En principio no hay inconveniente en que las fórmulas de [texx]\Gamma[/texx] tengan variables libres, pero en primer lugar observamos que no perdemos generalidad si suponemos que no las tienen, es decir, que son sentencias.

Spoiler: Demostración (click para mostrar u ocultar)

Así pues, basta probar que si [texx]\Gamma[/texx] es una colección consistente de sentencias de un lenguaje formal, entonces [texx]\Gamma[/texx] tiene un modelo.

Vamos a necesitar un hecho elemental sobre consistencia:

Teorema: Sea [texx]\Gamma[/texx] una colección de fórmulas y [texx]\alpha[/texx] una sentencia. Entonces [texx]\Gamma\cup\{\alpha\}[/texx] es consistente si y sólo si no [texx]\Gamma\vdash \lnot\alpha[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Notemos que este resultado se usa de forma habitual casi sin nombrarlo. Por ejemplo, es lo mismo decir que la hipótesis del continuo es consistente con ZFC que decir que no puede demostrarse que es falsa.

Definición Diremos que una colección de sentencias [texx]\Gamma[/texx] es maximalmente consistente si es consistente y para toda sentencia [texx]\alpha[/texx] se cumple que [texx]\Gamma\cup\{\alpha\}[/texx] es contradictoria.

Notemos que si una colección de sentencias [texx]\Gamma[/texx] tiene un modelo [texx]M[/texx], entonces [texx]\Gamma[/texx] se extiende a una colección maximalmente consistente de sentencias. Basta tomar la colección de todas las sentencias verdaderas en [texx]M[/texx]. Dicha colección contiene a toda sentencia [texx]\alpha[/texx] o bien a su negación, luego si intentamos añadirle una sentencia más, pasamos a una teoría contradictoria, pues contendrá la sentencia añadida y su negación.

De lo que se trata es de probar que toda colección consistente de sentencias puede extenderse a una colección maximalmente consistente (sin suponer que tiene un modelo) y usar esta extensión para construir el modelo.

Antes de ello observamos algunas consecuencias sencillas de la definición:

Teorema Sean [texx]\Gamma[/texx] una colección maximalmente consistente de sentencias de un lenguaje formal y sean [texx]\alpha,\beta[/texx] dos sentencias de dicho lenguaje. Entonces:

a) [texx]\Gamma\vdash \alpha[/texx] si y sólo si [texx]\alpha[/texx] está en [texx]\Gamma[/texx].

b) [texx]\Gamma[/texx] contiene a todos los teoremas lógicos (sin variables libres).

c) [texx]\lnot\alpha[/texx] está en [texx]\Gamma[/texx] si y sólo si [texx]\alpha[/texx] no está en [texx]\Gamma[/texx].

d) [texx]\alpha\rightarrow\beta[/texx] está en [texx]\Gamma[/texx] si y sólo si [texx]\alpha[/texx] no está en [texx]\Gamma[/texx] o [texx]\beta[/texx] está en [texx]\Gamma[/texx].

e) [texx]\alpha\lor\beta[/texx] está en [texx]\Gamma[/texx] si y sólo si [texx]\alpha[/texx] está en [texx]\Gamma[/texx] o [texx]\beta[/texx] está en [texx]\Gamma[/texx].

f) [texx]\alpha\land\beta[/texx] está en [texx]\Gamma[/texx] si y sólo si [texx]\alpha[/texx] y [texx]\beta[/texx] están en [texx]\Gamma[/texx].

g) [texx]\alpha\leftrightarrow \beta[/texx] está en [texx]\Gamma[/texx] si y sólo si [texx]\alpha[/texx] y [texx]\beta[/texx] están ambas en [texx]\Gamma[/texx] o ninguna lo está.


Notemos que este teorema es puramente sintáctico, pero tiene ya un "sabor" semántico, en el sentido de que está poniendo de manifiesto la interpretación de los conectores lógicos.

Spoiler: Demostración (click para mostrar u ocultar)

Necesitamos resultados análogos a los anteriores para los cuantificadores, pero para ello no basta la consistencia maximal:

Definición: Una colección [texx]\Gamma[/texx] de sentencias de un lenguaje formal es ejemplificada si cuando [texx]\exists x\alpha[/texx] está en [texx]\Gamma[/texx] existe un designador [texx]t[/texx] (un término sin variables libres) tal que [texx]S_x^t\alpha[/texx] está en [texx]\Gamma[/texx].

Es decir, si siempre que [texx]\Gamma[/texx] afirma la existencia de un [texx]x[/texx] que cumple algo, también pone un ejemplo de un [texx]t[/texx] concreto que cumple ese algo.

Teorema Sea [texx]\Gamma[/texx] una colección de sentencias maximalmente consistente y ejemplificada y sea [texx]\alpha[/texx] una fórmula en la que a lo sumo esté libre la variable [texx]x[/texx]

a) [texx]\exists x\alpha[/texx] está en [texx]\Gamma[/texx] si y sólo si existe un designador [texx]t[/texx] del lenguaje formal considerado tal que [texx]S_x^t\alpha[/texx] está en [texx]\Gamma[/texx].

b) [texx]\forall x\alpha[/texx] está en [texx]\Gamma[/texx] si y sólo si para todo designador [texx]t[/texx] del lenguaje formal se cumple que [texx]S_x^t\alpha[/texx] está en [texx]\Gamma[/texx].


Spoiler: Demostración (click para mostrar u ocultar)

Nuestro objetivo es obtener una colección maximalmente consistente y ejemplificada de sentencias a partir de una colección consistente. Para ello necesitamos el siguiente resultado técnico:

Teorema Si una constante [texx]c[/texx] no está en una fórmula [texx]\alpha[/texx], la variable [texx]x[/texx] no está ligada en [texx]\alpha[/texx] y [texx]\vdash S_x^c\alpha[/texx], entonces [texx]\vdash\alpha[/texx].

La demostración de este teorema es una rutinaria inducción sobre la longitud de una demostración de [texx]S_x^c\alpha[/texx] como muchas otras que hemos visto. Remito a mi libro de lógica para la prueba (teorema 4.10). La idea de fondo es que en una demostración da igual referirse a un objeto con una constante o con una variable que no se use para nada más, de modo que si en la demostración con la constante se sustituye sistemáticamente ésta por una variable "nueva", que no aparezca en la prueba para nada, lo que sale sigue siendo una demostración.

A partir de aquí demostramos el resultado que nos permite ejemplificar una sentencia:

Teorema Si [texx]\Gamma\cup\{\exists x\alpha\}[/texx] es una colección consistente de sentencias de un lenguaje formal y [texx]c[/texx] es una constante que no esté en ninguna de sus sentencias, entonces [texx]\Gamma\cup\{\exists x\alpha,S_x^c\alpha\}[/texx] es consistente.

Spoiler: Demostración (click para mostrar u ocultar)

Ahora viene el teorema fundamental, el núcleo del argumento que prueba el teorema de completitud. Si alguien se pregunta qué necesitamos suponer sobre las colecciones metamatemáticas que estamos usando, la respuesta es muy simple: ni más ni menos que lo necesario para reconocer que el argumento del teorema siguiente tiene sentido y es concluyente. En este teorema aparecen las colecciones de objetos más generales que hemos necesitado o vamos a necesitar.

Teorema Sea [texx]\mathcal L[/texx] un lenguaje formal, sea [texx]\mathcal L'[/texx] el lenguaje formal que resulta de añadir a [texx]\mathcal L[/texx] una sucesión de constantes [texx]d_0,d_1,d_2,\ldots[/texx], sea [texx]\Gamma[/texx] una colección consistente de sentencias de [texx]\mathcal L[/texx]. Entonces existe una colección [texx]\Gamma_\infty[/texx] maximalmente consistente y ejemplificada de sentencias de [texx]\mathcal L[/texx] que contiene a [texx]\Gamma[/texx].

Spoiler: Demostración (click para mostrar u ocultar)

Observaciones El lector no debe dejarse confundir por la notación conjuntista que hemos empleado (hemos hablado de uniones infinitas y otras cosas) que sólo sirve para simplificar la exposición. El argumento de la prueba es, en cierto sentido, elemental: tenemos numeradas las sentencias de [texx]\mathcal L'[/texx] y lo que hacemos es ir recorriéndolas todas una por una y decidiendo si la añadimos o no a la extensión de [texx]\Gamma[/texx] que vamos construyendo: si cada sentencia es consistente con las que ya tenemos, la añadimos (y si es existencial la ejemplificamos de paso) y si es contradictoria con las que ya tenemos la rechazamos. Eso es todo, sin necesidad de considerar uniones ni historias.

El punto delicado es que puede probarse que no existe un algoritmo para decidir si una colección de fórmulas es consistente o no, aunque sea finita. Por lo tanto, en cada paso tenemos un criterio muy concreto y definido que determina si cada sentencia [texx]\alpha_n[/texx] tiene que ser añadida o no a la colección que estamos definiendo, pero no sabemos comprobar en la práctica si [texx]\alpha_n[/texx] lo satisface o no. Esto hace que [texx]\Gamma_\infty[/texx] esté perfectamente definida y que sus elementos dependan únicamente de la ordenación que hemos dado  a las fórmulas (si [texx]\alpha[/texx] y [texx]\lnot\alpha[/texx] son consistentes con [texx]\Gamma[/texx], añadiremos una o la otra según cuál aparezca antes en la enumeración), pero en general no podemos decir cuáles son sus elementos.

Ahora ya podemos probar que toda colección consistente de sentencias tiene un modelo.

Spoiler: Demostración (click para mostrar u ocultar)

Notemos que hemos demostrado algo un poco más fuerte:

Teorema: Si una colección [texx]\Gamma[/texx] de fórmulas es consistente, entonces tiene un modelo (de universo) numerable.

La numerabilidad tiene consecuencias notables a la hora de entender la lógica de la teoría de conjuntos, pero no vamos a entrar en ello. De momento lo que nos interesa es que ya hemos probado que, si tenemos una teoría axiomática consistente, tiene sentido razonar semánticamente en ella, pues existen unos objetos (con las relaciones y funciones adecuadas) para los cuales los axiomas son verdaderos, luego tiene sentido plantearse qué fórmulas son necesariamente verdaderas en un modelo en el que los axiomas sean verdaderos, y eso es razonar semánticamente (razonar informalmente con afirmaciones expresadas como fórmulas de un lenguaje formal).

Ahora nos falta probar que razonar semánticamente es equivalente a razonar formalmente, es decir, vamos a demostrar el teorema de completitud. La prueba es elemental:

Spoiler (click para mostrar u ocultar)

Terminamos con un par de observaciones. La primera es que hemos demostrado lo siguiente:

Teorema de Löwenheim-Skolem Si una teoría axiomática tiene un modelo, entonces tiene un modelo numerable.

La segunda es que cuando definimos el concepto de fórmula lógicamente válida advertimos de que debíamos entenderlo como que una fórmula [texx]\alpha[/texx] es lógicamente válida, no si es verdadera en todo modelo, sino si tenemos un argumento que nos convence de que tiene que ser verdadera en todo modelo. Ahora podemos simplificar esto. Hay dos posibilidades: o bien [texx]\vdash \alpha[/texx] o bien no [texx]\vdash\alpha[/texx]. En el primer caso existe un razonamiento que nos convence de que [texx]\alpha[/texx] tiene que ser verdadera en todo modelo (el razonamiento informal codificado por una demostración formal de [texx]\alpha[/texx]). En el segundo caso sabemos que [texx]\lnot\alpha[/texx] es consistente, luego tiene un modelo, de modo que existe un modelo en el que [texx]\alpha[/texx] no es verdadera.

En definitiva, el concepto de fórmula lógicamente válida ya no depende de si sabemos o no encontrar un argumento. Podemos decir que una fórmula es lógicamente válida si es verdadera en todo modelo, pues, o bien existe un argumento que lo justifique (lo conozcamos o no) o bien existe un modelo que lo refuta (lo conozcamos o no).
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #17 : 03/04/2013, 18:14:11 pm »

Nadie puede tener una idea clara de la razón de ser de toda la teoría que hemos presentado hasta aquí sin comprender el papel que desempeña en la fundamentación de la teoría de conjuntos. Como no se trata aquí de entrar en los detalles de las teorías axiomáticas de conjuntos, vamos a plantear una muy simple, que es suficiente para ilustrar las ideas que queremos discutir aquí:

Definición El lenguaje de la teoría de conjuntos [texx]\mathcal L_{\rm tc}[/texx] es el  lenguaje formal cuyo único signo eventual es un relator diádico que representaremos por [texx]\in[/texx] y lo llamaremos {\it relator de pertenencia.} Escribiremos [texx]t_1\notin t_2\equiv \lnot t_1\in t_2[/texx]. También es frecuente abreviar [texx]
\forall u\in x\,\alpha\equiv \forall u(u\in x\rightarrow \alpha),\ \  \exists u\in x\, \alpha\equiv \exists u(u\in x\land \alpha).
[/texx]

La teoría básica de conjuntos es la teoría axiomática T cuyos axiomas son las sentencias siguientes:

[texx]\begin{array}{ll}
\mbox{Extensionalidad}&\forall xy(\forall u(u\in x\leftrightarrow u\in y)\rightarrow x=y)\\[1mm]
\mbox{Vacío}&\exists x\forall u\ u\notin x\\[1mm]
\mbox{Par}&\forall xy\exists z\forall u(u\in z\leftrightarrow u=x\lor u=y)\\[1mm]
\mbox{Unión}&\forall x\exists y\forall u(u\in y\leftrightarrow \exists v(u\in v\land v\in x))\\[1mm]
\mbox{Diferencia}&\forall xy\exists z\forall u(u\in z\leftrightarrow u\in x\land u\notin y)
\end{array}
[/texx]

Vamos a analizar esta definición. Ante todo observemos que todo lo dicho tiene sentido. La definición anterior determina exactamente qué es una fórmula del lenguaje [texx]\mathcal L_{\rm tc}[/texx], qué es lo que significa "ser un axioma" de [texx]\mathcal L_{\rm tc}[/texx] y, por consiguiente, está perfectamente determinado qué significa "ser un teorema" de [texx]\mathcal L_{\rm tc}[/texx]. Podemos ponernos ya mismo a demostrar formalmente teoremas de [texx]\mathcal L_{\rm tc}[/texx] y todo esto podemos hacerlo sin responder en ningún momento a la pregunta de "qué significa [texx]\in[/texx]".

Más aún, vamos a establecer, no sin cierta dosis de cinismo, que cuando leamos sentencias de [texx]\mathcal L_{\rm tc}[/texx], cada vez que nos encontremos con un [texx]\forall x[/texx] leeremos "para todo conjunto [texx]x[/texx]", cada vez que nos encontremos con un [texx]\exists x[/texx] leeremos "existe un conjunto [texx]x[/texx] tal que", y cuando nos encontremos con una fórmula [texx]x\in y[/texx] leeremos que "el conjunto [texx]x[/texx] pertenece a (o es un elemento de) el conjunto [texx]y[/texx]", y si alguien nos pregunta qué queremos decir cuando hablamos de "conjuntos" y de "pertenencia", le responderemos que nada, que es sólo una forma cómoda de leer las fórmulas de [texx]\mathcal L_{\rm tc}[/texx]. Y lo bueno es que nadie podrá acusarnos de falta de rigor.

Más concretamente, podemos leer el axioma de extensionalidad diciendo que "si dos conjuntos [texx]x[/texx] e [texx]y[/texx] tienen los mismos elementos, entonces son iguales", y podemos trabajar con esta afirmación, y deducir consecuencias lógicas de ella y los demás axiomas, sin necesidad de dar explicaciones sobre qué son esos conjuntos y esa relación de pertenencia de la que se supone que estamos hablando.

Si nos cansamos de ser cínicos y preferimos ser algo más conciliadores, podemos decir que suponemos que existen unos objetos llamados conjuntos, entre los cuales está definida una relación de pertenencia, y de forma que, cuando consideramos el modelo de [texx]\mathcal L_{\rm tc}[/texx] cuyo universo es la colección de todos esos conjuntos e interpretamos el relator [texx]\in[/texx] como la relación de pertenencia, todos los axiomas de T resultan ser verdaderos.

Pero si nos preguntan si tenemos garantías de que existen realmente tales objetos y tal relación, o si podemos poner algún ejemplo de objetos que realmente cumplan esos axiomas, podemos responder sin vacilar que no necesitamos responder a ninguna de esas preguntas para trabajar rigurosamente con la teoría~ T, porque para razonar formalmente no es necesario conocer los objetos sobre los que presuntamente estamos razonando, sino que basta con respetar las reglas sintácticas de [texx]\mathcal L_{\rm tc}[/texx] y las reglas deductivas de [texx]K_{\mathcal L_{\rm tc}}[/texx].

En resumen: todo el aparato lógico que hemos montado hasta aquí nos sirve ahora para que podamos hablar de conjuntos y de pertenencia sin necesidad de responder a ninguna pregunta embarazosa sobre qué son los conjuntos y qué es la pertenencia. Nos basta con suponer que los conjuntos y la pertenencia cumplen los axiomas de T y respetar en todo momento las reglas de deducción formal que hemos establecido.

En la práctica, cuando uno ya está habituado a estas situaciones y no necesita dar tantas vueltas a estos hechos, abrevia diciendo simplemente que los conceptos de "conjunto" y "pertenencia" son los conceptos primitivos (o no definidos) de la teoría T.

La lógica formal tendrá mil virtudes, pero si hoy tiene el grado de desarrollo que tiene, es porque sirve precisamente para esto: para justificar que uno se ponga a hablar de cosas sin decir de qué cosas está hablando y sin que nadie le pueda reprochar falta de rigor por ello. La fundamentación de las matemáticas consiste esencialmente en eso: en poder hablar de conjuntos y de pertenencia sin verse en la necesidad (o en el aprieto) de explicar qué significan exactamente estas palabras. De ahí el énfasis que hemos puesto en todo momento en la posibilidad de definir formalmente con rigor todos los conceptos sintácticos (fórmulas, axiomas, teoremas, etc.) sin hacer referencia en ningún momento a modelos, porque cuando llega el momento de introducir una teoría de conjuntos no sabríamos cómo justificar que nuestros axiomas tienen un modelo (en el caso de T es relativamente fácil hacerlo, pero en las teorías de conjuntos "para adultos" es práctica y teóricamente imposible). Lo bueno, lo que valdría su peso en oro si no fuera porque las buenas ideas no pesan, es que podemos decir con toda la autosuficiencia del mundo: "ni sé decirte nada sobre qué es un conjunto o qué cosas pueden formar un modelo de la teoría de conjuntos, ni tengo necesidad alguna de hacerlo para desarrollar con perfecto rigor formal toda la matemática".

Una vez eximidos de la necesidad de explicar qué es un conjunto o qué es la relación de pertenencia, nada nos impide tratar de formarnos una idea sobre qué características tendrían que tener unos objetos para cumplir los axiomas de~T. Si [texx]x[/texx] es un conjunto, entonces podemos hablar de la colección (en el sentido intuitivo de la palabra) de todos los conjuntos que cumplen [texx]u\in x[/texx]. En principio, esa colección recibe el nombre de la extensión de [texx]x[/texx], y lo que dice el axioma de extensionalidad es que si dos conjuntos tienen la misma extensión, entonces son iguales.

De aquí obtenemos dos cosas: por una parte, cada conjunto (en el sentido técnico, no definido de la palabra) tiene asociada una colección de objetos (su extensión) y en segundo lugar está completamente determinado por ella, de modo que lo único que diferencia a un conjunto de otro es que haya otros conjuntos que pertenezcan a uno y no al otro. Por lo tanto, podemos identificar a un conjunto con su extensión. Podemos considerar que, cuando hablamos de un conjunto, en realidad estamos hablando de su extensión. Según esto, los conjuntos son colecciones de objetos (colecciones de conjuntos). Eso sí, sería ingenuo y catastrófico identificar "conjunto" y "colección de conjuntos". Si [texx]M[/texx] es un modelo de T y consideramos unos cuantos objetos de [texx]M[/texx], nadie nos asegura que exista un conjunto (es decir, un elemento de [texx]M[/texx]) cuya extensión sea precisamente la colección de objetos de [texx]M[/texx] que hemos tomado, ni tampoco hay ninguna condición sencilla que nos permita decir: "de entre las colecciones de objetos de [texx]M[/texx], son conjuntos las que cumplen tal cosa". El concepto de "conjunto" es un concepto técnico: son conjuntos las colecciones de conjuntos que conviene que lo sean para que se cumplan los axiomas, y no lo son las que no conviene que lo sean. Y punto. De hecho, sucede que que en todo modelo de T hay colecciones de conjuntos que no son (extensiones de) conjuntos.

En el mensaje siguiente desarrollaremos un poco la teoría T para tratar de describir el papel de la lógica que hemos estudiado (y de algún concepto que tenemos pendiente de introducir) en el razonamiento matemático. La teoría T parece poca cosa, pero sus axiomas bastan para definir los números naturales (aunque no la suma de números naturales).
En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #18 : 07/04/2013, 07:45:13 am »

Hasta ahora hemos analizado lo que hay de fondo en las demostraciones formales que hacen los matemáticos, pero los matemáticos no sólo demuestran, sino que también definen. La teoría de conjuntos que usan habitualmente los matemáticos (al igual que le sucede a la teoría T que hemos expuesto en el mensaje anterior) no tiene más conceptos primitivos que los de "conjunto" y "pertenencia". Sin embargo, los matemáticos tratan con un rico abanicos de conceptos. ¿De dónde salen? ¿Cómo se interpreta formalmente la introducción de un nuevo concepto?

Por poner un caso muy simple, si trabajamos en la teoría T un matemático podría empezar diciendo:

Cita
Definición Diremos que un conjunto [texx]x[/texx] es un subconjunto de otro conjunto [texx]y[/texx] (y lo representaremos por [texx]x\subset y[/texx]) si todo elemento de [texx]x[/texx] es también un elemento de [texx]y[/texx].

¿Cómo se formaliza esto, que no es un teorema?

Hay esencialmente dos formas distintas de concebir una definición. Una es considerar que estamos añadiendo un nuevo signo al lenguaje formal de la teoría, en este caso un relator diádico [texx]x\subset y[/texx], y el nuevo relator se acompaña de un nuevo axioma que regula su uso:

[texx]\forall xy(x\subset y\leftrightarrow \forall u(u\in x\rightarrow u\in y))[/texx]

Según esta concepción, las definiciones son axiomas. Ahora bien, está claro que no pueden considerarse axiomas "normales", en el sentido de que no es lo mismo añadir como axioma la definición de inclusión que añadir como axioma la hipótesis del continuo. Las definiciones, así entendidas, son lo que los lógicos llaman "axiomas inesenciales", lo cual viene a decir que no añaden información a la teoría, y con precisión significa que todo modelo de la teoría puede dotarse de una nueva relación que hace verdadero al nuevo axioma. De este modo, los axiomas inesenciales no restringen las interpretaciones posibles de la teoría (al contrario que los axiomas esenciales, como la hipótesis del continuo: si un modelo no la cumple, no se puede hacer nada para que la cumpla, y es un modelo que se descarta al añadir el axioma adicional).

Sin embargo, hay una forma conceptualmente mucho más simple de concebir una definición, y es considerar que es una mera abreviatura. Vista así, la definición se reduce a

[texx]x\subset y\equiv \forall u(u\in x\rightarrow u\in y),[/texx]

donde ahora hay que entender que el término de la izquierda es otro nombre para la misma fórmula que nombra el término de la derecha. Deshaciendo todos los convenios de notación que venimos adoptando, la fórmula en cuestión es la sucesión de signos

[texx]\forall x\rightarrow \in ux\in uy[/texx]

Incluso podríamos considerar que esto no es más que una sucesión de números naturales. Puestos a referirnos a esta sucesión de signos o números con el nombre más cómodo de [texx] \forall u(u\in x\rightarrow u\in y)[/texx], nada nos impide usar un nombre más cómodo y llamarla [texx]x\subset y[/texx]. Así, aquí no hemos de ver una fórmula con tres signos, sino una fórmula con nueve signos, el primero de los cuales no es la variable [texx]x[/texx] sino el cuantificador universal.

Con esta forma de concebir las demostraciones el lenguaje de la teoría formal es siempre el mismo, y lo único que cambia es nuestra forma de referirnos a sus fórmulas. Así, en un razonamiento teórico sobre fórmulas arbitrarias no tenemos que preocuparnos para nada por los signos añadidos, ya que en realidad no hemos añadido ninguno. Podemos asegurar sin comprobación alguna que toda fórmula de la teoría (por muchas definiciones sucesivas que acumule) puede escribirse en términos de los signos primitivos de la teoría porque en realidad es una sucesión de signos primitivos del lenguaje de la teoría, porque nunca hemos añadido ninguno más.

Por el contrario, cuando se conciben las definiciones como axiomas que introducen un nuevo signo a la teoría, es necesario demostrar teoremas que justifiquen la inesencialidad en términos formales y no semánticos, estableciendo concretamente que toda fórmula que incluya signos "definidos" es equivalente a otra que no los contiene, pues para razonar con fórmulas "en abstracto" no podemos tener en cuenta todos los signos que podrían haberse introducido en la teoría mediante las definiciones oportunas. Con la segunda concepción todo esto es inmediato.

Sin embargo, hay dos clases muy distintas de definiciones, y todo lo que hemos dicho sólo vale para una de ellas. Imaginemos que un matemático sigue razonando en la teoría T y dice lo siguiente:

Cita
El axioma del par dice que, dados dos conjuntos [texx]x[/texx] e [texx]y[/texx], existe otro conjunto [texx]z[/texx] cuyos elementos son exactamente [texx]x[/texx] e [texx]y[/texx]. Dicho conjunto es único por el axioma de extensionalidad. En efecto, si hubiera dos conjuntos [texx]z[/texx] y [texx]z'[/texx] cuyos elementos fueran precisamente [texx]x[/texx] e [texx]y[/texx], ambos tendrían los mismos elementos, y lo que dice el axioma de extensionalidad es que dos conjuntos con los mismos elementos son iguales. A este único conjunto [texx]z[/texx] cuyos elementos son [texx]x[/texx] e [texx]y[/texx] lo llamaremos par desordenado de [texx]x[/texx] e [texx]y[/texx] y lo representaremos por [texx]\{x,y\}[/texx].

¿Cómo se ha de entender esto? Cuando escribimos [texx]x\in \{x,y\}[/texx], ¿qué hay que entender que es [texx]\{x,y\}[/texx]?

Al igual que antes, tenemos la opción de considerar que la definición consiste en añadir un nuevo signo al lenguaje formal, en este caso un funtor diádico, que podríamos representar en principio por [texx]P[/texx], junto con el axioma

[texx]\forall xy(\forall u(u\in Pxy\leftrightarrow u=x\lor u=y)),[/texx]

y además convenir en escribir [texx]\{x,y\}\equiv Pxy[/texx].

Con este convenio, la respuesta a la pregunta que habíamos planteado es que [texx]\{x,y\}[/texx] es un término del lenguaje formal de la teoría extendido con un nuevo funtor [texx]P[/texx], concretamente el término que consta del nuevo funtor seguido de las dos variables [texx]x, y[/texx].

De nuevo, esto exige justificar qué condiciones deben darse para que un axioma de este tipo sea inesencial, lo que formalmente supone demostrar que toda fórmula escrita con el nuevo signo [texx]\{x,y\}[/texx] es equivalente a otra que no lo contiene.

Si intentamos concebir una definición de este tipo como una abreviatura, nos encontramos con un problema: el lenguaje [texx]\mathcal L_{\rm tc}[/texx] no tiene más términos que las variables, y [texx]\{x,y\}[/texx] debería ser un término, pero no una variable. Entonces, ¿qué término es?

Una solución en esta línea consiste en considerar que en realidad no definimos [texx]\{x,y\}[/texx], sino más bien la fórmula

[texx]z=\{x,y\}\equiv \forall u(u\in z\leftrightarrow u\in y).[/texx]

Aquí se entiende que la parte izquierda es sólo una forma abreviada de escribir la fórmula de la derecha, que es una fórmula de [texx]\mathcal L_{\rm tc}[/texx], sin ningún signo añadido.

Toda fórmula en la que aparezca [texx]\{x,y\}[/texx] debe entenderse como una abreviatura de otra fórmula en la que [texx]\{x,y\}[/texx] aparece en la forma [texx]z=\{x,y\}[/texx]. Por ejemplo,
[texx]x\in \{x,y\}\equiv \exists z(z=\{x,y\}\land x\in z)[/texx].

Concretando algunos detalles, ésta es una forma viable de concebir las definiciones de términos sin implicar la adición de nuevos funtores o constantes al lenguaje de la teoría. Sin embargo, hay una tercera opción más "concreta" que vamos a discutir seguidamente:



Lenguajes con descriptor

Una forma de tratar las definiciones de términos de forma clara y sistemática es añadir un nuevo signo lógico a los lenguajes formales, llamado el descriptor "[texx]|[/texx]".

Ello nos obliga a modificar las definiciones que hemos dado en los mensajes anteriores para cubrir también este signo adicional.

En primer lugar, las definiciones de término y fórmula deben unirse a una definición conjunta de "expresión", pues igual que los relatores nos pasan de términos a fórmulas, el descriptor nos pasa de fórmulas a términos. En efecto, la definición de expresión queda ahora como sigue:

Toda variable [texx]x[/texx] es un término.

Toda constante [texx]c[/texx] es un término.

Si [texx]f[/texx] es un funtor [texx]n[/texx]-ádico y [texx]t_1,\ldots, t_n[/texx] son términos, entonces [texx]ft_1\cdots t_n[/texx] es una término.

Si [texx]R[/texx] es un relator [texx]n[/texx]-ádico y [texx]t_1,\ldots, t_n[/texx] son términos, entonces [texx]Rt_1\cdots t_n[/texx] es una fórmula.

Si [texx]\alpha[/texx] es una fórmula [texx]\lnot\alpha[/texx] es una fórmula.

Si [texx]\alpha[/texx] y [texx]\beta[/texx] son fórmulas, entonces [texx]\alpha\rightarrow \beta[/texx] es una fórmula.

Si [texx]\alpha[/texx] es una fórmula y [texx]x[/texx] es una variable, entonces [texx]\forall x\alpha[/texx] es una fórmula.

Si  [texx]\alpha[/texx] es una fórmula y [texx]x[/texx] es una variable, entonces [texx]|x\alpha\equiv (x|\alpha)[/texx] es un término.

Como siempre, el orden "real de los signos" es [texx]|x\alpha[/texx], con el nuevo signo delante, para marcar inequívocamente el tipo de expresión, pero en la práctica escribiremos [texx]x|\alpha[/texx], añadiendo paréntesis si es necesario. Los términos de la forma [texx]x|\alpha[/texx] se llaman descripciones.

Con ayuda del descriptor, la definición de par desordenado es:

[texx]\{x,y\}\equiv z|\forall u(u\in z\leftrightarrow u=x\lor u=y).[/texx]

Esto se lee: "[texx]\{x, y\}[/texx] es el conjunto [texx]z[/texx] tal que sus elementos son exactamente [texx]x[/texx] e [texx]y[/texx]".

Para poder manipular formalmente las descripciones necesitamos incorporar a [texx]_{\mathcal L}[/texx] un axioma que diga qué podemos decir de ellas. Es el axioma K7:

[texx]\exists !x\alpha\rightarrow S_x^{x|\alpha}\alpha[/texx]

Naturalmente, esto supone extender la definición de la sustitución para incluir el caso de las descripciones. La definición sigue exactamente el mismo criterio seguido para definir la sustitución en una fórmula de tipo [texx]\forall x\alpha[/texx]. Dejando de lado esos detalles, lo que dice el axioma K7, (que también puede presentarse en forma de regla derivada de inferencia (DP descripciones propias):

[texx]\exists !x\alpha\vdash S_x^{x|\alpha}\alpha[/texx])

es que si existe un único [texx]x[/texx] que cumple la descripción, entonces el [texx]x|\alpha[/texx] cumple la descripción (y por lo tanto es ese único objeto que la cumple).

En nuestro caso: como hemos demostrado que [texx]\exists! z(\forall u(u\in z\leftrightarrow u=x\lor u)y))[/texx], la regla de las descripciones propias nos permite sustituir [texx]z[/texx] por [texx]z|\forall u(u\in z\leftrightarrow u=x\lor u=y)[/texx] es decir, por [texx]\{x,y\}[/texx] en la definición, y nos queda

[texx]\forall u(u\in \{x,y\}\leftrightarrow u=x\lor u=y)[/texx],

es decir, el par [texx]\{x,y\}[/texx] cumple la propiedad que lo define.

Antes de presentar con más detalle el uso del descriptor, vamos a ver más ejemplos de su funcionamiento. Todos ellos siguen el mismo esquema:



Razonamos en la teoría T: el axioma del conjunto vacío afirma que [texx]\exists x\forall u\ u\notin x[/texx]. Este [texx]x[/texx] es único, porque si hubiera dos conjuntos sin elementos, ambos tendrían los mismos elementos (ninguno) y el axioma de extensionalidad afirma que dos conjuntos con los mismos elementos son iguales.

Por lo tanto, en T se demuestra: [texx]\exists ! x\forall u\ u\notin x[/texx].

Esta unicidad nos permite aplicar la regla de las descripciones propias. Si definimos

[texx]\emptyset\equiv x|\forall u\ u\notin x[/texx],

la regla DP nos permite pasar de la existencia con unicidad a la sustitución de la descripción [texx]\emptyset[/texx] en la fórmula que lo define, es decir: [texx]\forall u\ u\notin \emptyset[/texx], y a partir de ahí ya podemos usar el conjunto vacío sabiendo que cumple lo que dice su definición.

Similarmente, el axioma de la unión dice que, para todo conjunto [texx]x[/texx], existe un conjunto [texx]y[/texx] cuyos elementos son los elementos de los elementos de [texx]x[/texx], y dicho [texx]y[/texx] tiene que ser único por el axioma de extensionalidad. Por lo tanto, tenemos:

[texx]\forall x\exists !y\forall u(u\in y\leftrightarrow \exists v(u\in v\land v\in x))[/texx]

Si definimos

[texx]\bigcup x\equiv y|\forall u(u\in y\leftrightarrow \exists v(u\in v\land v\in x))[/texx]

La unicidad nos permite aplicar la regla DP para concluir que podemos sustituir [texx]\bigcup x[/texx] en la fórmula que la define, es decir:

[texx]\forall u(u\in \bigcup x\leftrightarrow \exists v(u\in v\land v\in x))[/texx]

Notemos que la regla DP sigue el "espíritu" de [texx]K_{\mathcal L}[/texx], es decir, es una regla que el matemático puede usar "instintivamente", sin siquiera ser consciente del paso lógico concreto que está dando. En la práctica, un matemático razona simplemente así:

Cita
El axioma de la diferencia afirma que, para todo par de conjuntos [texx]x[/texx] e [texx]y[/texx] existe un conjunto [texx]z[/texx] cuyos elementos son los elementos de [texx]x[/texx] que no pertenecen a [texx]y[/texx]. Claramente, dicho [texx]z[/texx] es único por el axioma de extensionalidad, luego podemos llamarmo [texx]x\setminus y[/texx]

Por debajo de esto hay dos cosas:

1) Que cuando el matemático dice ``podemos llamar [texx]x\setminus y[/texx] al conjunto cuyos elementos son los elementos de [texx]x[/texx] que no están en [texx]y[/texx]" eso se formaliza como

[texx]x\setminus y\equiv z|\forall u(u\in z\leftrightarrow u\in x\land u\notin y)[/texx]

2) Que el matemático tiene conciencia de que no puede dar nombre a algo salvo que haya demostrado que la definición lo caracteriza, es decir, que existe un único [texx]z[/texx] que cumple la definición. Esto se formaliza como que es la condición necesaria para que sea aplicable la regla DP, que nos permite afirmar que

[texx]\forall xyu(u\in x\setminus y\leftrightarrow u\in x\land u\notin y).[/texx]

Los ejemplos que hemos visto son los usos típicos del descriptor y, en realidad, todo uso del descriptor es un uso típico como los que acabamos de ver. Vemos así que la finalidad del descriptor no es ni más ni menos que (junto con la regla DP) formalizar de forma el concepto de definición matemática sin necesidad de recurrir a añadir signos al lenguaje formal.



Como comentábamos, la incorporación del descriptor a los lenguajes formales requiere retocar todas las definiciones para tenerlo en consideración. El cambio más drástico es el que ya hemos indicado: que ya no es posible definir los conceptos de término y fórmula por separado, sino que es necesario definirlos simultáneamente porque se puede construir fórmulas a partir de términos y términos a partir de fórmulas.

En segundo lugar, las definiciones de variable libre y ligada se han de extender para tener en cuenta que en un término como [texx]z|\forall u(u\in z\leftrightarrow u\in x\land u\notin y)[/texx] la variable [texx]z[/texx] está ligada por el descriptor, igual que la variable [texx]u[/texx] está ligada por el cuantificador, mientras que las variables [texx]x, y[/texx] están libres. La idea es que el descriptor liga variables exactamente igual que lo hacen los cuantificadores.

Por último, hay que definir el concepto de sustitución de una variable por un término en una expresión (término o fórmula) considerando a la vez los dos casos, pues ahora están relacionados, y sólo hay que añadir la definición de sustitución [texx]S_x^t y|\alpha[/texx], que se define exactamente igual que [texx]S_x^t\forall y\alpha[/texx], sin más que cambiar [texx]\forall y[/texx] por [texx]y|[/texx].

Remito para los detalles a mi libro de lógica (capítulo I).

Desde el punto de vista semántico, hay que definir qué es el objeto denotado en un modelo [texx]M[/texx] por una descripción [texx]x|\alpha[/texx] respecto de una valoración [texx]v[/texx].

Para ello necesitamos hacerle un pequeño añadido a la definición de modelo. En un modelo [texx]M[/texx] de un lenguaje con descriptor debe fijarse (además de una interpretación para cada constante, relator y funtor del lenguaje) un objeto [texx]d[/texx] de su universo al que llamaremos "descripción impropia" en el modelo [texx]M[/texx] y que será el objeto asignado a cada descripción impropia, en el sentido siguiente:

[texx]M(x|\alpha)[v][/texx] se define como el único objeto [texx]a[/texx] que cumple [texx]M\vDash \alpha[v_x^a][/texx], si es que existe tal único [texx]a[/texx], o bien [texx]M(x|\alpha)[v]\equiv d[/texx]  en caso contrario (tanto si no existe ningún [texx]a[/texx] como si existen varios).

De este modo el objeto denotado por [texx]x|\alpha[/texx] es lo que cabe esperar que sea (el único objeto que cumple [texx]\alpha[/texx]) cuando existe tal objeto, pero sucede que el término [texx]x|\alpha[/texx] está ahí, es un término que requiere interpretación, aunque no se dé la unicidad, y en tal caso le asignamos un significado convencional, el objeto al que llamamos [texx]d[/texx], y que podemos elegirlo en cada modelo.

Por ejemplo, un matemático nunca diría "definimos [texx]A[/texx] como el conjunto que tiene entre sus elementos al conjunto vacío", porque sabe que eso no define un conjunto (no hay un único conjunto que cumpla eso), pero nada nos impide considerar el término [texx]A\equiv x|\emptyset\in x[/texx].

Aunque un matemático nunca definiría esta [texx]A[/texx], no hay ningún problema en definirla a condición de que tengamos claro que no podemos aplicar la regla DP y, por consiguiente, no podemos afirmar que [texx]\emptyset \in A[/texx] (y, por consiguiente, no podemos decir nada de [texx]A[/texx] a partir de su "definición", podemos dar la definición, pero no usarla, y ahí se ataja formalmente el sinsentido).

Pero como [texx]A[/texx] es un término (si no "bien definido" en el sentido que los matemáticos usan la definición, sí al menos correctamente definido), tiene que tener una interpretación en todo modelo, y hemos convenido que se interpreta como un objeto [texx]d[/texx] fijado arbitrariamente en el modelo de antemano, y que no tiene nada que ver con la definición. Si da la casualidad de que dicho objeto contiene al conjunto vacío, entonces [texx]A[/texx] denotará un objeto que casualmente cumplirá la definición de [texx]A[/texx], pero no tiene por qué ser así.

Con la definición que hemos dado de "objeto denotado por una descripción" se comprueba inmediatamente que el axioma K7 es verdadero en todo modelo, por lo que [texx]K_{\mathcal L}[/texx] sigue siendo correcto.

En cambio, con dicha definición ha dejado de ser semánticamente completo. Hay sentencias verdaderas en todo modelo de T que no son demostrables a partir de los axiomas de T. Por ejemplo:

[texx](x|\emptyset\in x)=(x|\emptyset\notin x)[/texx]

Esta sentencia es verdadera en todo modelo de T, porque ambos miembros son descripciones impropias: ni hay un único conjunto que contenga al conjunto vacío, ni hay un único conjunto que no contenga al conjunto vacío. Por ejemplo, [texx]\{\emptyset\}, \{\emptyset, \{\emptyset\}\}[/texx] son dos conjuntos que cumplen lo primero y [texx]\emptyset, \{\{\emptyset\}\}[/texx] son dos conjuntos que cumplen lo segundo. Esto hace que en cualquier modelo de T ambos términos denoten la descripción impropia [texx]d[/texx] y, por consiguiente, la sentencia resulta verdadera. Pero no tenemos ninguna regla de inferencia que nos permita tratar con descripciones impropias para que podamos demostrar esa igualdad.

La completitud semántica de [texx]K_{\mathcal L}[/texx] se recupera añadiendo un octavo y último axioma que recoja el convenio que hemos adoptado con las descripciones impropias:

[texx]\lnot\exists !x\alpha\rightarrow (x|\alpha)=(x|x=x)[/texx]

Notemos que [texx]x|x=x[/texx] siempre denota en un modelo a la descripción impropia (porque sólo es una descripción propia si en el modelo hay un único objeto que es idéntico a sí mismo, lo cual sólo puede suceder si el modelo tiene un único objeto, y entonces dicho objeto tiene que ser [texx]d[/texx] necesariamente, porque no hay otra posibilidad para [texx]d[/texx]). Por lo tanto, lo que afirma K8 es que cuando no hay un único objeto que cumple [texx]\alpha[/texx], la descripción [texx]x|\alpha[/texx] (es decir, cualquier descripción impropia) es igual a una descripción impropia concreta (luego todas las descripciones impropias son iguales entre sí, todas denotan al mismo objeto en un modelo).

Este axioma K8 no se usa para nada en la práctica, pues explica cómo tratar el caso que nunca plantea un matemático, pues un matemático nunca usa descripciones impropias. Sin embargo, es todo lo que hace falta para demostrar igualdades "tontas" como la anterior que, queramos o no, tienen que poder demostrarse para que podamos decir que nuestro cálculo deductivo es semánticamente completo. En efecto, con este último axioma, la demostración del teorema de completitud sigue siendo válida aunque el lenguaje tenga descriptor.

Pese a todo, es posible dar al axioma K8 una utilidad práctica que un matemático considerará, si no especialmente útil, al menos razonable. Podemos añadir un axioma a T que diga:

[texx](x|x=x)=\emptyset[/texx]

Esto significa "la descripción impropia es el conjunto vacío". Dicho así puede que lo le diga mucho a un matemático, pero se puede explicar en términos más simples: "Cualquier cosa que esté mal definida se entenderá por convenio que es igual al conjunto vacío". Eso sí lo entiende el matemático y, aunque no le preocupe mucho, porque no tiene por costumbre definir cosas mal, sí puede serle útil a veces, para no tener que precisar qué sucede en los casos que no le interesan.

Por ejemplo, si la Aritmética de Peano adoptamos como axioma [texx](x|x=x)=0[/texx], entonces podemos definir

[texx]x-y\equiv z|(x=y+z)[/texx],

y con esta definición puede demostrarse que [texx]0''''-0'''=0'[/texx], mientras que [texx]0''-0''''[/texx] es una descripción impropia, porque puede probarse que no existe ningún número [texx]z[/texx] tal que [texx]0''''+z=0''[/texx], pero entonces, por K8 y el axioma específico sobre las descripciones impropias, podemos afirmar que [texx]0''-0''''=(x|x=x)=0[/texx]. Así estamos conviniendo en que todas las restas que no se pueden calcular valen cero.

Similarmente, volviendo a la teoría de conjuntos, podemos convenir que las integrales de las funciones no integrables son el conjunto vacío, que los límites de las sucesiones que no tienen límite son el conjunto vacío, etc. No es imprescindible, pero no queda mal. Evita que podamos escribir cosas que no tengan interpretación.

Lo dicho es suficiente para manejar descripciones en la práctica (y manejarlas inconscientemente, como hace el matemático), así que nos limitaremos a citar un último resultado: si en una teoría podemos caracterizar la descripción impropia sin usar descriptores (por ejemplo, como el único [texx]x[/texx] que cumple [texx]\forall u\ u\notin x[/texx] en T, o como [texx]x=0[/texx] en AP), entonces toda fórmula con descriptores es equivalente en dicha teoría a otra sin descriptores. Por lo tanto, al estudiar la teoría a nivel teórico siempre podemos decir "consideramos únicamente fórmulas sin descriptores", y con ello (si lo que vamos a decir sobre fórmulas se conserva por equivalencia lógica) no perdemos generalidad. Por ello, una vez demostrado este teorema, el considerar descriptores no es un lastre con el que estemos obligados a cargar para siempre, sino que en cualquier momento podemos desprendernos de él a efectos teóricos, y usar los descriptores únicamente a efectos prácticos, para formalizar definiciones de forma económica y precisa.

En línea
Carlos Ivorra
Administrador
Pleno*
*****

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 9.081


Ver Perfil WWW
« Respuesta #19 : 10/04/2013, 18:11:20 pm »

Para terminar esta exposición de la lógica que subyace al razonamiento matemático quiero destacar algo que ya ha quedado implícito en el mensaje anterior. Imaginemos que le pedimos a un matemático que nos demuestre que [texx]\forall xy(x\subset y\land y\subset x\rightarrow x=y)[/texx]. Podemos comparar varias posibilidades:

Respuesta típica del matemático Por el axioma de extensionalidad.

Respuesta típica del matemático al que hemos mirado con cara de pocos amigos por haber acabado tan rápido Si tomas un [texx]u[/texx] que esté en [texx]x[/texx], tienes que estará en [texx]y[/texx] por definición de inclusión [texx]x\subset y[/texx], e igualmente al revés, luego tienes que [texx]x[/texx] e [texx]y[/texx] tienen los mismos elementos, luego son iguales por el axioma de extensionalidad.

Demostración formal:



Un matemático tiende a dar por evidentes ciertos pasos que, detallados al máximo, requieren varios razonamientos menores, pero si realmente sabe lo que está diciendo, es capaz de detallar más cualquier fragmento de su argumentación (como si pusiéramos una lupa sobre él). Es posible que si alguien con serios problemas para entender razonamientos lógicos presiona mucho al matemático preguntándole "¿y eso cómo  lo sabes?", "¿y eso por qué?", "no entiendo ese paso," etc., el matemático no sea capaz de llegar a detallar su argumento hasta el nivel de detalle que supone el razonamiento formal que hemos presentado, porque el matemático no necesita conocer [texx]K_{\mathcal L}[/texx], ni qué es EC o IB. Sin embargo, lo verdaderamente importante es que si a un matemático desesperado porque no logra hacer ver a alguien que su argumento está justificado le enseñamos el razonamiento formal que hemos presentado y nos aseguramos de que lo entienda, no dirá "bueno... sí... es otra forma de verlo", sino que dirá, "¡exacto!, eso es lo que estaba tratando de explicar sin saber ya cómo".

Lo que quiero decir es que el razonamiento formal no es otra forma de razonar, distinta de la habitual del matemático, aunque éste la reconozca como válida, sino que es exactamente la forma de razonar del matemático, sólo que detallada al máximo. El matemático abrevia todos aquellos pasos que pueden darse "por pura lógica", sin necesidad de recurrir a alguna idea matemática propiamente dicha (y en niveles más avanzados incluso abrevia los pasos que un experto en la teoría tratada puede rellenar por su experiencia), pero esos pasos lógicos que abrevia son su lógica subyacente, independientemente de que pueda no estar familiarizado con la forma de expresarla formalmente (con un cálculo deductivo formal en concreto).

Si alguien ha estudiado lógica y se ha quedado con la idea de que lo que le han enseñado tiene cierta relación con el razonamiento matemático, pero es otra cosa, que se puede razonar algo "por lógica" o "como hacen los matemáticos", como si fueran dos cosas distintas, es que no ha entendido lo que le han enseñado o (muy probablemente) no se lo han enseñado bien.

La lógica que hemos expuesto aquí es la que subyace a todo razonamiento matemático "usual" exactamente en el mismo sentido en que el código máquina subyace a toda aplicación informática ejecutable en un ordenador. Un programador familiarizado con el lenguaje C puede no saber nada de código máquina, pero lo que al final está programando es una secuencia de instrucciones en código máquina, aunque el software de programación que utilice le permita explicitar sólo instrucciones de alto nivel que luego se pueden concretar mecánicamente (de eso se encarga su compilador). La diferencia es que, aunque todos los razonamientos de alto nivel de un matemático (si son correctos) se pueden desarrollar al lenguaje de bajo nivel de [texx]K_{\mathcal L}[/texx], nadie se molesta en hacerlo porque no hace falta para nada.

De este modo, sin perjuicio de que la lógica sea un campo de estudio muy vasto, con mil direcciones para explorar, puede decirse que quien entienda todo lo expuesto aquí entiende todo lo que hay debajo del trabajo de un matemático "normal". Naturalmente, es posible dar cálculos deductivos distintos pero equivalentes al que hemos dado, es posible desarrollar la teoría de otro modo, etc., pero salvo variantes insustanciales, lo que sirve de fundamento al razonamiento matemático es que disponemos de un cálculo deductivo correcto y semánticamente completo que funciona como hemos visto que funciona. Razonar correctamente en matemáticas es razonar de forma que todos los pasos puedan desarrollarse hasta adquirir el aspecto del razonamiento formal precedente. Hacerlo en la práctica sería insufrible, porque los árboles no dejarían ver el bosque de los razonamientos: tanto paso insustancial impediría captar las ideas centrales de las demostraciones, sin contar con la prueba más elemental se haría eterna, pero, desde un punto de vista teórico, lo que hace un matemático es aplicar dando cien pasos en uno las técnicas de razonamiento que aquí hemos descrito, ni más ni menos.

Confío en que este artículo pueda servir a sus lectores para ver con más claridad tanto lo que es la concepción moderna de las matemáticas como lo que es la lógica formal que sirve de sustento a las matemáticas. La conexión concreta entre ambas se realiza a través de la teoría de conjuntos. No hemos entrado aquí en detalles sobre cómo es una teoría de conjuntos, pero para entender en qué consiste eso de usar una teoría de conjuntos basta haber entendido cómo se usa la teoría T, pues la diferencia entre T y ZFC es simplemente que en ZFC se pueden demostrar más cosas, pero siempre de la misma manera.

* cic16.jpg (40.96 KB - descargado 851 veces.)
En línea
Páginas: [1]   Ir Arriba
  Imprimir  
 
Ir a:  

Impulsado por MySQL Impulsado por PHP Powered by SMF 1.1.4 | SMF © 2006, Simple Machines LLC XHTML 1.0 válido! CSS válido!