Glucagon-like peptide-1 (GLP-1) receptor agonists, such as semaglutide, and dual GLP-1 and glucose-dependent insulinotropic polypeptide (GIP) receptor agonists, such as tirzepatide, have been found to be effective for treating obesity and diabetes, significantly reducing weight and the risk or predicted risk of adverse cardiovascular events. There is a global shortage of these medications that could last several years and raises questions about how limited supplies should be allocated. We propose a fair-allocation framework that enables evaluation of the ethics of current (...) practices and could guide governments, professional societies, and physicians in allocation decisions. (shrink)

This Viewpoint analyzes policies for covering GLP-1 receptor agonist drugs for obesity treatment across 13 high-income countries. It identifies four key lessons for developing coverage policies: 1) using up-to-date cost-effectiveness analyses that incorporate new evidence of benefits, 2) negotiating lower prices while preserving innovation incentives, 3) prioritizing coverage for specific populations rather than issuing blanket denials, and 4) treating obesity medications similarly to high-cost drugs for other conditions. It argues that blanket coverage denials are unethical and that countries should implement (...) targeted coverage policies that maximize benefits while managing costs. (shrink)

In our reply to critiques of our GLP-1 receptor agonist allocation framework, we explain that using potential years of life lost (PYLL) as a metric addresses racial health disparities without explicitly allocating resources based on race. This approach is "racism-conscious" and has legal and ethical challenges over race-based approaches. Meanwhile, though acknowledging the importance of cardiovascular risk assessment, we maintain in response to other interlocutors that focusing solely on immediate risk would ignore the broader goal of mitigating disadvantage. We emphasize (...) that our framework balances multiple ethical objectives beyond just maximizing medical benefits. (shrink)

Many factors determine whether and when a class of therapeutic agents will be successfully developed and brought to market, and historians of science, entrepreneurs, drug developers, and clinicians should be interested in accounts of both successes and failures. Successes induce many participants and observers to document them, whereas failed efforts are often lost to history, in part because involved parties are typically unmotivated to document their failures. The GLP-1 class of drugs for diabetes and obesity have emerged over the past (...) decade as clinical and financial blockbusters, perhaps soon becoming the highest single source of revenue for the pharmaceutical industry (Berk 2023). In that context, it is instructive to tell the story of the first commercial effort to develop this class of drugs for metabolic disease, and how, despite remarkable early success, the work was abandoned in 1990. Told by a key participant in the effort, this story documents history that would otherwise be lost and suggests a number of lessons about drug development that remain relevant today. (shrink)

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.

A well-known polymodal provability logic inlMMLBox due to Japaridze is complete w.r.t. the arithmetical semantics where modalities correspond to reflection principles of restricted logical complexity in arithmetic. This system plays an important role in some recent applications of provability algebras in proof theory. However, an obstacle in the study of inlMMLBox is that it is incomplete w.r.t. any class of Kripke frames. In this paper we provide a complete Kripke semantics for inlMMLBox . First, we isolate a certain subsystem inlMMLBox (...) of inlMMLBox that is sound and complete w.r.t. a nice class of finite frames. Second, appropriate models for inlMMLBox are defined as the limits of chains of finite expansions of models for inlMMLBox . The techniques involves unions of n -elementary chains and inverse limits of Kripke models. All the results are obtained by purely modal-logical methods formalizable in elementary arithmetic. (shrink)

This article evaluates seven strategies for managing the high costs of GLP-1 receptor agonists (GLP-1RAs) like semaglutide and tirzepatide for weight management: complete exclusion of coverage, annual cost increase caps, lifetime cost caps, tiered access, formulary reevaluation, subscription payment models, and patent reform. The authors assess each strategy against three ethical objectives: benefiting people and preventing harm, showing equal moral concern, and mitigating disadvantage. Complete coverage exclusions, arbitrary reimbursement caps, and lifetime limits are deemed unethical as they fail to meet (...) these objectives. Tiering access based on relative benefit is considered justifiable, though current implementation often unfairly favors diabetes over obesity treatment. The authors recommend formulary reevaluation as the most ethical approach for smaller health plans, allowing them to prioritize more cost-effective treatments. For larger payers with market power and for governments, subscription payment models and patent reforms are potentially ethical solutions if implemented sustainably. The authors conclude that health plans should avoid ad hoc restrictions on GLP-1RAs in favor of comprehensive policy reforms that ensure sustainable access to these and future breakthrough treatments. (shrink)

