Llògica categòrica

Adjunción entre dos funtores explicitada pels seus hom-sets. La adjunción és un dels conceptes fonamentals en llògica categòrica i teoria de categories en general.

La llògica categòrica és una branca de les matemàtiques, particularment de la llògica matemàtica, que investiga als sistemes formals usant conceptes de teoria de categories; particularment, l'us de nocions com categoria cartesiana tancada o talps. També és notable per les seues conexions en l'informàtica teòrica, teoria de tipos, i la teoria de tipos homotópica. En térmens generals, la llògica categòrica representa tant la sintaxis com la semàntica de sistemes formals per mig d'una categoria, i una interpretació per mig d'un funtor. Les conectiva llògiques i els quantificadors poden interpretar-se, d'igual forma, com funtores adjunts sobre una categoria cartesiana tancada. El marc categòric proporciona un ric marc conceptual per a construccions llògiques i de teoria de tipos. El seu estudi va iniciar a finals de 1960 seguint el treball pioner de William Lawvere.

Descripció general

Alguns dels temes principals abordats per mig de l'enfocament categòric són els següents:

Semàntica categòrica

La llògica categòrica introduïx la noció de estructura valuada en una categoria C en la noció modele-teorética clàssica d'una estructura que apareix en el cas particular a on C és la categoria de conjunts i funcions. Esta noció ha demostrat ser útil quan la noció de teoria de conjunts d'un model carix de generalitat i/o resulta inconvenient. La modelació de RAG Seely de vàries teories impredicativas, com el Sistema F, és un eixemple de l'utilitat de la semàntica categòrica.

Segons el treball de William Lawvere sobre hiperdoctrinas, els conectors i quantificadors de la llògica de primer orde es podien representar baix el concepte de functores adjunts. Per eixemple, la adjunción entre el quantificador universal i el quantificador existencial sorgix naturalment baix les regles d'eliminació i introducció d'estos mateixos quantificadors en deducció natural.

Llenguages interns

Açò pot vore's com una formalisació i generalisació de la prova per mig de la busca de diagrames . Es definix un llenguage intern adequat que nomena els constituents rellevants d'una categoria i després s'aplica la semàntica categòrica per a convertir les afirmacions en una llògica sobre el llenguage intern en declaracions categòriques corresponents. Açò ha tingut molt èxit en la teoria de talps, a on el llenguage intern d'un talps junt en la semàntica de la llògica intuicionista d'orde superior en un talps permet raonar sobre els objectes i morfismos d'un talps com si foren conjunts i funcions. Açò ha tingut èxit en tractar en talps que tenen "conjunts" en propietats incompatibles en la llògica clàssica. Un bon eixemple és el model de càlcul lambda no tipificat de Dana Scott en térmens d'objectes que es retrauen en el seu propi espai funcional . Un atre és el model Moggi -Hyland del sistema F per mig d'una subcategoría interna completa del talps efectiu de Martin Hyland .

Construccions de models de térmens

En molts casos, la semàntica categòrica d'una llògica proporciona una base per a establir una correspondència entre teories en la llògica i instàncies d'un tipo apropiat de categoria. Un eixemple clàssic és la correspondència entre les teories de la llògica ecuacional βη sobre el càlcul lambda simplement tipificat i les categories tancades cartesianas, coneguda com correspondència de Curry-Howard-Lambek (que inclou la correspondència entre tipos i proposicions llògiques). Les categories que sorgixen de les teories a través de construccions de models de térmens generalment es poden caracterisar fins a la seua equivalència per mig d'una propietat universal adequada. Açò ha permés realisar proves de propietats metateóricas d'algunes llògiques per mig d'un àlgebra categòrica apropiada. Per eixemple, Freyd va donar una prova de les propietats de disjunció i existència de la llògica intuicionista d'esta manera.

Principals construccions

Conectivas com funtores adjunts

