Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

URI permanent per a aquesta col·leccióhttps://diposit.ub.edu/handle/2445/133559

Treballs Finals del Màster de Lògica Pura i Aplicada de la Facultat de Filosofia de la Universitat de Barcelona.

Estadístiques

Examinar

Mostrant 1 - 20 de 28

Structural reflection for large cardinal partition properties
(2025-09) Cobo Rodríguez, Germán; Bagaria, Joan
In the theory of large cardinals, the Structural Reflection research program has the ultimate goal of providing a uniform way of characterizing any large cardinal notion in terms of structural reflection principles. In the present work, we study and provide such a characterization for Erdős, Ramsey, Rowbottom and Jónsson cardinals, which are large cardinal notions commonly defined in terms of partition properties and contained in the region below the first measurable cardinal. We introduce three new families of structural reflection principles: the invariant structural reflection principles, which characterize Erdős and Ramsey cardinals; the two-cardinal structural reflection principles, which characterize Rowbottom cardinals; and the proper structural reflection principles, which characterize Jónsson cardinals. Finally, we show how a particular generalization of a proper structural reflection principle yields a characterization of exacting cardinals.
Possible worlds and the contingency of logic
(2024-09) Mayaux, Paul; Joosten, Joost J.; van der Giessen, Iris
In modal semantics, when speaking of possible worlds, there seems to be the tacit assumption that logical reasoning will stay constant throughout. That is to say that a logical reasoning valid at one world is valid in all worlds, hence necessary. But what happens then if we decide to consider possible worlds semantics where different worlds may respond to different logics? What then becomes necessary? In this thesis, we expand the possible world semantics for modal logics by not assuming one ‘type’ of possible worlds in a model, but by considering that different possible worlds might reason under different logics. We focus ourselves on a setting where we combine classical and intuitionistic worlds. We use ⊢, to denote pure propositional intuitionistic reasoning even if the language contains □. In that sense, formulas of the form □ A behave as propositional variables as far as ⊢, is concerned. Likewise we consider the ⊢ relation for classical reasoning. We define so-called mixed models which are tuples ⟨W, R, {lw}w∈W , {Tw}w∈W ⟩, where lw ∈ {i, c} and Tw a set of modal formulas such that 1. ⊥ ∈/ Tw 2. Tw ⊢lw φ ⇒ φ ∈ Tw 3. □φ ∈ Tw ⇐⇒ ∀v(wRv ⇒ Tv ⊢lv φ) 4. ¬□φ ∈ Tw ⇐⇒ ∃u(wRu ∧ Tu ⊢lu ¬φ) We prove soundness of the intuitionistic normal modal logic iK+ (bem) wrt mixed models, where bem is short for ‘Box Excluded Middle’ and denotes the axiom □A ∨ ¬□A. The logic iK has well-studied birelational semantics with an R relation for the □ and ≤ for intuitionistic implication (Bozic and Dosen 1984). We prove soundness and completeness for iK + (bem) with respect to these birelational semantics together with the birelational model frame condition. w ≤ v ⇒ ∀z(wRz ⇒ vRz). We conclude completeness for iK + (bem) wrt mixed models. These results pave the way for new semantic constructions of Kripke models, raising intriguing mathematical and philosophical questions. It invites us to consider the implementation of more logics, possibly non-comparable, in this construction.
The mountain pass theorem on subsystems of second order arithmetic
(2024-09) Aguilar Enríquez, Miguel Alejandro; Fernández Duque, David
The main goal of this work is to formalize the Mountain Pass Theorem of Ambrosetti and Rabinowitz within the formal subsystem of second order arithmetic known as ACA0. We develop some Analysis within this system to have access to the space of continuous functions from [0, 1] into a separable Banach space and from there built formalized proofs of the basic ingredients of the Mountain Pass Theorem: The deformation lemma and the minimax principle that proves the theorem itself.
Interactive Proofs in Bounded Arithmetics
(2024-08) Soto, Martín; Atserias, Albert
Previous work [3] has shown that V02, the theory of bounded arithmetic in Buss’ Language equipped with comprehension for boundedly definable sets, is consistent with the conjecture NEXP ⊈ P/poly. That work entertains two diferent formalizations of the inclusion NEXP ⊆ P/poly inside V02, termed α and β. Both formalizations are provably equivalent in the standard model of arithmetic, by invoking the Easy Witness Lemma (EWL), a technically deep modern result in complexity theory. While the implication β → α is provable in V02, it is open whether V02 proves the converse implication α → β. Since this converse implication can be interpreted as a formalization of the EWL, whether V02 proves the equivalence of the two formalizations amounts to whether V02 proves (this formalizationof) the EWL. In the present work, we make progress towards resolving this question in the positive. More concretely, we show that V02+α does prove a suitable formalization of IP = PSPACE, which is a central ingredient in the proof of the EWL. In the process of doing so, we lay the foundations necessary to discuss exact counting of large sets and formalization of interactive proofs in V02 and other second-order bounded arithmetics.
Reiterman‘s theorem for pseudovarieties
(2024-09) Liberal Grana, Ion Mikel; Moraschini, Tommaso; Horčík, Rostislav
In this thesis we will restrict our attention only to classes of finite algebras. Besides the inherent motivation in studying finite algebras, they appear and are used in many other fields. For example, finite semigroups and monoids are very useful in the theory of au tomata and rational languages (see [22] and [9]). In particular, the classes considered in this context have some special properties, namely, they are closed under homomorphic images, under subsemigoups and under finite products. This motivates the general definition of a pseudovariety, which is a class of finite algebras closed under homomorphic images, under subalgebras and under finite products.
Multimodal logics for musical grammars
(2024-09) Asensi Arranz, Roger; Fernández Duque, David
Musical theory has often employed multiple grammars to formalize harmonic languages. We reinterpret a particular model in terms of a fusion of temporal and transitive modal logics. This work focuses on the analysis of typical decision problems of the field, while exploring how might the results vary according to the applied restrictions. In order to do so, we recur to well-known techniques and methods from computability theory and the field of modal logic. Some examples from the music-theoretic literature are presented and analyzed through the lenses of the considered results and observations.
On Languages and a Strictly Positive Fragment of Linear Temporal Logic
(2024-09) Acevedo, Lucas Uzías; Joosten, Joost J.
This thesis explores various characterizations of regular and star-free languages and in troduces a novel syntactic fragment of Linear Temporal Logic (LTL), called Strictly Pos itive Linear Temporal Logic (SPLTL), inspired by the Reflection Calculus. The opening chapter provides a comprehensive survey of regular languages, characterized by regular expressions, regular grammars, finite automata, and Monadic Second-Order logic over words. We conclude the exposition with a detailed proof of Büchi’s Theorem, which bridges automata and logic. The discussion then shifts to star-free languages, emphasiz ing their representation using LTL. An exhaustive proof of the Completeness Theorem for LTL is also provided. The principal contribution of this thesis is the definition and analysis of SPLTL, which aims to achieve improved complexity compared to LTL. We establish several foundational results for SPLTL and show its soundness concerning the standard semantic framework of LTL. However, proving the completeness of SPLTL presents difficulties, primarily due to the absence of the disjunction operator in the SPLTL formalization. Despite these challenges, we think that this thesis introduces valuable insights and results that lay the groundwork for future research. It paves the way for a more in-depth investigation into the completeness of SPLTL and its potential applications.
A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic
(2024-09) Cantero de Arriba, Carlos; Atserias, Albert
The aim of this work is to formalize the circuit-size lower bound showed by Kannan in 1982 in a weak theory for feasible computations. In particular, we will work with theories of bounded arithmetic, which are subtheories of Peano Arithmetic that weaken its induction axiom scheme by restricting it to formulas in which the quantifiers are bounded. Kannan’s circuit lower bound states that for every fixed polynomial size of circuits, there is a language in the second level of the polynomial hierarchy that cannot be decided by circuits of that size. We note that the essential ingredient in this proof is a key use of the weak pigeonhole principle, which is available in bounded arithmetic. Instrumental in the proof of Kannan’s Theorem is the celebrated Karp-Lipton’s Theorem, stating that if the satisfiability problem for propositional formulas can be decided by polynomial-size circuits then the polynomial hierarchy collapses to its second level, which we also formalize in the same theory
Lexical Semantics in Modern Type Theory: The challenge of selectional coercion
(2024-08) Kuznetsov, Stepan G; Joosten, Joost J.; Sutton, Peter R.
The goal of this work is to address the challenge of modelling selectional coercions in frame of MTT semantics. We will claim that selectional coercions, but not contextual coercions can be modelled via incorporating notions of lexical records and the Lecial Conceptual Paradigm (LCP) from the Generative Lexicon (Pustejovsky 1996) (further: GL) thus drawing the line between them: Main Questions: What are the possible ways of integrating lexical semantics from the Generative Lexicon for cases of linguistical coercion into Modern Type Theory? To what extent can selectional coercion be modelled in MTT enriched with GL-style lexical structure? In order to address the main questions, we use methods and definitions which are already present in Modern Type Theories: namely, Σ-types (e.g. Luo 2021), coercive subtyping (Luo, Soloviev, and Xue 2013), unit-types (e.g. Luo 2011a, A) and dependent event types (Luo and Soloviev 2017). This introduces a number of challenges. We briefly describe these here and then break the Main Questions down into sub-questions (Q1)- (Q3).
Higher Structural Reflection and Very Large Cardinals
(2024-09) Hou, Nai-Chung; Bagaria, Joan
One line of research in set theory aims at deriving large cardinal axioms from strengthened forms of reflection principles. This research is often motivated by the foundational goal of justifying the large cardinal axioms. The most comprehensive attempt in this direction is the program of structural reflection (SR), initiated by Joan Bagaria, whose ultimate goal is to formulate all large cardinal axioms as instances of a single, general structural reflection principle that is conceptually compelling. The basic version of SR already gives the hierarchy of large cardinals from supercompact cardinals, through C(n)-extendible cardinals, up to Vopěnka’s Principle. A stronger version of SR, the exact structural reflection principle (ESR), is studied by Bagaria and Philipp Lücke, which gives almost huge cardinals, and beyond. However, ESR differs in form from the basic version of SR, rather than being direct generalization of the same principle. In this thesis we formulate the level by level version and the capturing version of SR (CSR). CSR is a direct generalization of the basic version of SR. We introduce and study the m-supercompact cardinals, the C(n)-m-fold extendible cardinals, and the capturing version of VP, and show that the pattern of correspondence between large cardinals and the basic version of SR also extends to the higher realm. We also apply our results to answer several open questions concerning ESR. Finally, we note that CSR, when generalized to its ω-version, leads to inconsistency.
A classification of the set-theoretic total recursive functions of KPl
(2024-07) Fernández Dejean, Anton; Joosten, Joost J.; Aguilera, Juan Pablo
The set theory KPl, which stands for Kripke-Platek-limit, roughly stipulates that there are unboundedly many admissible sets. Admissible sets are models of the Kripke-Platek set-theory KP which is a very weak fragment of ZFC. In [1], J. Cook and M. Rathjen classify the provably total set functions in KP using a proof system based on an ordinal notation system for the Bachmann-Howard ordinal relativized to a fixed set. In this paper, we adapt this result to the KPl set theory. We consider set functions which are provably total in KPl and Σ-definable by the same formula in any admissible set. We prove that, if f is such a function then, for any set x in the universe, the value f(x) always belongs to an initial segment of L(x), the constructible hierarchy relativized to the transitive closure of x, at a level below the relativized Takeuti-Feferman-Buchholz ordinal (the TFB ordinal is the prooftheoretic ordinal of KPl). To prove this result, we first construct an ordinal notation system based on [2] for KPl relativized to a fixed set that we will use in order to build a logic dependent on this fixed set where we will embed KPl. Thanks to this relativized system, we will be able to bound the value of the function at this fixed set.
Inconsistency lemmas and the inconsistency by cases property
(2024-07) Hortelano Martín, Isabel; Moraschini, Tommaso; Ugolini, Sara
La teoria dels lemes d’inconsistència no ha estat investigada sistemàticament fins al moment, amb només unes poques excepcions notables. Raftery va demostrar que per a una lògica protoalgebraica finitària tenir un lema d’inconsistència (global) equival a requerir que el semireticle superior de filtres deductius compactes en cada àlgebra del tipus corresponent sigui dualment pseudocomplementat. Posteriorment, Lávička i Přenosil van introduir les versions local i local parametritzada de manera similar a la jerarquia de teoremes de deducció i van presentar la contrapart algebraica del lema d’inconsistència local, l’anomenada propietat d’extensió de filtres consistents maximals. En aquest projecte, presentem els resultats existents traduïts al marc de les lògiques protoalgebraiques finitaries. A més, s’introdueixen dues nocions noves: la propietat d’inconsistència per casos i la definibilitat (de primer ordre) de filtres consistents maximals. En paral·lel a la connexió entre la propietat de demostració per casos i la distributivitat dels filtres, demostrem que el teorema pont corresponent sorgeix entre la propietat d’inconsistència per casos i la 1-distributivitat dels filtres . Finalment, creuant enrere i endavant sobre el pont a l'entorn sintàctic i algebraic, el resultat crucial de la tesi afirma que una lògica protoalgebraica finitària té un lemma d’inconsistència si i només si té la propietat d'extensió de filtres consistents maximals, per a cada àlgebra A el filtre deductiu A és finitament generat, té filtres consistents maximals definibles i és filtre-1-distributiu.
Rational and Delta expansions of the Nilpotent Minimum Logic
(2024-07) Sempere Camín, Paula; Gispert Brasó, Joan
[eng] The aim of this thesis is to study some expansions of the Nilpotent minimum logic (denoted by NML), focusing on their lattices of axiomatic and finitary extensions and, additionally, exploring the structural completeness of these logics, alongside their variants (active structural completeness, passive structural completeness, ... ). The project includes research about the rational Nilpotent minimum logic (designated by RNML), which is obtained by adding rational constants to the language of NML. Moreover, we also study the Δ-core fuzzy logic obtained by expanding the language of NML with the Baaz Delta connective and examine the impact of the incorporation of rational constants to the language of this logic (which is equivalent to the addition of the Baaz Delta connective to RNML). The thesis culminates with the corresponding analysis of an extension of the later logic which is obtained by introducing bookkeeping axioms for the Δ operator, motivated by the aim for the algebra of constants to form a subalgebra. In the project, through comparative analysis, the differences and similarities between the lattices of axiomatic and finitary extensions among the previously mentioned expansions are evaluated, as well as how the structural completeness results obtained may vary from one logic to another.
Meet-irreducible elements in the poset of all logics
(2024-07) Muñoz Pérez, MIguel; Moraschini, Tommaso
[cat] En aquest treball hem estudiat els elements meet-irreductibles del poset Log de totes les lògiques. A més, hem presentat les eines tècniques requerides, com la relació d’interpretabilitat entre lògiques i la construcció del producte no-indexat d’una família de lògiques, inspirades en l’anàlisi del lattice de les varietats de l’àlgebra universal. Finalment, hem treballat en criteris de meet-irreductibilitat per a alguns sub-semilattices de Log
Epimorphism Surjectivity in Logic and Algebra
(2024-07) Kurtzhals, Miriam; Moraschini, Tommaso; Carai, Luca
As the theorems we aim to prove require a variety of tools and background theory, we will start by recalling some basics of first-order logic (Section 2.1), model theory (Section 2.2), and universal algebra (Section 2.3). We will then continue presenting the protagonist of this thesis, the epimorphism surjectivity property, and making some easy but useful observations concerning this property (Section 2.4). Finally, we will establish a correspondence between the (weak) ES property in algebra and the (finite) Beth definability property in logic, providing motivation for the study of the ES property from a logical standpoint (Section 2.5)
On interval logics and stopwatches in model-checking real-time systems
(2024) López Chamosa, Marina; Joosten, Joost J.; Müller, Moritz
Our thesis focuses on the model-checking problem, which is at the heart of both formal verification of software and algorithmic law. In general, this computational problem consists of deciding whether a given structure fulfills a given property expressed by a sentence in a logic1. These structures and logics can take many forms. We speak of algorithmic law whenever the application of that particular law is intended to be performed by a computer on a data set representing a real case. In the field of algorithmic law one needs an algorithm to decide whether a particular real case is legal or not. For a model-checking approach, the law is formalized by a sentence in some logic, whereas a case is viewed as a word structure. In the field of formal verification of software, whose goal is to test whether a program works correctly, the verification task is naturally formalized as a modelchecking problem by associating a structure to every program, and a sentence in a suitable logic to every desired property of the program [4]. The model-checking framework often allows to transform a complex and informal question into the formally precise computational problem of whether K ⊨ φ, where the input K is in some class of structures K and the input φ is in some language L. As a result, it is of practical interest in many realworld applications, providing both simple procedures and mathematical proofs of correctness. Thus, the computational complexity of the mentioned problem is of central importance. In our thesis, we discuss different formalisms as inputs of the model-checking problem to analyze their complexity. In particular, the model-checking problem of linear-temporal properties is studied, both in the presence of discrete and continuous time, with an automata-theoretic approach. The strategy in this setting is to reduce questions about models and sentences, to questions about automata, and then provide an answer using standard decision procedures for automata.
Unification in intuitionistic logic
(2023) Cristancho S., Sebastián R.; Moraschini, Tommaso; Vidal Wandelmer, Amanda
The concept of unification has been widely studied from a logical perspective. In the context of logic, a formula A is said to be unifiable in a logic ⊢ if there is a substitution σ that turns A into a theorem of ⊢. In this case, we say that σ is a unifier (in ⊢) of A, or that A is unifiable (in ⊢) by σ. Given a logic ⊢ and a unifiable formula A (in ⊢), there is a natural way to compare its unifiers in terms of generality using the fact that, up to logical equivalence, some unifiers can be ‘obtained’ from others. More precisely, we say that the unifier σ1 of A is less general than the unifier σ2 of A if there is a substitution τ such that σ1(x) is logically equivalent to τ(σ2(x)) in ⊢ for all propositional variables x in the domain of σ1 and σ2. This gives rise to a hierarchy among the set of unifiers of A, where the unifiers in lower levels can be obtained from the unifiers in upper levels. A basis of unifiers of a unifiable formula A is a set of incomparable elements that ‘generates’ any other unifier of A. The study of the hierarchy among unifiers rises some interesting questions: Given a unifiable formula A in ⊢, is there a basis of unifiers of A? If so, is it finite or infinite? If it is finite, does it have one or more elements? These questions can be stated not only for formulas, but for logics in general.
Stationary Reflection on Pₖ (λ)
(2022) Torres Pachón, Martha Catalina; Bagaria, Joan
Throughout history, mathematicians have had to deal with infinity, always considering it in the “potential” sense, rather than an actual object. It was not until the late nineteenth century that actual infinity was the subject matter. In 1874 George Cantor published “On a Property of the Collection of All Real Algebraic Numbers”. From the results he proved in that paper, he concluded that there were larger infinites than others, giving birth in this way to Set Theory, the study of infinite sets and the set-theoretic foundations of mathematics. The study of infinite sets, and in particular their combinatorial properties, is not only of interest in itself, but it has numerous applications in areas such as analysis, algebra and topology (see e.g. [1; 2; 3]). Even possible applications to mathematical biology have being studied [4]. Combinatorics is always concerned about sizes, and when dealing with infinite sets there are different ways to capture the idea of how large a set is. For example, the notion of “filter” on a set A corresponds to “big” subsets of A, while positive subsets in the sense of a given filter corresponds to the notion of “not small”. Stationary subsets of a cardinal k are those that are not small in the sense of the closed and unbounded filter of k.
Cardinals Beyond Choice and the HOD-Dichotomy
(2020) Spoerl, John; Bagaria, Joan
In the 2019 paper "Large Cardinals Beyond Choice" [1], Bagaria, Koellner and Woodin apply the large cardinal techniques and results developed fromWoodin's work on the HOD-Dichotomy to determine the structural resemblance of HOD to V . Whereas standard inner model theory attempts to nd suitable inner models for large cardinals, this new program is aimed at exploring very large cardinals that \break" the resemblance of HOD to V . This paper attempts to explain in full detail the tools and arguments required for that body of work.
Interpretability logics and generalized Veltman semantics in Agda
(2021-01) Mas Rovira, Jan; Joosten, Joost J.; Mikec, Luka
[eng] Suﬀiciently strong arithmetical theories such as PA can formalize their interpretability predicate. This predicate expresses the concept of relativized interpretability between finite extensions of the theory. Interpretability logics study the provable structural behaviour of the interpretability predicate. Interpretability logics extend the provability logic GL. As such, interpretability logics inherit a number of similarities from GL. For instance, the possibility to give relational semantics. In this thesis we focus on the study of two variations of relational semantics à la Kripke known as ordinary Veltman semantics and generalized Veltman semantics. In the literature we find various definitions of generalized Veltman semantics. In particular, there are several conditions of quasi-transitivity, a property that generalized frames must satisfy. We study the interrelations between all of these conditions and discuss their adequacy. In this thesis we compare the expressiveness of ordinary and generalized Veltman semantics. Furthermore, we give procedures that under some assumptions transform, while preserving modal theoremhood, ordinary models to generalized models and vice versa. We study the frame conditions of various relevant interpretability principles present in the literature. Moreover, we provide novel frame conditions for the the principle R1 and the Rn series of principles from [16] with respect to generalized Veltman semantics. We have formalized our findings in Agda, which is a state-of-the-art proof assistant based on an intuitionistic theory which features dependent types. Apart from giving a solid base to our claims, we hope that our Agda library will provide a rallying point for researchers willing to formalize theorems in the field of interpretability logics, or at least, to encourage more research in that direction. Our work is, to our knowledge, the first attempt at formalizing interpretability logics in any proof assistant.

El Dipòsit Digital ha actualitzat el programari. Contacteu amb dipositdigital@ub.edu per informar de qualsevol incidència.

Examinar

Enviaments recents