We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...) of GLP Λ. (shrink)

For any ordinal $\Lambda$, we can define a polymodal logic $\mathsf{GLP}_\Lambda$, with a modality $[\xi]$ for each $\xi < \Lambda$. These represent provability predicates of increasing strength. Although $\mathsf{GLP}_\Lambda$ has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities, denoted $\mathsf{GLP}^0_\omega$. Later, Icard defined a topological model for $\mathsf{GLP}^0_\omega$ which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary $\Lambda$. (...) More generally, for each $\Theta,\Lambda$ we build a Kripke model $\mathfrak I^\Theta_\Lambda$ and a topological model $\mathfrak T^\Theta_\Lambda$, and show that $\mathsf{GLP}^0_\Lambda$ is sound for both of these structures, as well as complete, provided $\Theta$ is large enough. (shrink)

Provability logics are modal or polymodal systems designed for modeling the behavior of Gödel’s provability predicate and its natural extensions. If Λ is any ordinal, the Gödel-Löb calculus GLPΛ contains one modality [λ] for each λ < Λ, representing provability predicates of increasing strength. GLPω has no non-trivial Kripke frames, but it is sound and complete for its topological semantics, as was shown by Icard for the variable-free fragment and more recently by Beklemishev and Gabelaia for the full logic. In (...) this paper we generalize Beklemishev and Gabelaia’s result to GLPΛ for countable Λ. We also introduce provability ambiances, which are topological models where valuations of formulas are restricted. With this we show completeness of GLPΛ for the class of provability ambiances based on Icard polytopologies. (shrink)

We prove a topological completeness theorem for the modal logic $$\textsf{GLP}$$ GLP containing operators $$\{\langle \xi \rangle :\xi \in \textsf{Ord}\}$$ { ⟨ ξ ⟩ : ξ ∈ Ord } intended to capture a wellordered sequence of consistency operators increasing in strength. More specifically, we prove that, given a tall-enough scattered space X, any sentence $$\phi $$ ϕ consistent with $$\textsf{GLP}$$ GLP can be satisfied on a polytopological space based on finitely many Icard topologies constructed over X and corresponding to the (...) finitely many modalities that occur in $$\phi $$ ϕ. (shrink)

In this paper a new trajectory-based representation to non-relativistic quantum mechanics is formulated. This is ahieved by generalizing the notion of Lagrangian path which lies at the heart of the deBroglie-Bohm “ pilot-wave” interpretation. In particular, it is shown that each LP can be replaced with a statistical ensemble formed by an infinite family of stochastic curves, referred to as generalized Lagrangian paths. This permits the introduction of a new parametric representation of the Schrödinger equation, denoted as GLP-parametrization, and of (...) the associated quantum hydrodynamic equations. The remarkable aspect of the GLP approach presented here is that it realizes at the same time also a new solution method for the N-body Schrödinger equation. As an application, Gaussian-like particular solutions for the quantum probability density function are considered, which are proved to be dynamically consistent. For them, the Schrödinger equation is reduced to a single Hamilton–Jacobi evolution equation. Particular solutions of this type are explicitly constructed, which include the case of free particles occurring in 1- or N-body quantum systems as well as the dynamics in the presence of suitable potential forces. In all these cases the initial Gaussian PDFs are shown to be free of the spreading behavior usually ascribed to quantum wave-packets, in that they exhibit the characteristic feature of remaining at all times spatially-localized. (shrink)