Recorde's que una categoria pot ser entesa com un conjunt parcialment ordenat (a on cada morfismo $A\to B$ pot ser vist com $A\le B$), de tal modo que si una categoria conté tots els llímits i colímites, pot ser interpretada com un retícul. Més específicament, si esta categoria és cartesiana tancada i té un objecte inicial i terminal, la categoria pot ser entesa com un àlgebra de Heyting o un àlgebra de Boole depenent el cas.

Siga l'objecte terminal interpretat com 1 o verdader i l'objecte inicial entés com 0 o fals, i siga $\mathscr{H}$ nostra àlgebra de Heyting (que és una categoria); tindrem llavors els següents funtores i adjunciones:

$\wedge :\mathscr{H}\times \mathscr{H}\to \mathscr{H}$, tal que: $(\varphi ,\psi )\mapsto \varphi \wedge \psi$. I tindrem la adjunción $\Delta ⊣\wedge$, a on $\Delta$ és el funtor diagonal $\Delta :\mathscr{H}\to \mathscr{H}\times \mathscr{H}$ definit per $\Delta (a)=⟨a,a⟩$.

$\vee :\mathscr{H}\times \mathscr{H}\to \mathscr{H}$, tal que: $(\varphi ,\psi )\mapsto \varphi \vee \psi$. I tindrem la adjunción $\vee ⊣\Delta$.

$\Rightarrow :\mathscr{H}\times \mathscr{H}\to \mathscr{H}$, tal que: $(\varphi ,\psi )\mapsto \varphi \Rightarrow \psi$. I tindrem la adjunción $(-\wedge A)⊣(-{)}^A$, sent A qualsevol objecte de la categoria.

$\mathrm{\neg }:\mathscr{H}\to {\mathscr{H}}^{op}$, tal que: $\varphi \mapsto \mathrm{\neg }\varphi ;\varphi \to \psi \mapsto \mathrm{\neg }\psi \to \mathrm{\neg }\varphi$, a on ${\mathscr{H}}^{op}$ és el seu categoria oposta.

