Masteruppsatser / Master in Logic

Permanent URI for this collectionhttps://gupea-staging.ub.gu.se/handle/2077/89643

Browse

Now showing 1 - 13 of 13

Inflationary µ-Calculus via an Infinitary Proof-System: Foundations, Soundness, and Completeness
(2025-08-15) Nematpur, Manzoor; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
Inflationary fixed-point logic (IFPL) extends modal logic with non-monotonic, in- flationary fixed-point operators, achieving greater expressiveness than the standard µ-calculus. While IFPL can define properties beyond regular languages and classical fixed-point systems, its lack of desirable properties (no finite model property, undecid- ability) and poor algorithmic tractability have relegated it to theoretical obscurity. This thesis bridges a foundational gap by proposing two novel infinitary proof systems: Kω (µ∗) with an ω-rule, and Kω1 (µ∗) with an ω1-rule, to derive deflationary fixed points. We adapt techniques from ω-rule-based µ-calculus systems to handle inflationary semantics, introducing dual approximation rules for fixed points. By restricting to the alternation-free fragment AF-Kω1 (µ∗), we sidestep nested fixed-point complexities while preserving core challenges. We present: (1) Soundness of Kω (µ∗) for finite models and soundness of Kω1 (µ∗) for all models. (2) Completeness of AF-Kω1 (µ∗) through a novel canonical model construction building on saturated sets and relying on truth-set signatures for the model con- struction. Beyond technical contributions, this work serves as an accessible introduction to (inflationary) fixed-point logics, explicitly detailing often-overlooked proofs and intu- itions. While completeness remains partial, the framework lays groundwork for future exploration of tractable IFPL-fragments or circular proof systems. The results suggest that inflationary operators, long dismissed as impractical, may yet find application in, for example, epistemic reasoning when carefully constrained.
Boolean valued models of set theory
(2025-08-04) Zaninotto, Alessio; University of Gothenburg / Department of Philosophy,Lingustics and Theory of Science; Göteborgs universitet / Institutionen för filosofi, lingvistik och vetenskapsteori
Given a first-order language L, a Boolean-valued model (BVM) for Lis a gener- alization of the classical notion of a Tarskian L-structure, in which formulas have truth values ranging over a Boolean algebra. In this work, we provide a short and self-contained presentation of the theory of BVMs. After that, we specialize on Boolean valued models of (the language of) set theory. These turn out to be a natural setting to develop the technique of forcing, introduced by Paul Cohen to prove the celebrated independence of the Continuum Hypothesis. In the final part of this work, we apply this framework to the study of the current literature in inner model theory, showing that the Boolean valued framework is particularly well-suited to produce general models into which any model of a sufficiently rich fragment of the theory of an initial segment of the universe can be embedded.
Translating Path-based Logics to Modal mu-Calculus
(2024-10-07) Lim, Fong Yuan; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
The modal μ-calculus Lμ is an expressive temporal logic defined on full transition systems. Lμ merely has immediate neighbour modalities and no direct way to specify properties on a path-by-path basis, so it is remarkable that Lμ can simulate logics such as linear temporal logic (LTL) whose semantics are based on linear paths, where an LTL formula ϕ is said to hold at a state s if ϕ holds on every path starting from s. However, expressing such path-based properties in Lμ is generally nontrivial. As a baseline, one may find a translation by constructing an automaton as an intermediate step. However, a naive implementation of such a method may cause a non-elementary blowup in the size of the translation. A translation obtained this way also tends to reflect the structure of the automaton rather than that of the original input formula. In this thesis, we investigate a more syntactic approach to translate path-based logics into Lμ. In particular, we analyse the method given by [Dam94] to translate LTL into Lμ in depth, and reformulate it in several aspects. Furthermore, we generalise the method to the fragment of the linear-time μ-calculus LTμ where fixpoint variables in a formula occur exactly once and are not nested. These translations achieve a worst-case doubly exponential blowup in formula size. For simpler inputs, directly inspecting the translations may yield insights as to how Lμ accommodates path-based properties.
Cyclic Proofs for Theories of Truth
(2024-08-12) Gortworst, Bente; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
Formal theories of truth aim to help us understand the notion of truth and its role in logic and mathematics. The field has come forth from Tarski’s effort to give a formal truth definition, and has since seen significant developments. One of the guiding theories on mathematical truth is Kripke’s semantic theory which partially models the truth predicate as a minimal fixed point. Kripke’s theory has motivated several axiomatic theories that capture this truth notion. Among them the most popular seems to be the theory Kripke- Feferman (KF). Investigations into the proof theory of KF have been ongoing and inform our understanding of the relation between truth and provability in mathematical logic. In this thesis we contribute to these investigations through the lens of cyclic proofs, a type of formal proof that allows for finite proof-theoretic representations of possibly infinite derivations through cyclic reasoning. This type of proof has received much attention in recent years due to its practical applicability, and has been analyzed in the context of several logical theories, but has not yet been applied to theories of truth. Therefore we bring together the streams of research by developing a cyclic proof system for the theory KF. We also demonstrate we are able to further expand this system into cyclic systems for μKF (a version of KF where truth and falsity are taken to be minimal fixed points), and νKF (which takes truth and falsity to be maximal fixed points). We show that all three systems are sound with respect to their semantic construction and that we can simulate inductive reasoning through cyclic rules in these systems.
Type Theories of Natural Numbers: A Study of Conservative Extension
(2023-06-30) Babunović, Aleksandar; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
We present some possible definitions for what it means for a type theory to be a conservative extension over another type theory. We do so by giving two type theories of natural numbers: T T (N) and T T (N, ×). T T (N) is a type theory that comprises only the natural numbers as a type, while TT(N,×) is an extended theory of TT(N) that includes an additional type constructor that can form pair types. Our aim is to search for a general definition of a conservative extension. Our approach does not only involve judgements in our definition of conservativity, but also convertibility between terms, which corresponds to the process of computation for each type theory. Understanding type theories and their computation have valuable implications in research areas, such as in Computer Science, particular in the context of proof assistants and other fields where type theory is considered. We prove that TT(N,×) is not a conservative extension over TT(N) in the strongest sense, by giving a counter example, but that it is a conservative extension in three other senses. We do this by defining a translation from TT(N,×) to TT(N), we define terms in TT(N) that will represent terms from TT(N,×), and therefore use the translation to prove conservativity. Our contribution lies in providing a deeper understanding of the relationships between type theories, specifically focusing on type theories that are fragments of Martin-L ̈of type theory, where Martin-L ̈of type theory serves as an alternative foundation of mathematics. We argue why one of the notions of conservative extension, proposed in this thesis, is the most suitable definition to establish a conservative extension between T T (N) and T T (N, ×). From this notion of conservative extension, we discover that since they are conservative, they denote the same functions, specifically the primitive recursive functions. This motivates us to utilize this definition of conservative extension, because it provides the insight that if two theories are conservative, they denote the same functions. If this is the case in general between type theories then this deserves further research on our notions of conservativity, as it may be helpful for transferring theorems. This could serve as a new feature for proof assistants that are based on a type theory, with a particular focus on conservativity. These findings prompt further questions: can these definitions of conservative extensions be regarded as a general definition within the context of type theory? Can these definitions be valuable in applications within type theory? Are there any significant implications that arise from conservative extensions in type theories overall? Having an understanding of conservative extensions and their implications has the potential to enhance our understanding of type theory.
Quantitative Probabilistic Fixed Point Logic and the Problem of Satisfiability
(2023-06-26) Lazar, Vlad; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
The analysis of time-dependent systems in a probabilistic setting has greatly benefited from the application of temporal logic. This thesis focuses on a specific probabilistic modal fixed point logic setup, which offers a higher level of expressiveness compared to conventional probabilistic logics by incorporating quantitative semantics. Additionally, the logic has the capability of encoding proba- bilistic computation tree logic, one of the most widely used logics in probabilistic model checking. The decidability of the satisfiability problem for this logic however, remains a significant open prob- lem. In this thesis we propose a tableau system for the quantitative probabilistic fixed point logic that is intended to characterise satisfiability. Drawing inspiration from related work, the tableau con- struction we propose has novel rules that syntactically capture the quantitive aspect of the logic. Our objective is to demonstrate that the proposed structure is suitable for further exploration while offering a deeper understanding of the complexity associated with solving the satisfiability problem for this logic.
Hydra Games for Cut Elimination and Ordinal Analysis of IPL2
(2023-06-22) Feuilleaubois, Armand; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
Intuitionistic propositional logic with 2nd order propositional quantifiers (IPL2) was introduced by Gabbay in 1974. Since then, a substantial body of work has been written about its semantics. However, there has not been any work thoroughly exploring the proof theory of IPL2, or even defining a Gentzen style sequent calculus. We define two fragments of IPL2 that will be the focus of our efforts. First, the fragment corresponding to the absence of quantifier rule appli- cations to formulas that are later used as cut formulas. Second, the fragment corresponding to the application of at most quantifier free substitutions in quantifier rules that are applied to formulas that are later used as cut formulas. In this work, we will define such a sequent calculus, and prove that these two fragments have the property of cut elimination. In order to prove this, we will make use of 𝑛-ary multicut rules and hydra games. Our proof of cut elimination will make use of cut rewrite operations, as with the usual proof. However these will be applied to the tree structure within an application of a multicut rule, rather than to the proof trees themselves. We will use the cut rewrite operations as moves within a Büchholz hydra game. These will show that, despite the blowup in the proof size and the length of the multicut, the hydra game on its tree must terminate. Then we show that this termination property on the multicut rewrite hydra game corresponds to cut elimination for the fragment of IPL2 in question. Because of the explicit measure assigned to the multicut trees within the hydra game, we immediately obtain an upper bound for an ordinal analysis of both of the fragments from the cut elimination proof. This ordinal is 𝜔𝜔 . Finally, we discuss the failure of this method for the full IPL2 calculus.
Deflationism in Logic, Formal Theories of Truth and Philosophy
(2023-06-20) Collazos Chaves, María Camila; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
The concept of truth has been studied and used along the areas of philosophy, logic, and mathematics. Although is the same word (“truth”) it has been used in very different ways in each area. Logicians have studied truth in the context of formal theories, while philosophers have examined it in natural languages and the world in general. The Deflationist Theory of Truth, however, seems to be a middle ground between these approaches. According to this theory, truth has a thin nature, meaning that it has little metaphysical content and does not add much to a sentence when used. This work aims to explore how these two approaches can be connected and how deflationism can be understood in them. It specifically addresses the question of conservativity in the formal theory known as the Compositional Theory of Truth and how it relates to deflationism. This project includes a review and critique of the literature on the subject, including its history, logic, results, and the arguments made by its main proponents (such as Tarski, Ramsey, Halbach, Leigh, Field, Horsten, among others). Additionally, this work suggests possible solutions to the questions posed above. The purpose of this thesis was to establish a connection between formal theo- ries of truth, specifically axiomatic theories of truth and the theory of CT , and the philosophical approach to truth, particularly deflationism in formal and natural lan- guage. My main contributions and results are presented in Chapter 5.2 titled "Is truth deflationist?" In this chapter, I propose two distinct labels for different forms of defla- tionism, address the question of whether CT is an appropriate theory for deflationism, with a particular focus on the conservativity feature, and suggest how philosophical and formal approaches can collaborate with each other. This entails considering how the truth predicate behaves in various formal theories when contemplating the nature of truth, as well as taking into account other philosophical positions such as pragmatism or coherence.
What’s the Name of the Game? Dialogue Game Semantics for Intuitionistic Modal Logic with Strict Implication
(2022-06-27) Wolff, Johanna; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
In this thesis we will develop dialogue game semantics for intuitionistic modal logic with strict implication. We begin by introducing Kripke se- mantics and proof systems for intuitionistic modal logic. Afterwards, we define a dialogue semantics for classical and intuitionistic propositional logic similar to the one found in [1] and a dialogue semantics for modal logic based on the work in [11]. We then discuss a suitable way to include strict implication in this framework. However, when adding strict impli- cation to the existing dialogue semantics for intuitionistic modal logic, the interdefinability of strict implication and the box operator is valid, even though it does not hold in intuitionistic modal logic. We suggest two ways of fixing this issue. First, we adapt the dialogue semantics for intu- itionistic modal logic to mirror the approach that is taken for the Kripke semantics. This involves adapting the dialogue semantics for classical modal logic into dialogue semantics for intuitionistic propositional logic and then creating a Bi-Modal dialogue semantics for intuitionistic modal logic. We then add strict implication to this system and show that the resulting semantics is sound and complete with respect to intuitionistic modal logic. The second approach that we explore is to restrict the way players may use previous information in our dialogue games. We then show that these two approaches are equivalent. Finally we discuss the benefits of both systems and discuss directions for further research.
Proof Theory of Circular Description Logics
(2022-06-23) Femke Dik, Josephine; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
In [12], Hofmann introduces a sequent calculus for the description logic EL where the TBoxes allow for circular concept definitions. In this thesis, we apply this frame- work to a family of DLs which allow for circular TBoxes. We start off by adjusting the calculus for the class of frame-based DLs, with base logic FL0. We continue to the attribute languages AL and ALE. For these calculi, we prove soundness and completeness with respect to greatest fixpoint semantics for their fragments AL′ and ALE′, using Hofmann’s strategy. When applying the theory to a logic including disjunction, we require a different strategy and introduce the notion of pre-interpretation for the soundness and completeness proofs. Then, we acknowl- edge the drawbacks of considering only greatest fixpoint semantics when it comes to circular definitions, and propose a calculus that includes greatest- and least-fixpoint semantics in one. Finally, we discuss the drawbacks of Hofmann’s system for the classical logic ALC by discussing the consequences for the proofs when including the disjunction or negation, and give suggestions for future research.
Monadic Semantics, Team Logics and Substitution
(2022-06-14) Lorimer Olsson, Orvar; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
In this thesis we investigate the issue of non-substitutionality of propositional team logics, in particular propositional dependence logic, by semantic means. We establish a general language to discuss semantic systems for logics fundamentally based on consensus of truth in a class of objects. Importantly we admit a notion of logic that does not assume closure under substitution. We show how to express traditional semantic systems using this general language and describe a condition of being truth-compositional defined using a notion of defining sets for formulas. We then give an account of propositional dependence logic as described by Yang and Väänänen [YV16], and investigated by Lück [Lüc20] and Quadrellaro [Qua21].This is done using valuational team semantics based on sets of valuations as semantic objects. For valuational team semantics in general we describe the property of flatness and prove that a flat valuational team semantics always is equivalent to a standard valuational semantics. We then formulate the problem of non-substitutionality for logics based on the semantics and describe some of the consequences it has for the development and investigation of team logics. The main part and contribution of this thesis develops a new semantic framework we call monadic semantics, constructed by considering a universe for which propositional variables are interpreted as unary predicates by monadic models and the interpretation of complex formulas are governed by a monadic frame. We show how monadic semantics are sufficient to express every logic with truth- compositional semantics, in the sense defined, by constructing monadic dual semantics. We also define the maximal and the full semantics of a monadic frame. We show how a notion of monadic team semantics corresponding to Yang and Väänänens construction can be identified as a particular type of monadic semantics and translate the results regarding flatness to this setting. With this se- mantic notion defined we utilise a definiton of interpretation sets for formulas to express notions of independence and generality of atoms in a semantics. With this in place we can prove connections between these properties of a semantics, and substitutionality of the logic it defines. In this way we can give a full semantic categorisation of whether a logic is closed under singular substitution, and both a necessary and a sufficient condition for unrestricted substitution in any logic with monadic semantics. As a direct consequence these categorisations imply that every maximal monadic seman- tics that correspond to a semantics of Yang and Väänänen’s construction is either flat, or its logic is not closed under substitution. We reveal that the main reason for this is the treatment of atomic formulas in valuational team semantics. In the last part of the thesis we use monadic semantics and introduce natural teamifications to construct a semantics defining a new logic we call boolean teamified boolean logic, BTB. We com- plement this by exhibiting a set of axioms that, when assumed in BTB, gives an up to typographical renaming conservative extension of propositional dependence logic. We also hint on strong connec- tions between BTB and Girard’s linear logic [GLR95].
Dialetheism and the Law of Non-contradiction
(2021-09-15) Mak, Siu Fung; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
To say that the Law of Non-contradiction (LNC) underpins Western philosophy is perhaps not an exaggeration, but the discovery of paradoxes poses a serious challenge to its foundational status. This paper examines and defends one of the most thought-provoking solutions - dialetheism, which proposes that there are indeed true contradictions. With the help of a model explaining how change in logic takes place, I discuss how, despite the LNC being regarded as the hallmark of rational thinking, it is possible to debate the LNC without being circular. I also evaluate arguments from both LNC proponents and opponents. Ultimately I conclude that the dialetheist comes out on top on both establishing a constructive argument and defending his position.
On the Reduction of Quantum Teams
(2020-09-04) Fokkens, Jelle Tjeerd; Göteborgs universitet/Institutionen för filosofi, lingvistik och vetenskapsteori; Göteborg University/Department of Philosophy, Linguistics and Theory of Science
In this thesis, a reduction procedure on quantum teams is defined. Physically, this reduction procedure can be seen as an attempt to describe the measurement results of a certain (quantum mechanics) experiment purely classically, i.e. with hidden variables. In complete agreement with the expectation, the failure of this attempt indicates that genuine quantum effects are in play; the reduction procedure halts without having converted the team to a multi-team. It can therefore be used to demonstrate contextuality in a given quantum team. The reduction procedure conserves the corresponding probability table as well as all the properties expressible in Quantum Team Logic. Finally, an attempt has been made to solve the open problem of the axiomatisation of QTL formulas that agree with quantum mechanics. Absence of references to literature indicates original work from the author.

Browse

Recent Submissions