Lògica de segon ordre

Una lògica de segon ordre és una extensió d'una lògica matemàtica de primer ordre en la qual s'afegeixen variables per propietats i quantificadors que operen sobre aquestes variables. Així s'expandeix el poder expressiu del llenguatge sense haver d'afegir nous símbols lògics.

Molts sistemes matemàtics no poden ser unívocament caracteritzats per un llenguatge formal de primer ordre, com ara l'aritmètica de Peano o la teoria dels grups lliures de torsió. En aquests casos els llengüatges de primer ordre formalitzen una part d'aquestes teories però hi ha propietats matemàtiques d'aquestes teories que no poden ser expressades amb el sistema de una lògica de primer ordre.

Introducció

La necessitat de les lògiques de segon ordre es reflexen en l'axioma d'inducció de l'aritmètica tal como Giuseppe Peano la va formalitzar:

Per qualsevol conjunt X de nombres enters, si $0\in X$ i a més $n \in X \Rightarrow n+1\in X$, llavors es té que $X = \mathbb{N}''$

La expresió "Per qualsevol conjunt" requereix un llengüatge on els quantificadors puguin afectar a les variables, per exemple si el predicat $a\in X$ es representa mitjançant el símbol $\tilde{X}(a)$ l'axioma d'inducció es pot representar en símbols com a:

$\forall \tilde{X}\ (( \tilde{X}(0) \land \forall x(\tilde{X}(x)\to \tilde{X}(x+1)) \to \forall y \tilde{X}(y))$

A més, una lògica de segon ordre també pot quantificar sobre propietats. Gràcies a això pot expressar, per exemple, que tot individu o té una propietat o no la té:

$\forall P\,\forall x\, (Px\or\neg Px)$

O el principi d'identitat dels indiscernibles:

$\forall P\,\forall x\,\forall y\,\Big ((Px\Leftrightarrow Py)\to (x = y)\Big)$

No obstant això, el que es guanya en poder expressiu es perd en metateoria. Hi ha propietats metateòrica generalment considerades desitjables que les lògiques de segon ordre no tenen i les lògiques de primer ordre sí tenen. Per exemple, les lògiques de segon ordre (amb semàntiques estàndard) són incompletes. Vol dir que no hi pot haver cap sistema deductiu finit a partir del qual es puguin demostrar totes les veritats lògiques expressables en el llenguatge. Això és: el conjunt de les veritats del sistema és més gran que el conjunt de les veritats demostrables en el sistema. Això es deu al fet que les lògiques de segon ordre tenen el poder expressiu suficient per ser afectades pels teoremes d'incompletesa de Gödel. De fet va ser el propi Gödel qui va demostrar que en un llenguatge de segon ordre el conjunto de veritats no és recursivament enumerable, i per tant, no hi ha cap procediment per descobrir si una proposició és vàlida en cada model possible d'aquest llenguatge de segon ordre.

Conseqüències

La lògica de segon ordre té una expressivitat més gran de la de primer ordre, això permet axiomatitzar sistemes matemàtiques més complexos. És a dir, i ha proposicions no formalitzables exactament utilitzant el formalisme de la lògica de primer ordre però si poden ser formalitzats amb lògica de segon odre. Això constitueix un avantatge. Tanmateix l'ús de lògiques de segon ordre ocassiona algunes dificultats:

• El teorema de compacitat, que afirma que un conjunt de proposicions lògiques d'una lògica de primer ordre es satisfactible si i només si qualsevol conjunto finit d'aquestes es satisfactible, no és vàlid per una lògica de segon ordre.
• El teorema de Löwenheim-Skolem que afirma que una lògica de primer ordre amb una quantitat finita de signes diferents admet un model numerable no es vàlid per una lògica de segon ordre.

El fet que aquests dos teoremes molt útils de la lògica de primer ordre no es puguin generalitzar a segon ordre, no admetin generalització a segon ordre dificulten certes applicaicons matemàtiques de la lògica de segon ordre. Per aquesta raó s'han buscat altres generalitzacions més útils de la lògica de primer ordre.

Tipus d'extensions de segons ordre

Existeixen diversos tipus de lògiques de segon ordre. Això significa que hi ha varies maneres d'extendre una lògica de primer ordre per formar una lògica de segon ordre. Aquestes maneres d'extendre la lògica de primer ordre difereixen en el tipus de variables addiocionals que introdueixen. Entre les lògiques de segon ordre més estudiades es poden trobar:

• La lògica de segon ordre monàdica (LSOM), en la que s'afegeixen només variables per subconjunts dintre d'un cert domini.
• La lògica de segon ordre completa (LSOC), en la que s'introduexien tots els tipus possibles de variables i els quantificadors poden lligar a qualsevol tipus de variables.

Una lògica de segon ordre inclou quantificadors de diferents tipus ($\exists_1, \forall_1, \exists_2, \forall_2$), a més de quatinficadors de primer ordre que requereixen variables com les de la lògica de primer ordre, existeixen quantificadors per a subconjunts i propietats, que no poden aparéixer en una lògica de primer ordre. Igualment es pot construir un llenguatge de segon ordre específic. La lògica de segon ordre conté fòrmules de primer ordre i fòrmules de segon ordre. Una fòrmula de lògica de segon ordre s'animena fòrmula de primer ordre (i es considera un element del conjunt $\Sigma^1_0$ o del conjunt $\Pi^1_0$) si tots els quantificadors quantifiquen només variables de primer ordre (podent contenir altres variables de segon ordre lliures). Una fòrmula de segon ordre existencial és una fòrmula del conjunt $\Sigma^1_1$ que conté a més alguns quantificadors existencials sobre variables de segon ordre, és a dir, $\exists_2 R_0\ldots\exists_2 R_m \phi$, on $\phi$ designa una fòrmula de primer ordre. El conjunt de fòrmules existencials de segon ordre que conté només existencials $\exists_2$ es designa pero $\Sigma^1_1$ o fins i tot ∃SO. Les fòrmules de $\Pi^1_1$ es defineixen dualment, són el conjunt de fòrmules de segon ordre que contenen només quantificadors $\forall_2$. Poden formar-se conjunts més complicats definits recursivament per qualsevol k > 0, com $\Sigma^1_{k+1}$ format per fòrmules de la forma $\exists R_0\ldots\exists R_m \phi$, on $\phi$ és una fòrmula del tipus $\Pi^1_k$.

Bibliografia

• Hilbert, David; and Ackermann, Wilhelm (1950); Principles of Mathematical Logic, Chelsea (English translation of Grundzüge der theoretischen Logik, 1928 German first edition)
• Ebbinghaus, Heinz-Dieter; Flum, Jörg; and Thomas, Wolfgang (1994); Mathematical Logic, Undergraduate Texts in Mathematics, Berlin, DE/New York, NY: Springer-Verlag, Second Edition, ISBN 978-0-387-94258-2