Quan treballem en un àlgebra bi-Heyting (és dir, que opera tant en la negació de Heyting i negació de co-Heyting, podem definir els operadors modals $◻,◊$ en abdós negacions, donant-nos una atra situació de funtores adjunts.

Formalment, siga $\mathrm{\neg }$ la negació de Heyting i siga $\sim$ la negació de co-Heyting. Llavors definim: $◊=\sim \mathrm{\neg }$ i $◻=\mathrm{\neg }\sim$, la composició d'abdós com funtores (a on la negació de co-Heyting es definix análogamente a la seua contraparte). Ademés tindrem la següent adjunción $◊⊣◻$.

Hiperdoctrinas i adjunción de quantificadors

Esta exposició seguix el treball original de Lawvere.

Primer definirem una categoria cartesiana tancada $𝐓$ els objectes de la qual seran tipos o contexts, els morfismos s'interpreten com a térmens i el morfismo $1\to C$ de l'objecte terminal a qualsevol un atre objecte una constant de tipo $C$.

Llavors, una hiperdoctrina es definix com un funtor $P:{𝐓}^{op}\to ℂ$ sobre un llenguage $ℒ$ (que pot ser de qualsevol llògica), i a on $ℂ$ és una 2-categoria (o de major orde), tal que els seus objectes tinguen una llògica interna corresponent a $ℒ$. Per eixemple, podem deixar que $ℂ$ siga una categoria de conjunts parcialment ordenats, o de retículs o de àlgebra de Heyting. Per a tota $X\in 𝐓,P(X)$ es dirà la categoria d'atributs o de predicats sobre $X$.

Un atre eixemple canònic és aquell en que la hiperdoctrina envia a cada $X$ al seu retícul, o àlgebra, de subobjetos (que pot entendre's com el clàssic retícul format pels subconjunts d'un conjunt ordenats baix inclusió). En este sentit, també es diu que una hiperdoctrina assigna a cada objecte una categoria similar a una sobrecategoría (un cas especial de la categoria menge), o una axiomatisació de les seues sobrecategorías.

L'acció de la hiperdoctrina, en ser un funtor contravariante, és tal que, a cada morfismo $f:X\to Y$ en $𝐓$, assigna l'operació de substitució de variables per als predicats, o proposicions, de cada context; és dir $P(f):P(Y)\to P(X)$. Ara vorem cóm els quantificadors són adjunts a $P(f)$.

En tant $𝐓$ és cartesiana tancada, existix el producte de cada colecció d'objectes. Pensem en $X\times Y$ i les seues proyeccions respectives ${\pi }_X,{\pi }_Y$. Llavors per contravarianza tindrem $P({\pi }_X):P(X)\to P(X\times Y)$, que pot vore's com agregar una variable $Y$ lliure (o vàries) el context de $X$. En tant el codominio de la hiperdoctrina és una 2-categoria, tindrem que $P({\pi }_X)$ és un funtor, per lo que podem definir dos funtores adjunts que revertixquen lo que fa $P({\pi }_X)$; és dir, que eliminen les variables lliures agregada al context $X$. Com pot vore's, estos correspondran, llavors, a quantificar sobre $Y$.

Definirem dos funtores ${\mathrm{\forall }}_Y:P(X\times Y)\to P(X),{\mathrm{\exists }}_Y:P(X\times Y)\to P(X)$, que tindran la següent adjunción: ${\mathrm{\exists }}_Y⊣P({\pi }_X)⊣{\mathrm{\forall }}_Y$. Açò implica la següent situació (a on $A⊢B$ significa $A\to B$, $\star =P({\pi }_X)$ per brevetat i $\varphi ,\psi$ són elements de la 2-categoria, és dir, predicats):

$\begin{array}{c}\star (\varphi (\overline{x}))⊢\psi (\overline{x},y)\\ \varphi (\overline{x})⊢{\mathrm{\forall }}_y\psi (\overline{x},y)\end{array}\begin{array}{c}{\mathrm{\exists }}_y\psi (\overline{x},y)⊢\varphi (\overline{x})\\ \psi (\overline{x},y)⊢\star (\varphi (\overline{x}))\end{array}$

Aixina, és fàcil vore que la counidad de la adjunción $P({\pi }_X)⊣{\mathrm{\forall }}_Y$ és simplement la regla d'eliminació de $\mathrm{\forall }$ i l'unitat de la adjunción ${\mathrm{\exists }}_Y⊣P({\pi }_X)$ la regla d'introducció de $\mathrm{\exists }$ en deducció natural.

Vore també

• Història de la teoria de talps
• Teoria de categories
• William Lawvere

Bibliografia complementària

• (1990).«Model Theory».Elsevier.
• (1980).«Categoricity».History and Philosophy of Logic.1(1–2)

187–207.doi:10.1080/01445348008837010.

• Hodges, Wilfrid, "First-order Model Theory", The Stanford Encyclopedia of Philosophy (Summer 2005 Edition), Edward N. Zalta (ed.).
• (2002).«Model theory: An introduction».Springer-Verlag.New York, NY:217
• «Mathematical Logic».Springer-Verlag.doi:10.1007/978-1-4684-9452-5.
• (1965).«Categoricity in Power».Transactions of the American Mathematical Society.American Mathematical Society, Vol. 114, No. 2.114(2)

514–538.ISSN 0002-9947.doi:10.2307/1994188.

• (1974).«Proceedings of the Tarski Symposium (Proc. Sympos. Pure Math., Vol. XXV, Univ. of Califòrnia, Berkeley, Calif., 1971)».American Mathematical Society.Providence, R.I.:25

187–203.doi:10.1090/pspum/025/0373874.

• (1990).«Classification theory and the number of nonisomorphic models».Elsevier. (IX, 1.19, pg.49)
• (1904).«A System of Axioms for Geometry».Transactions of the American Mathematical Society.American Mathematical Society, Vol. 5, No. 3.5(3)

343–384.ISSN 0002-9947.doi:10.2307/1986462.