On Logics and Semantics for Interpretability

Abstract

[eng] In the central part of this thesis we study for different interpretability logics the following aspects: completeness for modal semantics, decidability and algorithmic complexity. In particular, we will study two basic types of relational semantics for interpretability logics. One is the Veltman semantics, which we shall refer to as the regular or ordinary semantics; the other is called generalised Veltman semantics. In the recent years and especially during the writing of this thesis, generalised Veltman semantics was shown to be particularly well-suited as a relational semantics for interpretability logics. In particular, modal completeness results are easier to obtain in some cases; and decidability can be proven via filtration in all known cases. We prove various new and reprove some old completeness results with respect to the generalised semantics. We use the method of filtration to obtain the finite model property for various logics. Apart from results concerning semantics in its own right, we also apply methods from semantics to determine decidability (implied by the finite model property) and complexity of provability (and consistency) problems for certain interpretability logics. From the arithmetical standpoint, we explore three different series of interpretability principles. For two of them, for which arithmetical and modal soundness was already known, we give a new proof of arithmetical soundness. The third series results from our modal considerations. We prove it arithmetically sound and also characterise frame conditions w.r.t. ordinary Veltman semantics. We also prove results concerning the new series and generalised Veltman semantics.

[cat] El tema d’aquesta tesis són les lògiques d’interpretabilitat les quals descriuen el comportament del predicat d’interpretabilitat. Per tal de discutir la interpretabilitat entre teories matemàtiques, permeteu que primer diguem unes paraules sobre interpretacions. Hi ha diferents nocions d’una interpretació en ús, però una cosa que tenen en comú és que totes involucren una traducció que preserva l’estructura; aquesta traducció transforma formules de la teoria interpretada a formules de la teoria interpretadora. Aquest mapa cal que preservi la demostrabilitat fins a un cert punt, i.e. si A és un teorema de la teoria interpretada, llavors la imatge de A ha de ser demostrable en la teoria interpretadora. Que aquest mapa preservi l’estructura significa que almenys commuta amb les connectives lògiques. Les fórmules quantificades poden ser modificades lleugerament quan són interpretades; específicament hom pot fitar el domini de (totes) les fórmules quantificades fent servir un predicat fixat anomenat domini especificador (i.e. estem interessats en interpretabilitat relativitzada). Això ens permet construir una interpretació de, per exemple, una teoria de nombres en una teoria de conjunts, on (per la construcció habitual) només alguns conjunts es fan servir per representar nombres. Podem requerir els axiomes de la teoria interpretada de ser demostrables en la teoria interpretadora, però també podem requerir que això també es compleixi per tots els teoremes de la teoria interpretada (aquesta diferència és rellevant només quan hom treballa en una metateoria dèbil). Les lògiques d’interpretabilitat descriuen el comportament d’un tipus específic d’interpretabilitat. Per començar, limitem el nostre interès en teories de primer ordre. En segon lloc, només ens concentrem en interpretabilitat entre extensions finites d’una teoria fixada T. En tercer lloc, estem interessats en interpretabilitat formalitzada, i.e, no estudiem el problema de si T + A interpreta T + B, sinó el problema de si T pot demostrar que T + A interpreta T + B. En quart lloc, no estem interessats per quines A i B tenim que T + A interpreta T + B, sinó que estem interessats en aquelles propietats que són estructurals en el sentit que es compleixen per qualsevol tria de A i B. Optem per teoremes d’interpretabilitat en aquesta tesi; i.e. per tal que T + A interpreti T + B hem requerit que la traducció de qualsevol teorema de T + B sigui demostrable en T + A. La teoria T hauria de ser suficientment forta; i.e. seqüencial. Si tal teoria és axiomatitzable, té un predicat IntT(·, ·), definit d’una manera natural, expressant el fet que el primer argument del predicat interpreta el segon argument. La lògica d’interpretabilitat de T és definida d’una manera molt semblant a la lògica de demostrabilitat de T, però amb un operador binari: _; la interpretació corresponent d’aquest operador és IntT. Així, la lògica d’interpretabilitat d’una teoria T és el conjunt de totes les fórmules lògiques modals en el llenguatge de lògiques d’interpretabilitat que són demostrables per qualsevol lectura aritmètica que es doni a les variables proposicionals i prenent els operadors modals a les seves aritmetitzacions corresponents. A diferència del que pot ser el cas en lògiques de demostrabilitat, la lògica d’interpretabilitat de T realment depèn de T. Per exemple, la lògica d’interpretabilitat de la teoria de conjunts de Gödel-Bernays (que és la lògica denominada ILP), i la lògica d’interpretabilitat de l’Aritmètica de Peano (que és la lògica denominada ILM), difereixen. Donada una teoria seqüencial T, hi ha una certa quantitat de contingut, normalment denominat IL(All), que la lògica d’interpretabilitat de T inevitablement ha de tenir. Els continguts exactes de IL(All) no són coneguts; de fet, millorar la fita inferior és la pregunta que motiva la major part de les investigació en aquest camp. Una simple fita és la lògica d’interpretabilitat bàsica, denominada IL. Aquesta és una extensió de la lògica de demostrabilitat i conté cinc esquemes d’axioma addicionals que en la literatura són coneguts com J1-J5. Tornant a la qüestió de IL(All), hi ha una manera interessant i sorprenent de millorar les millors fites inferiors conegudes, i.e. de trobar nous principis d’interpretabilitat aritmèticament vàlids. L’enfocament és estudiar semàntiques relacionals modals (semblant a Kripke). Nous principis aritmèticament vàlids han sorgit prenent les condicions de marc de principis ja coneguts, modificant-les, i llavors obtenint la fórmula modal que caracteritza la condició de marc modificada. Això, efectivament, no garanteix la validesa aritmètica de la fórmula modal obtinguda de tal forma, però noves fórmules aritmèticament vàlides s’han descobert talment. Un altre enfocament relacionat és intentar establir completesa d’una certa extensió de IL. Si la demostració de completesa modal falla per a alguna extensió concreta, estendre l’extensió més enllà, fins que sigui modalment completa, pot produir noves fórmules aritmèticament vàlides (aquest intent serà seguit en el capítol final de la tesi). Hi ha dos tipus de semàntiques modals per lògiques d’interpretabilitat. Una és coneguda com semàntica regular Veltman (o semàntica ordinària Veltman, o només Veltman semantics quan no hi ha risc d’ambigüitat). L’altra és coneguda com semàntica generalitzada Veltman, introduïda per Verbrugge, que combina una semàntica en l’estil de Kripke amb una semàntica de veïnat. La semàntica regular Veltman pot ser usada per demostrar completesa per moltes lògiques d’interpretabilitat. Tanmateix, per lògiques més complexes, la semàntica generalitzada Veltman es poden emprar per donar demostracions de completesa més simples i fàcils d’entendre. En els darrers anys i especialment durant la redacció d’aquesta tesi, la semàntica generalitzada Veltman ha sigut provada de ser particularment ben adequada com a semàntica relacional per lògiques d’interpretabilitat. En particular, resultats sobre completesa modal són més fàcils d’obtenir en alguns casos; i decidibilitat pot ser demostrada via filtració en tots els casos coneguts. Demostrem diversos nous i redemostrem alguns resultats coneguts respecte la semàntica generalitzada.En alguns casos, només sabem que una lògica és completa respecte la semàntica generalitzada Veltman. També hi ha exemples de lògiques completes respecte semàntica generalitzada Veltman però incompletes respecte semàntica regular Veltman. Tots els resultats de complexitat (la majoria dels quals són establerts en aquesta tesi) estan basats en semàntica regular Veltman. Pel que fa a decidibilitat, sembla que la semàntica generalitzada Veltman és una eina més apropiada, ja que permet un mètode uniforme per obtenir la propietat de model finit. En aquesta tesi estudiarem diverses propietats d’interpretabilitat relativitzada formalitzada. En la part central d’aquesta tesi estudiem per diferents lògiques d’interpretabilitat els següents aspectes: completesa per semàntiques modal, decidibilitat i complexitat algorísmica. A banda de resultats al voltant de les semàntiques en el seu si, també apliquem mètodes de semàntiques per determinar la complexitat de problemes de demostrabilitat (i de consistència) per certes lògiques d’interpretabilitat. Des del punt de vista aritmètic, explorem tres sèries diferents de principis d’interpretabilitat. Per dos d’ells, pels quals la solidesa aritmètica i modal ja era coneguda, donem una nova demostració de solidesa aritmètica. La tercera sèrie resulta de les nostres consideracions modals. Demostrem que és sòlida aritmèticament i que també caracteritza condicions de marc respecte semàntica regular Veltman. A més, donem una demostració de completesa per certes lògiques relacionades amb la tercera sèrie (les lògiques ILWR i ILW!). Permeteu que descrivim l’estructura de la tesi. En el Capítol 1 donem una introducció informal del tema general de la tesi. En el Capítol 2 donem una introducció més formal, definicions bàsiques i presentem alguns resultats senzills. En els dos capítols subseqüents explorem completesa modal. Primer introduïm l’eina clau: etiquetes asseguradores. Aquí presentem la teoria general d’etiquetes asseguradores, incloent la noció d’etiquetes asseguradores Γ-completes. Desenvolupem la teoria usada posteriorment en la tesi, però també demostrem resultats interessants per si sols (com la caracterització de Γ-completesa). En el Capítol 4 fem servir etiquetes asseguradores per tal d’obtenir diversos resultats de completes respecte la semàntica generalitzada Veltman. Definim ILX-estructures per X _{M, P,M0, P0, R} i X _ {W,W_} i demostrem que la les lògiques ILX corresponents són completes respecte la seva classe de marcs característica. En particular obtenim que ILP0 i ILR són completes, els quals són resultats nous. També definim el problema d’iteració d’etiqueta i introduïm un tipus especial d’estructures, ILWP-estructures, que poden ser usades per solucionar aquest problema en el cas simple de la lògica ILP. La motivació d’això és que el problema d’iteració d’etiqueta reapareix en lògiques més complexes com ILWR, on la solució encara és desconeguda. Sospitem que la mateixa solució pot ser aplicable fins i tot en lògiques més complexes, però hi ha altres problemes que encara no s’han solucionat en aquest cas. Tornem al tema de completesa en el capítol final de la tesi on entre altres resultats donem una demostració condicional de la completesa de ILWR. En el Capítol 5 apliquem resultats de completesa i obtenim resultats de decidibilitat. Aquest és una aplicació, i potser la més útil, de la semàntica generalitzada: l’habilitat de definir filtracions amb bon comportament. El Capítol 6 tracta la complexitat; demostrem que IL, ILW i ILP són PSPACE-completes. En el Capítol 7 treballem amb l’aspecte aritmètic de les lògiques d’interpretabilitat. Concretament, donem una nova demostració de solidesa per dues sèries de principis recentment descobertes. En el capítol final, Capítol 8, introduïm una altra sèrie de principis, demostrem que és aritmèticament sòlida i la hi donem semàntica ordinària Veltman. Com ja hem mencionat abans, també donem demostracions condicionals de completesa per lògiques relacionades amb aquesta sèrie nova.