# Metalògica

La metalògica és la metateoria de la lògica Mentre que la lògica estudia com els sistemes lògics es poden utilitzar per construir arguments vàlids i sòlids, la metalògica estudia les propietats dels sistemes lògics. La lògica es refereix a les veritats que es poden derivar mitjançant un sistema lògic, i la metalògica es refereix a les veritats que es poden derivar sobre els llenguatges i sistemes que s'utilitzen per expressar veritats.
Els objectes bàsics de l'estudi metalògic són els llenguatges formals, els sistemes formals i les seves interpretacions. L'estudi de la interpretació de sistemes formals és la branca de la lògica matemàtica que es coneix com a teoria de models, i l'estudi dels sistemes deductius és la branca que es coneix com a teoria de la demostració.

## Visió general
### Llenguatge formal

Un llenguatge formal és un conjunt organitzat de símbols, que el defineixen precisament en forma i lloc. Per tant, aquesta mena de llengua es pot definir sense fer referència als significats de les seves expressions; pot existir abans que se li assigni cap interpretació, és a dir, abans que tingui cap significat. La lògica de primer ordre s'expressa sempre en algun llenguatge formal. Una gramàtica formal determina quins símbols i conjunts de símbols són fórmules en un llenguatge formal.
Un llenguatge formal es pot definir formalment com un conjunt A de cadenes (seqüències finites) en un alfabet fix α. Alguns autors, entre ells Rudolf Carnap, defineixen la llengua com la parella ordenada <α, A >. Carnap també requereix que cada element de α hagi de aparèixer en almenys una cadena de A.

### Normes de formació

Les regles o normes de formació (també anomenades gramàtica formal) són una descripció precisa de les fórmules ben formades d'un llenguatge formal. Són sinònimes del conjunt de cadenes sobre l'alfabet del llenguatge formal que constitueixen fórmules ben formades. Tanmateix, no descriu la seva semàntica (és a dir, què volen dir).

### Sistemes formals

Un sistema formal (també anomenat càlcul lògic, o sistema lògic) consisteix en un llenguatge formal juntament amb un aparell deductiu (també anomenat sistema deductiu). L'aparell deductiu pot consistir en un conjunt de regles de transformació (també anomenades regles d'inferència) o en un conjunt d'axiomes, o tenir tots dos. Un sistema formal s'utilitza per derivar una expressió a partir d'una o més expressions.
Un sistema formal es pot definir formalment com un triplet ordenat <α, ${\mathcal {I}}$, ${\mathcal {D}}$ d>, on ${\mathcal {D}}$d és la relació de derivabilitat directa. Aquesta relació s'entén en un sentit global de manera que les oracions primitives del sistema formal es prenen com a derivables directament del conjunt buit d'oracions. La derivabilitat directa és una relació entre una frase i un conjunt finit, possiblement buit, d'oracions. Els axiomes es trien de manera que cada membre en primer lloc de ${\mathcal {D}}$d és membre de ${\mathcal {I}}$ i cada membre en segon lloc és un subconjunt finit de ${\mathcal {I}}$ .
Un sistema formal també es pot definir només amb la relació ${\mathcal {D}}$d. Així es pot ometre ${\mathcal {I}}$ i α en les definicions de llenguatge formal interpretat i sistema formal interpretat. Tanmateix, aquest mètode pot ser més difícil d'entendre i utilitzar.

### Demostracions formals

Una demostració o prova formal és una seqüència de fórmules ben formades d'un llenguatge formal, l'última de les quals és un teorema d'un sistema formal. El teorema és una conseqüència sintàctica de totes les fórmules ben formades que el precedeixen en el sistema de demostració. Perquè una fórmula ben formada es pugui qualificar com a part d'una demostració, ha de resultar d'aplicar una regla de l'aparell deductiu d'algun sistema formal a les fórmules ben formades anteriors de la seqüència de demostració.

### Interpretacions

Una interpretació d'un sistema formal és l'assignació de significats als símbols i valors de veritat a les frases del sistema formal. L'estudi de les interpretacions s'anomena semàntica formal. Donar una interpretació és sinònim de construir un model.

## Distincions importants
### Metallenguatge–llenguatge objecte

En metalògica, els llenguatges formals de vegades s'anomenen llenguatges d'objectes. El llenguatge utilitzat per fer enunciats sobre un llenguatge objecte s'anomena metallenguatge. Aquesta distinció és una diferència clau entre la lògica i la metalògica. Mentre que la lògica tracta de demostracions en un sistema formal, expressades en algun llenguatge formal, la metalògica tracta de demostracions sobre un sistema formal que s'expressen en un metallenguatge sobre algun llenguatge objecte.

### Sintaxi-semàntica

