BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Joost J. Joosten

Joost J. Joosten contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
math.LOLogic in Computer ScienceComputation and Language

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
13works
0followers
3topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

13 published item(s)

preprint2026arXiv

Coherency through formalisations of Structured Natural Language, A case study on FRETish

Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Arithmetical and Hyperarithmetical Worm Battles

Japaridze's provability logic $GLP$ has one modality $[n]$ for each natural number and has been used by Beklemishev for a proof theoretic analysis of Peano aritmetic $(PA)$ and related theories. Among other benefits, this analysis yields the so-called Every Worm Dies $(EWD)$ principle, a natural combinatorial statement independent of $PA$. Recently, Beklemishev and Pakhomov have studied notions of provability corresponding to transfinite modalities in $GLP$. We show that indeed the natural transfinite extension of $GLP$ is sound for this interpretation, and yields independent combinatorial principles for the second order theory $ACA$ of arithmetical comprehension with full induction. We also provide restricted versions of $EWD$ related to the fragments $IΣ_n$ of Peano arithmetic. In order to prove the latter, we show that standard Hardy functions majorize their variants based on tree ordinals.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Assuring and critical labels for relations between maximal consistent sets for interpretability logics

The notion of a critical successor [dJV90] has been central to almost all modal completeness proofs in interpretability logics. In this paper we shall work with an alternative notion, that of an assuring successor. As we shall see, this will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so-called full labels and maximal labels.. After a general treatment of assuringness, we shall apply it to obtain certain completeness results. Namely, we give another proof of completeness of ILW w.r.t. ordinary semantics and of ILP w.r.t. generalised semantics.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A new principle in the interpretability logic of all reasonable arithmetical theories

The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper from 2011 revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by ${\textbf{IL}}({\rm All})$. In this paper we present a new principle $\sf R$ in ${\textbf{IL}}({\rm All})$. We show that $\sf R$ does not follow from the logic ${\textbf{IL}}{\sf P_0W^*}$ that contains all previously known principles. This is done by providing a modal incompleteness proof of ${\textbf{IL}}{\sf P_0W^*}$: showing that $\sf R$ follows semantically but not syntactically from ${\textbf{IL}}{\sf P_0W^*}$. Apart from giving the incompleteness proof by elementary methods, we also sketch how to work with so-called Generalized Veltman Semantics as to establish incompleteness. To this extent, a new version of this Generalized Veltman Semantics is defined and studied. Moreover, for the important principles the frame correspondences are calculated. After the modal results it is shown that the new principle $\sf R$ is indeed valid in any arithmetically theory. The proof employs some elementary results on definable cuts in arithmetical theories.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

An overview of Generalised Veltman Semantics

Interpretability logics are endowed with relational semantics à la Kripke: Veltman semantics. For certain applications though, this semantics is not fine-grained enough. Back in 1992, in the research group of de Jongh, the notion of generalised Veltman semantics emerged to obtain certain non-derivability results as was first presented by Verbrugge ([76]). It has turned out that this semantics has various good properties. In particular, in many cases completeness proofs become simpler and the richer semantics will allow for filtration arguments as opposed to regular Veltman semantics. This paper aims to give an overview of results and applications of Generalised Veltman semantics up to the current date.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Hidden variables simulating quantum contextuality increasingly violate the Holevo bound

In this paper from 2011 we approach some questions about quantum contextuality with tools from formal logic. In particular, we consider an experiment associated with the Peres-Mermin square. The language of all possible sequences of outcomes of the experiment is classified in the Chomsky hierarchy and seen to be a regular language. Next, we make the rather evident observation that a finite set of hidden finite valued variables can never account for indeterminism in an ideally isolated repeatable experiment. We see that, when the language of possible outcomes of the experiment is regular, as is the case with the Peres-Mermin square, the amount of binary-valued hidden variables needed to de-randomize the model for all sequences of experiments up to length n grows as bad as it could be: linearly in n. We introduce a very abstract model of machine that simulates nature in a particular sense. A lower-bound on the number of memory states of such machines is proved if they were to simulate the experiment that corresponds to the Peres-Mermin square. Moreover, the proof of this lower bound is seen to scale to a certain generalization of the Peres- Mermin square. For this scaled experiment it is seen that the Holevo bound is violated and that the degree of violation increases uniformly.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Interpretability in PRA

In this paper from 2009 we study IL(PRA), the interpretability logic of PRA. As PRA is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to PRA: IL(PRA) is not ILM or ILP. IL(PRA) does of course contain all the principles known to be part of IL(All), the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of PRA and see what their consequences in the modal logic IL(PRA) are. These properties are reflected in the so-called Beklemishev Principle B, and Zambella's Principle Z, neither of which is a part of IL(All). Both principles and their interrelation are submitted to a modal study. In particular, we prove a frame condition for B. Moreover, we prove that Z follows from a restricted form of B. Finally, we give an overview of the known relationships of IL(PRA) to important other interpetability principles.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Modal Matters in Interpretability Logics

This paper from 2008 is the first in a series of three related papers on modal methods in interpretability logics and applications. In this first paper the foundations are laid for later results. These foundations consist of a thorough treatment of a construction method to obtain modal models. This construction method is used to reprove some known results in the area of interpretability like the modal completeness of the logic ${\textbf{IL}}$. Next, the method is applied to obtain new results: the modal completeness of the logic ${\textbf{IL}}{\sf M_0}$, and modal completeness of ${\textbf{IL}}({\sf W^*})$.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Propositional proof systems and fast consistency provers

A fast consistency prover is a consistent poly-time axiomatized theory that has short proofs of the finite consistency statements of any other poly-time axiomatized theory. Kraj\'ıček and Pudlák proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that ${\sf NP}={\sf coNP}$ implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of an unlikely fast consistency prover and prove that its existence is equivalent to ${\sf NP}={\sf coNP}$. Next it is proved that fast consistency provers do not exist if one considers RE axiomatized theories rather than theories with an axiom set that is recognizable in polynomial time.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Provability and interpretability logics with restricted realizations

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 $Γ$. We make an analogous modification for interpretability logics. This is a paper from 2012. We first studied provability logics with restricted realizations, and show that for various natural candidates of theory T and restriction set $Γ$, where each sentence in $Γ$ has a well understood (meta)-mathematical content in T, 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$Σ_1$. We then study interpretability logics, obtaining some upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely relatively to linear frames. The technique is also applied to yield the non-trivial result that IL(PRA) $\subset$ ILM.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Self Provers and $Σ_1$ Sentences

This paper from 2012 is the second in a series of three papers. All three papers deal with interpretability logics and related matters. In the first paper a construction method was exposed to obtain models of these logics. Using this method, we obtained some completeness results, some already known, and some new. In this paper, we will set the construction method to work to obtain more results. First, the modal completeness of the logic ${\textbf{IL}}({\sf M})$ is proved using the construction method. This is not a new result, but by using our new proof we can obtain new results. Among these new results are some admissible rules for ${\textbf{IL}}({\sf M})$ and ${\textbf{GL}}$. Moreover, the new proof will be used to classify all the essentially $Δ_1$ and also all the essentially $Σ_1$ formulas of ${\textbf{IL}}({\sf M})$. Closely related to essentially $Σ_1$ sentences are the so-called \emph{self provers}. A self-prover is a formula $φ$ which implies its own provability, that is $φ\to \Box φ$. Each formula $φ$ will generate a self prover $φ\wedge \Box φ$. We will use the construction method to characterize those sentences of ${\textbf{GL}}$ that generate a self prover that is trivial in the sense that it is $Σ_1$.

0 citations0 reviewsNo code linkedOpen access