Logique, Forçage, Modèles à valeurs booléennes, Compacité, Forcing itéré, Préservation des sous-Ensembles stationnaires

Les principaux résultats de cette thèse sont liés au forcing, mais notre présentation bénéficie de sa mise en relation avec un autre domaine de la logique: la théorie des modèles des logiques infinitaires. Une idée clé de notre travail, qui était plus ou moins implicite dans les recherches de nombreux auteurs, est que le forcing joue un rôle en logique infinitaire similaire à celui joué par le théorème de compacité en logique du premier ordre. Plus précisément, de la même manière que le théorème de compacité est l'outil clé pour produire des modèles de théories du premier ordre, le forcing peut être l'outil clé pour produire les modèles des théories infinitaires. La première partie de cette thèse explore la relation entre les logiques infinitaires et les modèles à valeurs booléennes. Une propriété de consistance est une famille d'ensembles de formules non contradictoires, fermée sous certaines opérations logiques naturelles. Les propriétés de consistance reproduisent dans le contexte des logiques infinitaires la technique donnée par la méthode de résolution pour produire des modèles d'une formule du premier ordre; elles sont l'outil standard pour produire des modèles de formules infinitaires non contradictoires. Le premier résultat majeur que nous établissons dans cette thèse est le Théorème d'Existence des Modèles Booléens, affirmant que toute formule dans un ensemble qui est dans une propriété de consistance possède un modèle à valeurs booléennes avec la propriété de "mixing", et renforce le résultat original de Mansfield. Le Théorème d'Existence des Modèles Booléens nous permet de prouver trois résultats supplémentaires dans la théorie des modèles des logiques infinitaires munis de la sémantique des modèles à valeurs booléennes avec la propriété de ``mixing": un théorème de complétude par rapport à un calcul de type Gentzen, un théorème d'interpolation et un théorème d'omission des types. Cependant, nous croyons que le résultat central de cette partie de la thèse est le Théorème de Compacité Conservative. Dans la poursuite d'une généralisation de la compacité du premier ordre pour les logiques infinitaires, nous introduisons le concept de "renforcement conservatif" et de "conservativité finie". Nous soutenons que la généralisation appropriée de la consistance finie (relative à la sémantique de Tarski pour la logique du premier ordre) est la conservativité finie (relative à la sémantique donnée par les modèles à valeurs booléennes). À notre avis, ces résultats nous permettent de soutenir que: Les modèles à valeurs booléennes avec la propriété de "mixing" fournissent une sémantique naturelle pour les logiques infinies. Dans la seconde partie de la thèse, nous nous appuyons sur les résultats de la première partie pour aborder la question suivante: pour quelle famille de formules infinitaires peut-on forcer l'existence d'un modèle de Tarski sans détruire les sous-ensembles stationnaires? Kasum et Velickovic ont introduit une caractérisation des formules pour lesquelles un modèle de Tarski peut être forcé par un forcing préservant les ensembles stationnaires (AS-goodness). Leur travail s'appuie sur le résultat révolutionnaire d'Asperò et Schindler. Nous définissons la propriété ASK - une variante de l'AS-goodness - que nous utilisons également de la même manière que Kasum et Velickovic. Il est démontré que pour toute formule ayant la propriété ASK, on peut forcer l'existence d'un modèle de Tarski d'une manière qui préserve les ensembles stationnaires. La preuve de ce résultat s'appuie sur la perspective de la théorie des modèles de forcing présentée dans la première partie de la thèse, tout en introduisant une nouvelle notion de forcing itéré. Cette présentation du forcing itéré est étroitement liée au Théorème de Compacité Conservateur, soulignant à nouveau l'analogie entre les paires (forcing, logiques infinitaires) et (compacité, logique du premier ordre).