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

URI permanent per a aquesta col·leccióhttps://hdl.handle.net/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 38

Truth, revenge, and the limits of semantic closure
(2026-09-01) Barreto Mayayo, Brick; Martínez Fernández, José, 1969-
This thesis examines the prospects for a sufficiently expressive language to contain a fully general, self-applicable truth predicate without incurring semantic incompleteness. It does so through a comparative analysis of Tarski’s truth hierarchy, Kripke’s fixed-point theory, Gupta and Belnap’s revision theory, and Field’s paracomplete approach, focusing on how each responds to the Liar paradox and the problem of revenge. Field’s claim of revenge immunity is then reassessed in the light of Welch’s boundedness result, leading to a broader discussion of whether semantic closure is a suitable standard of success for theories of truth and suggesting that revenge immunity may be better understood comparatively.
Ambiguity-marking Kleene logic: adapting K3 for or and some ambiguity in natural language
(2026-09-15) Tormo Bañuelos, Lucía; Gispert, Joan, 1961-; Bonatti, Luca L.
We start from the fact that or and some do not receive the same reading in every position in a sentence. Sometimes or allows both disjuncts to hold and sometimes it excludes them; sometimes some is compatible with all and sometimes it is not. What decides between one reading and the other is not so much the conversational situation as the monotonicity of the context in which the lexical item appears. Grice explains the phenomenon as an inference the hearer draws about what the speaker has chosen not to say. His explanation is cancellable, it rests on reasonable maxims, and it forces no change to the semantics. Nevertheless, we present a range of phenomena that escape it. These phenomena that escape the pragmatic explanation lead Gennaro Chierchia to argue that strengthening is not a conversational residue but a grammatical operation. We reconstruct his mechanism, which consists in a set of alternatives associated with each lexical item, and an exhaustification operator that can be anchored at any node of the syntactic structure, and illustrate it for or and some. Out of that discussion come four requirements any theory of the phenomenon would have to meet (lexical trigger, locality, sensitivity to monotonicity, and reversibility). We also show the mathematical requirements that his mechanism imposes: an intensional higher-order metalanguage, two-dimensional meanings with a composition rule of their own, contextual pruning, and repair strategies for the cases in which exhaustification turns out contradictory. With those requirements in mind, we propose an expansion of Strong Kleene, which we have called Ambiguity-marking Kleene logic (K3), intended to make the formal language itself record the ambiguity rather than resolve it. This calls for a connective that yields indeterminacy from determinate arguments, something no Strong Kleene connective does, and from it come the ambiguous disjunction ˜∨ and the ambiguous quantifier ˜∃. The algebraic study of the resulting logic shows that ˜∨ is the greatest lower bound, in the information order, of its two readings (the most informative value compatible with both), and it also shows how restrictive this design is: ˜∨ is not a lattice operation, it is not monotone in the truth order, it is not definable in Strong Kleene, and K3 has no theorems. We describe the formalisation of natural-language sentences as a function Φ that assigns to each sentence not a formula but a formula together with a set of admissible resolutions, over which a supervaluation is defined; polarity-sensitive pruning stages return the classical tautologies, idempotence and De Morgan, whereas absorption never returns. We show that the final stage, the hearer’s choice, cannot be a semantic operation, and that the point at which compositionality fails is the point at which semantics ends and pragmatics begins. We conclude by comparing the two frameworks over the fragment of language for which they are designed. Chierchia’s operator strengthens the sentence and returns a determinate proposition, whereas ˜∨ commits itself only where the two readings agree. Our framework meets the four requirements, though locality comes out weaker and the polarity that drives sensitivity to monotonicity is enumerated rather than characterised, and it covers considerably less: with no modals there is no free choice, with no epistemic content there are no ignorance inferences, and the discourse asymmetry of or is invisible to a commutative connective.
Beyond Degrees of Truth and the Axiomatization of Superintuitionistic Prime Mixed Models
(2026-08-28) Asensio García, Miguel; Gispert, Joan, 1961-
Introduction This thesis can be divided into two main parts. In the first part, after two chapters of overview of preliminary knowledge, we introduce a new family of logics, which we call order-based logics, and provide a Hilbert-style presentation for them. These logics are obtained by taking the axioms of a logic associated with a variety of bounded integral commutative residuated lattices and replacing the usual rule of modus ponens with a restricted version thereof. The motivation for introducing these systems is to study weaker counterparts of the well-known logics preserving degrees of truth associated with varieties of (bounded) integral commutative residuated lattices. The resulting systems form a family of paraconsistent logics for which we provide a natural matrix semantics. We also determine their position within the Leibniz and Frege hierarchies. In particular, we show that all order-based logics are fully selfextensional, while none of them is protoalgebraic and, all of them fail to be (fully) Fregean. Furthermore, we prove that the order-based logic associated with classical logic coincides with a language reduct of the well-known paraconsistent logic D2. As a consequence, this logic admits an interpretation into the global modal logic S5 as well as the local modal logic T via what Priest calls the Jaśkowski move in [11]. This result serves as the main motivation for the second part of the thesis.
An Exposition on Radin Forcing
(2016-07-01) Docherty, Curtis; Poveda, Alejandro; Bagaria, Joan
Chapter 1 Historical Introduction The origins of set theory date back to the late 19th century, due to the work of Georg Cantor. In Cantor’s theory, the relative size, or cardinality, of sets is based on whether they can be put into one-to-one correspondence with each other. He first showed how to put the natural numbers and algebraic numbers into such a correspondence, thereby establishing that these sets have the same cardinality. He then showed that no such bijection exists between the set of natural numbers and real numbers, meaning that the continuum represents a strictly larger infinite set.
Hybrid Logics for Spacetimes along the Causal Ladder
(2026-09-13) Tenorio Hernández, Pablo; Fernández Duque, David; McLean, Brett
We study how Modal and Hybrid Logic can be used to describe the causal structure of spacetime. Motivated by Malament’s Theorem, which shows that the causal order alone can recover the Lorentzian manifold structure up to conformal factor, we introduce a Hybrid Language capable of expressing spacetime notions such as future/past cones and chronological/causal diamonds. In terms of this language, the modalities F, P, @, and U are definable. Within this language we give axioms for characterising several levels of the Causal Ladder – non-total viciousness, chronology, causality, and distinguishability. The broader aim is to lay groundwork toward complete logics for the spacetimes classified by the Causal Ladder though this larger goal is left for future work
The Admissible Rules of Peano Arithmetic
(2026-09-14) van Oudheusden Navarro, Lucas; Joosten, Joost J.; Mojtahedi, Mojtaba
This thesis studies arithmetical admissibility, with the aim of characterising the admissible rules of Peano Arithmetic PA. Our approach relies on Solovay’s arithmetical completeness theorem [21], which establishes the fundamental connection between provability in PA and the provability logic GL. We therefore begin with a study of unification and admissibility in GL, following the work of Ghilardi [8] and Mojtahedi [17]. In particular, we study projective formulas and their semantic characterisation through extendability, and use these notions to obtain the finitary unification type of GL. We then return to arithmetical admissibility and show that admissibility in PA is not characterised directly by admissibility in GL. Instead, it admits a modal characterisation in terms of derivability in GLS, a non-normal extension of GL closely connected to truth in the standard model of arithmetic.
The n-proof by cases property
(2026-09-11) Ramírez Eirís, Miguel; Moraschini,Tommaso; Přenosil, Adam
This chapter reviews the background material used throughout the thesis: basic universal algebra, including quasivarieties and (relative) finitely subdirectly irreducible algebras, as well as basic lattice theory and Heyting algebras. Readers already comfortable with these topics may safely skip ahead, with one exception: the notion of a parametric equation and parametric quasiequation, introduced in Section 1.3, will likely be new even to those familiar with standard universal algebra.
Axiomatization of the elementary theory of finite root systems
(2026-09-08) Rodríguez Díaz, Pedro; Moraschini, Tommaso
A root system is a partially ordered set (poset) in which the set of successors of every element is linearly ordered, and above each element there exists a maximal one. We refer to a root system with a maximum as a cotree. In the literature, the terms forests and trees sometimes denote root systems and cotrees, respectively, but can also refer to their respective order duals. These tree-like structures are ubiquitous across various branches of mathematics. Central problems in set theory revolve around a special class of forests in which the set of predecessors of every node is well-ordered (see, e.g., [Jec71]). One of the five main systems in reverse mathematics also relates to trees through theWeak K¨onig’s Lemma (see, e.g., [Sim09, Chapter 4]). On the other hand, modal logic has the tree model property, under which every satisfiable modal formula is satisfied in a tree (see, e.g., [BRV01, Sections 1,2]). Trees also play a fundamental role in computability theory, for instance through König’s Lemma (see, e.g., [Soa16, Part II]), in automata theory (see, e.g., [KN01]), and in linguistics (see, e.g., [BPMMV94]). Moreover, a foundational result for this work is Rabin’s celebrated Tree Theorem (see [Rab69]), which establishes the decidability of the monadic second order theory of the two successor functions, S2S. This theorem is central to decidability theory because it implies the decidability of the elementary theory of several classes of structures, including trees, root systems, and their finite members. For the basics of monadic second order logic, we refer the reader to Section 2.4. For further details on the decidability of the monadic second order theory of S2S and related structures, see [Rab69], [KN01], and [Gur17].
Search to Decision Procedures for Time Bounded Kolmogorov Complexity
(2026-06-19) Ünal, Aydos; Atserias, Albert
In the 2024 paper “Exact Search-to-Decision Reductions for Time-Bounded Kolmogorov Complexity”, Hirahara, Kabanets, Lu, and Oliveira apply modern meta-complexity techniques—such as symmetry of information and computational depth—to solve a foundational open problem in time-bounded Kolmogorov complexity. This recent breakthrough provides exact search-to-decision reductions that can find exact minimal programs over any polynomial-time samplable distribution, whereas earlier works mainly focused on approximate reductions that output larger or slower programs. This master’s thesis unpacks their work, explaining in detail the underlying tools, technical mechanics, and proofs required to establish these results.
Until-Like Modalities in Topology
(2026-06-16) Gagarin, Aleksandr; Fernández Duque, David
The topological semantics of modal logic has been an active area of research ever since its introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. This thesis investigates two binary modalities, both of which mimic the Until modality from temporal logic. One is a path-reachability modality γ that has recently been studied in Bezhanishvili et al. (2024) in polyhedral semantics; we investigate its topological counterpart. Focusing on the language combining γ with the classical Cantor derivative modality and the universal modality, we exhibit an axiomatic system sound and complete both for the class of T1 topologies and for the class of all metric spaces, and establish its EXPTIME-completeness. We also axiomatize the logic of all topological spaces in a weaker language obtained by substituting the closure modality for the Cantor derivative. To prove our results, we introduce an equivalent neighborhood-like semantics allowing for the finite model property, and then encode it in a variant of propositional dynamic logic. The second topological modality we address is “until-a-boundary,” proposed by Aiello (2002). We point out that it can express several properties of topologies, notably regularity and zero-dimensionality. We also establish EXPTIME-completeness, though only for the logic of Alexandroff spaces.
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.

Examinar

Enviaments recents