Pawel Pawlowski

The relationship between formal and informal provability has been a significant subject of philosophical and mathematical investigation. Formal systems such as Gödel-Löb logic (GL) capture formal provability but do not validate the reflection schema—a principle stating that if a statement is provable, it must be true. This schema is intuitively valid for the informal notion of provability as understood and used in mathematical practice. Several logical systems have been developed to capture this informal notion of provability, including BAT, CABAT, and T-BAT. However, a first-order version of T-BAT logic has not yet been developed. This paper aims to address this research gap by providing such an extension.

T-BAT logic is a formal system designed to express the notion of informal provability. This type of provability is closely related to mathematical practice and is quite often contrasted with formal provability, understood as a formal derivation in an appropriate formal system. T-BAT is a non-deterministic four-valued logic. The logical values in T-BAT semantics convey not only the information whether a given formula is true but also about its provability status. The primary aim of our paper is to study the proposed four-valued non-deterministic semantics. We look into the intricacies of the interactions between various weakenings and strengthenings of the semantics with axioms that they induce. We prove the completeness of all the logics that are definable in this semantics by transforming truth values into specific expressions formulated within the object language of the semantics. Additionally, we utilize Kripke semantics to examine these axioms from a modal perspective by providing a frame condition that they induce. The secondary aim of this paper is to provide an intuitive axiomatization of T-BAT logic.

This paper explores the development and evaluation of physics-specific large-scale AI models, which we refer to as large physics models (LPMs). These models, based on foundation models such as large language models (LLMs) are tailored to address the unique demands of physics research. LPMs can function independently or as part of an integrated framework. This framework can incorporate specialized tools, including symbolic reasoning modules for mathematical manipulations, frameworks to analyse specific experimental and simulated data, and mechanisms for synthesizing insights from physical theories and scientific literature. We begin by examining whether the physics community should actively develop and refine dedicated models, rather than relying solely on commercial LLMs. We then outline how LPMs can be realized through interdisciplinary collaboration among experts in physics, computer science, and philosophy of science. To integrate these models effectively, we identify three key pillars: Development, Evaluation, and Philosophical Reflection. Development focuses on constructing models capable of processing physics texts, mathematical formulations, and diverse physical data. Evaluation assesses accuracy and reliability through testing and benchmarking. Finally, Philosophical Reflection encompasses the analysis of broader implications of LLMs in physics, including their potential to generate new scientific understanding and what novel collaboration dynamics might arise in research. Inspired by the organizational structure of experimental collaborations in particle physics, we propose a similarly interdisciplinary and collaborative approach to building and refining large physics models. This roadmap provides specific objectives, defines pathways to achieve them, and identifies challenges that must be addressed to realise physics-specific large scale AI models.

In previous publications, it was shown that finite non-deterministic matrices are quite powerful in providing semantics for a large class of normal and non-normal modal logics. However, some modal logics, such as those whose axiom systems contained the Löb axiom or the McKinsey formula, were not analyzed via non-deterministic semantics. Furthermore, other modal rules than the rule of necessitation were not yet characterized in the framework.In this paper, we will overcome this shortcoming and present a novel approach for constructing semantics for normal and non-normal modal logics that is based on restricted non-deterministic matrices. This approach not only offers a uniform semantical framework for modal logics, while keeping the interpretation of the involved modal operators the same, and thus making different systems of modal logic comparable. It might also lead to a new understanding of the concept of modality.

In 2008 Christopher Hardin and Alan Taylor published an article titled “Peculiar connection between the axiom of choice and predicting the future” in which they claim that if some system can be described as a function from a set of some instants of time to some set of states, then there is a way to predict the next value of the function based on its previous input. Using their so-called $$\mu $$ -strategy one can randomly choose an instant t and the probability that the strategy is correct at t (i.e. that the output for a strategy for input t is exactly the same as the value of the function) equals 1. Mathematical aspects of this article are sound, but the background story about the correlation between theorems and philosophical aspects of predicting the future faces certain problems. The goal of my paper is to bring them up.

The increasing use of AI in healthcare has sparked debates about responsibility and accountability for AI-related errors. The difficulty in attributing moral responsibility for undesirable outcomes caused by increasingly autonomous (often opaque) AI systems has become a new focal point in the debate on ‘responsibility gaps’. We approach the problem of these gaps by offering a framework that combines causal selection principles from the philosophy of science with recent accounts of authorship attribution in AI contexts. We argue this framework offers a more comprehensive and context-sensitive approach to the responsibility gap in medical AI.