En metalògica, la noció de sintaxi té a veure amb els llenguatges formals o els sistemes formals sense tenir en compte cap interpretació d'ells, mentre que la noció de semàntica té a veure amb les interpretacions de llenguatges formals. El terme "sintàctic" té un abast una mica més ampli que "teòrica de demostracions", ja que es pot aplicar a propietats de llenguatges formals sense cap sistema deductiu, així com a sistemes formals. "Semàntica" és sinònim de "teòrica del model".

### Ús-menció

En metalògica, les paraules "ús" i "menció", tant en la seva forma nominal com verbal, adquireixen un sentit tècnic per identificar una distinció important. La distinció ús-menció (de vegades anomenada distinció paraules com a paraules) és la distinció entre utilitzar una paraula (o frase) i ger-ne esment. Normalment s'indica que s'esmenta una expressió en lloc d'utilitzar-la posant-la entre cometes, imprimint-la en cursiva o posant l'expressió per si mateixa en una línia. El tancament entre cometes d'una expressió ens dóna el nom d'una expressió, per exemple:
    'Metalògica' és el nom d'aquest article.
    Aquest article tracta sobre metalògica.

### Tipus-testimoni

La distinció tipus-testimoni separa en metalògica un concepte abstracte dels objectes que són instàncies particulars del concepte. Per exemple, la bicicleta concreta del teu garatge és un testimoni del tipus de cosa que es coneix com "La bicicleta". Mentre que, la bicicleta del vostre garatge es troba en un lloc determinat en un moment determinat, això no és cert per a "la bicicleta" tal com s'utilitza a la frase: "La bicicleta s'ha fet més popular recentment." Aquesta distinció s'utilitza per aclarir el significat dels símbols dels llenguatges formals.

## Història

S'han formulat preguntes metalògiques des de l'època d'Aristòtil. Tanmateix, va ser només amb l'auge dels llenguatges formals a finals del segle XIX i principis del XX que les investigacions sobre els fonaments de la lògica van començar a desenvolupar-se. L'any 1904, David Hilbert va observar que en investigar els fonaments de les matemàtiques es pressuposen nocions lògiques i, per tant, es requeria una explicació simultània dels principis metalògics i metamatemàtics. Avui dia, la metalògica i la metamatemàtica són en gran part sinònimes, i ambdues han estat substancialment subsumides per la lògica matemàtica a l'àmbit acadèmic. Un possible model alternatiu, menys matemàtic, es pot trobar en els escrits de Charles Sanders Peirce i altres semiòtics.

## Resultats

Els resultats en metalògica consisteixen en coses com ara demostracions formals que proven la coherència, la integritat i la decidibilitat de sistemes formals particulars.
Els principals resultats en metalògica inclouen:
* Prova de la incomptable del conjunt de potències dels nombres naturals ( teorema de Cantor 1891)
* Teorema de Löwenheim–Skolem (Leopold Löwenheim 1915 i Thoralf Skolem 1919)
* Prova de la consistència de la lògica proposicional veritat-funcional ( Emil Post 1920)
* Prova de la completesa semàntica de la lògica proposicional veritat-funcional ( Paul Bernays 1918), (Emil Post 1920)
* Prova de la completesa sintàctica de la lògica proposicional veritat-funcional (Emil Post 1920)
* Prova de la decidibilitat de la lògica proposicional veritat-funcional (Emil Post 1920)
* Prova de la consistència de la lògica dels predicats monàdics de primer ordre ( Leopold Löwenheim 1915)
* Prova de la completesa semàntica de la lògica dels predicats monàdics de primer ordre (Leopold Löwenheim 1915)
* Prova de la decidibilitat de la lògica dels predicats monàdics de primer ordre (Leopold Löwenheim 1915)
* Prova de la consistència de la lògica dels predicats de primer ordre ( David Hilbert i Wilhelm Ackermann, 1928)
* Prova de la integritat semàntica de la lògica de predicats de primer ordre (teorema de completesa de Gödel 1930)
* Prova del teorema d'eliminació de talls per al càlcul seqüent ( Hauptsatz de Gentzen 1934)
* Prova de la indecidibilitat de la lògica dels predicats de primer ordre ( teorema de Church 1936)
* Primer teorema d'incompletezza de Gödel 1931
* Segon teorema d'incompletezza de Gödel 1931
* Teorema d'indefinibilitat de Tarski (Gödel i Tarski a la dècada de 1930)

## Vegeu també

* Programació metalògica

## Referències

* 1 2 3 4 Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1973
* 1 2 Rudolf Carnap (1958) Introduction to Symbolic Logic and its Applications, p. 102.
* ↑ Hunter, Geoffrey, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, 1973
* ↑ , <https://plato.stanford.edu/archives/win2022/entries/aristotle-logic/>. Consulta: 28 agost 2023
* ↑ Hao Wang, Reflections on Kurt Gödel