¿Cuál es la definición formal de una variable?

Question

¿Qué es una variable?

Sé que un ( $n$ -ary) puede pensarse como una función de $\{ 0,1 \}^n$ a $\{ 0,1 \}$ .

Y un cuantificador sobre $M$ puede considerarse como un conjunto de subconjuntos de $M$ .

¿Cuál es la forma correspondiente de pensar en una variable que va sobre $M$ ?

Answer 1

Una variable es un portador de algo, es decir, representa algo. Normalmente definimos una variable como perteneciente a un conjunto, por ejemplo $x\in\mathbb{R}$ significa que cuando vemos la variable $x$ representa algún valor de los números reales. La mayoría de las cosas que involucran variables implican lógica de primer orden --es sólo que normalmente no pensamos en ello de esa manera.

Como ejemplo resuelve cada una de las dos ecuaciones siguientes (para x, un número real): $x^2 = -1$ y $x^2 = 1$ . Cuando te pedimos que resuelvas una ecuación, lo primero que debes hacer es comprobar si hay o no es una solución es una fórmula de primer orden: $\exists x \in \mathbb{R} : x^2 = -1$ que se lee: "existe un valor del conjunto de los números reales, que llamamos $x$ , tal que el cuadrado de este valor, $x$ es negativo". Si esta expresión es verdadera, entonces podemos ser capaces de encontrar el valor o los valores de los números reales que hacen que esto sea cierto (teóricamente siempre podemos encontrar el valor, si existe, pero éste, o éstos, pueden ser muy difíciles de encontrar).

Así que para la primera ecuación, hay no existe un valor real tal que su cuadrado es negativo uno y por lo tanto esta ecuación no tiene soluciones. Sin embargo, para la segunda ecuación, existe son valores reales cuyo cuadrado da positivo y podemos encontrar esos valores. Decimos que $x = 1$ o $x = -1$ . Lo que realmente estamos diciendo es que $1$ y $-1$ son los dos números reales existentes cuyo valor al cuadrado da positivo (los dos valores reales que hacen la expresión booleana $x^2 = 1$ verdadero). El $x$ es sólo una forma conveniente de poner un "marcador de posición" mientras no conocemos los valores particulares que pretendemos para $x$ para representar.

edit: Definición más rigurosa de una variable

Esencialmente, una variable es un símbolo, que puede ser cualquier cosa --incluyendo símbolos para conjuntos, funciones, operadores, etc. A Firma define el conjunto de símbolos de un lenguaje, $s_\text{func}$ y $s_\text{rel}$ y algunas propiedades de esos símbolos. El conjunto $s_\text{func}$ se compone de símbolos que representan funciones (que incluyen variables y constantes como $x$ y $1$ respectivamente). El conjunto $s_\text{rel}$ define operadores relacionales como $=$ , $\leq$ , $\geq$ etc. La última pieza de la firma es un conjunto de funciones, $ar$ cada uno de los cuales asigna una aridad a un símbolo concreto. Una aridad de $n$ significa que este símbolo requiere $n$ (así que algo como $+$ definiendo la adición, tendría arrity $2$ ya que requiere dos entradas, por ejemplo $a + b$ ).

Como ejemplo, puedo tener $S: \langle \{2, 3, 5,x, +, - \}, \{=\}, ar\rangle$ . Cada una de las constantes tiene aridad $0$ (que se define en $ar$ ) lo que significa que su interpretación será una solo de un dominio. La variable $x$ es en realidad una función de aridad $1$ ¡! Requiere al menos un valor de entrada a interpretar. Incluso si $x$ representa un valor vectorial, sigue necesitando sólo una única entrada que es un solo valor del conjunto de dominios $\mathbb{D}^n$ (donde $n$ sería la aridad del vector). Los dos símbolos $+$ y $-$ tienen aridad $2$ --que requieren dos entradas cada una y, de nuevo, esas entradas podría sean valores vectoriales. Finalmente $=$ (un símbolo relacional) también es de arrity $2$ -- requiere dos valores para hacer una comparación.

El interpretación de los símbolos define lo que realmente significan. Así, por ejemplo, la interpretación de $x$ sería una función que mapea $\{2, 3, 5\} \mapsto \{2, 3, 5\}$ de tal manera que cada elemento se mapea a sí mismo (es decir $x(2) = 2$ , $x(3) = 3$ y $x(5) = 5$ ). Las constantes sólo representan valores particulares del conjunto de $\mathbb{I}$ . Los símbolos más y menos definen funciones que asignan $\mathbb{I}\times\mathbb{I} \mapsto \mathbb{I}$ y así sucesivamente. Así que puedo usar esta firma de arriba para resolver una ecuación:

$$ x + 3 = 5 \\ x = 5 - 3 = 2 \\ x = 2 $$

Todos los símbolos que utilicé para resolver esa ecuación están definidos por la firma anterior y un interpretación (que expliqué parcialmente, aunque ciertamente no de manera formal).

Answer 2

Puedes ver Gramática categorial y, en detalle: Sara Negri y Jan von Plato, Teoría de la prueba estructural (2001), Apéndice A.2 : GRAMÁTICA CATEGORIAL PARA LENGUAJES LÓGICOS [página 221].

En lógica proposicional En cuanto a las proposiciones atómicas, no se les da ninguna estructura, sino que se introducen como puros parámetros $P, Q, R$ ..., con las categorizaciones

$P : Prop, Q : Prop, R : Prop$ , ...

Conectivos son funciones para formar nuevas proposiciones a partir de otras dadas. Tenemos la función constante $\bot$ , llamado falsedad para lo que simplemente escribimos $\bot : Prop$ .

A continuación tenemos negación , con la categorización :

$Not: (Prop)Prop$ .

Y así sucesivamente...

Podemos poner lógica de predicados en [este] marco [...] si asumimos para simplificar que tratamos con un solo dominio $\mathcal D$ . Los objetos, individuales constantes se denotan por $a, b, c$ ,.... En lugar de las constantes proposicionales $P, Q, R$ ..., las proposiciones atómicas pueden ser valores de funciones proposicionales sobre $\mathcal D$ , por lo que se clasifica como $P : (\mathcal D)Prop, Q : (\mathcal D)(\mathcal D)Prop$ y así sucesivamente. A continuación tenemos a los individuos variables $x, y, z$ . . . . tomando valores en $\mathcal D$ . Siguiendo la costumbre habitual permitimos variables libres en las proposiciones. Las proposiciones con variables libres se entienden como proposiciones bajo supuestos, por ejemplo, si $A : (\mathcal D)Prop$ entonces $A(x) : Prop$ bajo el supuesto $x : \mathcal D$ . Términos $t,u,v$ ... son parámetros individuales o variables. El lenguaje de la lógica de predicados se obtiene añadiendo a la lógica proposicional el cuantificadores Cada uno y Algunos, con las categorizaciones

$Every : ((\mathcal D)Prop)Prop$

$Some : ((\mathcal D)Prop)Prop$ .

Son relativas a un dominio determinado $\mathcal D$ . Así, para cada dominio $\mathcal D$ un cuantificador sobre ese dominio es una función que toma como argumento una función proposicional de un lugar función $A : (\mathcal D)Prop$ y da como valor una proposición, aquí o $Every(A)$ o $Some(A)$ .