Computational Reliabilism (CR) has emerged as a promising framework for assessing the trustworthiness of AI systems, particularly in domains where complete transparency is infeasible. However, the rise of sophisticated adversarial attacks poses a significant challenge to CR’s key reliability indicators. This paper critically examines the robustness of CR in the face of evolving adversarial threats, revealing the limitations of verification and validation methods, robustness analysis, implementation history, and expert knowledge when confronted with malicious actors. Our analysis suggests that CR, in its current form, is inadequate to address the dynamic nature of adversarial attacks. We argue that while CR’s core principles remain valuable, the framework must be extended to incorporate adversarial resilience, adaptive reliability criteria, and context-specific reliability thresholds. By embracing these modifications, CR can evolve to provide a more comprehensive and resilient approach to assessing AI reliability in an increasingly adversarial landscape.

Large language models (LLMs) such as ChatGPT present immense opportunities, but without proper training for users (and potentially oversight), they carry risks of misuse as well. We argue that current approaches focusing predominantly on transparency and explainability fall short in addressing the diverse needs and concerns of various user groups. We highlight the limitations of existing methodologies and propose a framework anchored on user-centric guidelines. In particular, we argue that LLM users should be given guidelines on what tasks LLMs can do well and which they cannot, which tasks require further guidance or refinement by the user, and context-specific heuristics. We further argue that (some) users should be taught to refine and elaborate adequate prompts, be provided with good procedures for prompt iteration, and be taught efficient ways to verify outputs. We suggest that for users, shifting away from looking at the technology itself, but rather looking at the usage of it within contextualized sociotechnical systems, can help solve many issues related to LLMs. We further emphasize the role of real-world case studies in shaping these guidelines, ensuring they are grounded in practical, applicable strategies. Like any technology, risks of misuse can be managed through education, regulation, and responsible development.

The aim of this paper is to study a particular family of non-deterministic semantics for modal logics that has eight truth-values. These eight-valued semantics can be traced back to Omori and Skurt (2016), where a particular member of this family was used to characterize the normal modal logic K. The truth-values in these semantics convey information about a proposition’s truth/falsity, whether the proposition is necessary/not necessary, and whether it is possible/not possible. Each of these triples is represented by a unique value. In this paper we will study which modal logics can be obtained by changing the interpretation of the $$\Box $$ modality, assuming that the interpretation of other connectives stays constant. We will show what axioms are responsible for a particular interpretations of $$\Box $$. Furthermore, we will study subsets of these axioms. We show that some of the combinations of the axioms are equivalent to well-known modal axioms. We apply the level-valuation technique to all of the systems to regain the closure under the rule of necessitation. We also point out that some of the resulting logics are not sublogics of S5 and comment briefly on the corresponding frame conditions that are forced by these axioms. Ultimately, we sketch a proof of meta-completeness for all of these systems.

According to the dialetheist argument from the inconsistency of informal mathematics, the informal version of the Gödelian argument leads us to a true contradiction. On one hand, the dialetheist argues, we can prove that there is a mathematical claim that is neither provable nor refutable in informal mathematics. On the other, the proof of its unprovability is given in informal mathematics and proves that very sentence. We argue that the argument fails, because it relies on the unjustified and unlikely assumption that the informal Gödel sentence is informally provable.

Classical logic of formal provability includes Löb’s theorem, but not reflection. In contrast, intuitions about the inferential behavior of informal provability (in informal mathematics) seem to invalidate Löb’s theorem and validate reflection (after all, the intuition is, whatever mathematicians prove holds!). We employ a non-deterministic many-valued semantics and develop a modal logic T-BAT of an informal provability operator, which indeed does validate reflection and invalidates Löb’s theorem. We study its properties and its relation to known provability-related paradoxical arguments. We also argue that T-BAT is a fairly sensible candidate for a formal logic of informal provability.

BAT is a logic built to capture the inferential behavior of informal provability. Ultimately, the logic is meant to be used in an arithmetical setting. To reach this stage it has to be extended to a first-order version. In this paper we provide such an extension. We do so by constructing non-deterministic three-valued models that interpret quantifiers as some sorts of infinite disjunctions and conjunctions. We also elaborate on the semantical properties of the first-order system and consider a couple of its strengthenings. It turns out that obtaining a sensible strengthening is not straightforward. We prove that most strategies commonly used for strengthening non-deterministic logics fail in our case. Nevertheless, we identify one method of extending the system which does not.

Recently, in an ongoing debate about informal provability, non-deterministic logics of informal provability BAT and CABAT were developed to model the notion. CABAT logic is defined as an extension of BAT logics and itself does not have independent and decent semantics. The aim of the paper is to show that, semantically speaking, both logics are rather complex and they can be characterized by neither finitely many valued deterministic semantics nor possible word semantics including neighbourhood semantics.