By Solovay’s celebrated completeness result [31] on formal provability we know that the provability logic ${\textbf {GL}}$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result in [22] by considering a polymodal version ${\mathsf {GLP}}$ of ${\textbf {GL}}$ with modalities $[n]$ for each natural number n referring to ever increasing notions of provability. Modern treatments of ${\mathsf {GLP}}$ tend to interpret the $[n]$ provability notion as “provable in (...) a base theory T together with all true $\Pi ^0_n$ formulas as oracles.” In this paper we generalise this interpretation into the transfinite. In order to do so, a main difficulty to overcome is to generalise the syntactical characterisations of the oracle formulas of complexity $\Pi ^0_n$ to the hyper-arithmetical hierarchy. The paper exploits the fact that provability is $\Sigma ^0_1$ complete and that similar results hold for stronger provability notions. As such, the oracle sentences to define provability at level $\alpha $ will recursively be taken to be consistency statements at lower levels: provability through provability whence the name of the paper. The paper proves soundness and completeness for the proposed interpretation for a wide class of theories, namely for any theory that can formalise the recursion described above and that has some further very natural properties. Some remarks are provided on how the recursion can be formalised into second order arithmetic and on lowering the proof-theoretical strength of these systems of second order arithmetic. (shrink)

We consider the well-known provability logic GLP. We prove that the GLP-provability problem for polymodal formulas without variables is PSPACE-complete. For a number n, let L0n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${L^{n}_0}$$\end{document} denote the class of all polymodal variable-free formulas without modalities ⟨n⟩,⟨n+1⟩,...\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\langle n \rangle,\langle n+1\rangle,...}$$\end{document}. We show that, for every number n, the GLP-provability problem for formulas from L0n\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${L^{n}_0}$$\end{document} (...) is in PTIME. (shrink)

Genetic and molecular studies of development in Caenorhabiditis elegans have identified regulators that appear to control pattern formation in the cellularized nematode embryo. Two genes, skn‐1 and pie‐1, are required for specifying the different identities of two sister blastomeres in a 4‐cell embryo, called P2 and EMS. The skn‐1 gene encodes a DNA binding protein that may control blastomere development by regulating transcription in EMS and its descendants. ABa and ABp, the other two sisters in a 4‐cell embryo, are influenced (...) to develop differently by cell signaling events that require the two genes apx‐1 and glp‐1. In this review, I summarize evidence that some or all of these genes may encode embryonic determinants of blastomere identity. (shrink)

The mechanisms used to establish embryonic polarity are still largely unknown. A recent paper(1) describes the expression pattern of the gene glp‐1, which is required for induction events during development of the nematode Caenorhabditis elegans. Although glp‐1 RNA is found throughout the early embryo, Glp‐1 protein is only expressed in anterior cells. This negative translational regulation in posterior cells is shown to be mediated through sequences in the glp‐1 3′ untranslated region (3′UTR). Thus in nematodes, as in Drosophila, translational repression (...) is one mechanism used to establish the embryonic anterior‐posterior axis. (shrink)

Cell communication is crucial for many aspects of growth and differentiation during the development of the nematode Caenorhabditis elegans. Two genes, glp‐1 and lin‐12, mediate a number of known cell–cell interactions. Genetic and molecular analyses of these two genes lead to the conclusion that they are structurally and functionally related. We summarize these studies as well as those involving the identification of other genes that interact with glp‐1 and / or lin‐12.

The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for the theory Primitive (...) Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic by capitalizing on the well-studied relationship between PRA and I$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM. (shrink)

Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories: iterate adding consistency of some weak base theory until you “hit” the target theory. Turing progressions based on n-consistency give rise to a \ proof-theoretic ordinal \ also denoted \. As such, to each theory U we can assign the sequence of corresponding \ ordinals \. We call this sequence a Turing-Taylor expansion or spectrum of a theory. In this paper, we relate Turing-Taylor expansions of sub-theories (...) of Peano Arithmetic to Ignatiev’s universal model for the closed fragment of the polymodal provability logic \. In particular, we observe that each point in the Ignatiev model can be seen as Turing-Taylor expansions of formal mathematical theories. Moreover, each sub-theory of Peano Arithmetic that allows for a Turing-Taylor expansion will define a unique point in Ignatiev’s model. (shrink)