Fórmula lóxica

En lóxica matemática, lóxica proposicional e lóxica de predicados, unha **fórmula ben formada** (abreviada en inglés **wff**, moitas veces simplemente **fórmula lóxica**, é unha secuencia finita de símbolos dun alfabeto dado que forma parte dunha linguaxe formal.

Unha linguaxe formal pódese identificar co conxunto de fórmulas da linguaxe. Unha fórmula é un obxecto sintáctico ao que se lle pode dar un significado semántico por medio dunha interpretación. Dous usos clave das fórmulas lóxicas son a lóxica proposicional e a lóxica de predicados.

## Introdución 
Un uso clave das fórmulas é a lóxica proposicional e a lóxica de predicados como lóxica de primeira orde. Neses contextos, unha fórmula é unha cadea de símbolos φ para os que ten sentido preguntar "é verdadeira &#x3C6; ?", unha vez que se crea unha instancia de calquera variable libre en φ. Na lóxica formal, as demostracións pódense representar mediante secuencias de fórmulas con certas propiedades, e a fórmula final da secuencia é a que se demostra.

## Cálculo proposicional 
As fórmulas do cálculo proposicional, tamén chamadas fórmulas proposicionais, son expresións como por exemplo (A \land (B \lor C)). A súa definición comeza coa elección arbitraria dun conxunto *V* de variábeis proposicionais. O alfabeto consta das letras en *V* xunto cos símbolos dos conectivos proposicionais e dos parénteses "(" e ")", todos eles se supón que non están en *V.* As fórmulas serán determinadas expresións (é dicir, cadeas de símbolos) sobre este alfabeto.

As fórmulas defínense indutivamente do seguinte xeito:

* Cada variábel proposicional é, por si mesma, unha fórmula.
* Se φ é unha fórmula, entón &#xAC; φ é unha fórmula.
* Se φ e ψ son fórmulas, e • é calquera conectivo binario, entón ( φ • ψ) é unha fórmula. Aquí • poderían estar (mais non limitarse a) os operadores habituais ∨, ∧, → ou ↔.

Usando esta gramática, a secuencia de símbolos

: ((( *p* &#x2192; *q* ) &#x2227; ( *r* &#x2192; *s* )) &#x2228; ( &#xAC; *q* &#x2227; &#xAC; *s* ))

é unha fórmula, porque é gramaticalmente correcta. A secuencia de símbolos

: (( *p* &#x2192; *q* ) &#x2192; ( *qq* )) *p* ))

non é unha fórmula, porque non se axusta á gramática (fáltalle unha conectiva entre dúas letras do alfabeto e outra conectiva para a última letra).

Unha fórmula complexa pode ser difícil de ler, debido, por exemplo, á proliferación de parénteses. Para paliar este último fenómeno, asúmense regras de precedencia (similares á orde matemática estándar das operacións) entre os operadores, facendo que uns operadores sexan máis vinculantes que outros. Por exemplo, asumindo a precedencia (de máis vinculante a menos vinculante) 1. &#xAC;&nbsp;2. &#x2192;&nbsp;3. &#x2227;&nbsp;4. &#x2228;. Así a fórmula

: ((( *p* &#x2192; *q* ) &#x2227; ( *r* &#x2192; *s* )) &#x2228; ( &#xAC; *q* &#x2227; &#xAC; *s* ))

pode abreviarse como

: *p* &#x2192; *q* &#x2227; *r* &#x2192; *s* &#x2228; &#xAC; *q* &#x2227; &#xAC; *s.*

## Lóxica de predicados 
A definición dunha fórmula na lóxica de primeira orde \mathcal{QS} é relativa á sinatura da teoría en cuestión. Esta sinatura especifica os símbolos constantes, símbolos de predicado e símbolos de función da teoría en cuestión, xunto coas aridades dos símbolos de función e predicado.

A definición dunha fórmula componse de varias partes. En primeiro lugar, o conxunto de **termos** defínese recursivamente. Os termos, informalmente, son expresións que representan obxectos do dominio do discurso.

# Calquera variábel é un termo.
# Calquera símbolo constante da sinatura é un termo
# unha expresión da forma *f*( *t*1 ,..., *t**n*), onde *f* é un símbolo de función *n*-aria, e *t*1 ,... , *t**n* son termos, é de novo un termo.

O seguinte paso é definir as fórmulas atómicas.

# Se *t*1 e *t*2 son termos, *t*1 = *t*2 é unha fórmula atómica
# Se *R* é un símbolo de predicado *n*-ario, e *t*1 ,... , *t**n* son termos, entón *R*( *t*1 ,..., *t**n* ) é unha fórmula atómica

Finalmente, o conxunto de fórmulas defínese como o conxunto máis pequeno que contén o conxunto de fórmulas atómicas de modo que se cumpre o seguinte:

# \neg\phi é unha fórmula cando \phi é unha fórmula
# (\phi \land \psi) e (\phi \lor \psi) son fórmulas cando \phi e \psi son fórmulas;
# \exists x\, \phi é unha fórmula cando x é unha variábel e \phi é unha fórmula;
# \forall x\, \phi é unha fórmula cando x é unha variábel e \phi é unha fórmula (alternativamente, \forall x\, \phi podería definirse como unha abreviatura de \neg\exists x\, \neg\phi ).

Se unha fórmula non ten ocorrencias de \exists x ou \forall x, para calquera variábel x, entón chámase **libre de cuantificadores**. Unha *fórmula existencial* é unha fórmula que comeza cunha secuencia de cuantificación existencial seguida dunha fórmula sen cuantificador.

## Fórmulas atómicas e abertas 
Unha *fórmula atómica* é unha fórmula que non contén conectivos lóxicos nin cuantificadores ou, equivalentemente, unha fórmula que non ten subfórmulas estritas. A forma precisa das fórmulas atómicas depende do sistema formal considerado; para a lóxica proposicional, por exemplo, as fórmulas atómicas son as variábeis proposicionais. Para a lóxica  de predicados, os átomos son símbolos de predicados xunto cos seus argumentos, sendo cada argumento un termo.

## Fórmulas pechadas 
Unha *fórmula pechada*, tamén *fórmula* ou *enunciado* fundamental, é unha fórmula na que non hai ocorrencias libres de ningunha variábel. Se **A** é unha fórmula dunha linguaxe de primeira orde na que as variábeis  teñen ocorrencias libres, entón **A** precedida de  é un *pechamento universal* de **A**.

## Propiedades aplicábeis ás fórmulas 
* Unha fórmula **A** nunha linguaxe \mathcal{Q} é *válida* se é certo para toda interpretación de \mathcal{Q}.
* Unha fórmula **A** nunha lingua \mathcal{Q} é *satisfactoria* se é certo para algunha interpretación  de \mathcal{Q}.
* Unha fórmula **A** da linguaxe na aritmética de Peano é *decidíbel* se representa un conxunto decidible, é dicir, se existe un método efictivo que, dada a substitución das variábeis libres de **A**, di que ou a instancia resultante de **A** é demostrábel ou o é demostrábel a súa negación.
## Notas 
## Véxase tamén 
### Bibliografía 
*
* 

* 
* 
*
*
* 
* 
### Outros artigos 
* Lóxica.
* Lóxica matemátia.
### Ligazóns externas 
*Well-Formed Formula for First Order Predicate Logic - includes a short Java quiz.
*Well-Formed Formula at ProvenMath