pith. sign in

arxiv: 2604.22042 · v1 · submitted 2026-04-23 · 💻 cs.LO

Probabilistic Epistemic Dynamic Agentive Logic

Shay Allen Logan This is my paper

Pith reviewed 2026-05-08 13:35 UTC · model grok-4.3

classification 💻 cs.LO
keywords probabilistic epistemic logicpropositional dynamic logicprogram verificationspecification checkingHilbert systemsoundness and completenessinfinitary rules
0
0 comments X

The pith

PEDAL layers probability measures over propositional dynamic logic models to represent an agent's epistemic state while checking program specifications.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces PEDAL as a new logic that combines probabilistic reasoning with the dynamic aspects of programs to model how an agent forms beliefs about whether a program meets its specification. It constructs this semantics by placing probability measures directly on the possible valuations of programs within standard propositional dynamic logic models. This approach lets the logic express uncertain epistemic attitudes in terms of program execution. A Hilbert-style proof system with one infinitary rule is shown to be sound and complete for the resulting semantics. The work closes by outlining ways to avoid the technical difficulties that arise from the infinitary rule.

Core claim

PEDAL is a probabilistic epistemic logic built on top of PDL-models in which probability measures are defined on the set of possible program valuations. This semantic setup captures the epistemic state of an agent engaged in checking whether a program meets its specification. A Hilbert system containing one infinitary rule is proved sound and complete with respect to these models.

What carries the argument

Probability measures defined on the set of possible program valuations within an otherwise standard PDL-model, which supply the semantics for the probabilistic epistemic operators.

Load-bearing premise

Probability measures placed on program valuations in PDL models are sufficient to represent an agent's epistemic state during specification checking without additional semantic constraints.

What would settle it

A specific program, specification, and set of valuations where the probability assigned by the measures fails to match the degree of belief an agent would actually hold about whether the specification holds.

read the original abstract

I introduce PEDAL -- a probabilistic epistemic logic meant to capture, in propositional dynamic terms, the epistemic state of an agent engaged in checking whether a program meets its specification. Semantically, PEDAL is built `on top of' PDL and uses probability measures defined on the set of possible program valuations of an otherwise-specified PDL-model. A Hilbert system with one infinitary rule is provided and proved to be sound and complete. Near the end, I discuss possible ways to circumvent infinitary proof difficulties.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces PEDAL, a probabilistic epistemic dynamic agentive logic extending PDL. Semantics are defined by layering probability measures over the set of program valuations in a PDL-model to capture an agent's epistemic state when checking whether a program meets its specification. A Hilbert-style system containing exactly one infinitary rule is presented, with claims that it is sound and complete; the paper closes by discussing possible ways to circumvent difficulties arising from the infinitary rule.

Significance. If the soundness and completeness results hold, the work supplies a formal system integrating dynamic program reasoning with probabilistic epistemic operators, which could support applications in program verification under uncertainty. The explicit inclusion and discussion of the infinitary rule, together with alternatives, is a constructive feature that aligns with standard practice in epistemic logics.

major comments (2)
  1. [Section on completeness proof] The completeness proof (centered on the infinitary rule) does not supply a sufficiently detailed construction of the canonical model that preserves the probability measures defined on program valuations; without this, it is unclear whether the semantic-to-syntactic correspondence holds for formulas involving the new probabilistic operators.
  2. [Semantics section] The semantic clause defining probability measures on the set of possible program valuations leaves open how these measures are required to interact with the dynamic modalities of the underlying PDL-model; additional constraints or invariance conditions appear necessary to ensure the measures adequately represent the agent's epistemic state.
minor comments (2)
  1. [Abstract] The abstract could briefly indicate the form of the infinitary rule to give readers an immediate sense of the technical machinery.
  2. [Preliminaries] Notation for the probability operators and the program valuations could be introduced with a small example to improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and constructive feedback on our manuscript introducing PEDAL. We address each major comment below and have prepared revisions to strengthen the presentation of the semantics and completeness proof.

read point-by-point responses

  1. Referee: [Section on completeness proof] The completeness proof (centered on the infinitary rule) does not supply a sufficiently detailed construction of the canonical model that preserves the probability measures defined on program valuations; without this, it is unclear whether the semantic-to-syntactic correspondence holds for formulas involving the new probabilistic operators.

    Authors: We agree that the canonical model construction merits additional explicit steps to clarify preservation of the probability measures. In the revised manuscript we will expand the completeness proof with a more detailed inductive construction of the canonical model, including how the Lindenbaum extension respects the infinitary rule and how probability measures on program valuations are lifted to the canonical structure while maintaining the required semantic-to-syntactic correspondence for the probabilistic operators. revision: yes

  2. Referee: [Semantics section] The semantic clause defining probability measures on the set of possible program valuations leaves open how these measures are required to interact with the dynamic modalities of the underlying PDL-model; additional constraints or invariance conditions appear necessary to ensure the measures adequately represent the agent's epistemic state.

    Authors: The layering of probability measures over program valuations is intended to be compatible with the underlying PDL semantics by construction, as valuations are drawn from the PDL-model. Nevertheless, we acknowledge that the interaction could be stated more explicitly. In the revised semantics section we will add a short invariance clause requiring that the probability measures remain stable under the accessibility relations induced by atomic programs, thereby ensuring consistent representation of the agent's epistemic state across dynamic transitions. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines PEDAL by layering probability measures over the program valuations of a standard PDL-model and then supplies an independent Hilbert system (with one explicit infinitary rule) whose soundness and completeness are proved directly from those semantics. No equation reduces a claimed result to a fitted parameter, no prediction is obtained by renaming an input, and no load-bearing premise rests on a self-citation whose content is itself unverified. The construction is a standard, self-contained definitional extension of PDL, with the infinitary rule and its handling discussed openly rather than smuggled in.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on extending PDL semantics with probability measures and adding an infinitary rule to the proof system; these are introduced without independent empirical grounding beyond the stated soundness and completeness.

axioms (2)
  • domain assumption PEDAL semantics are constructed on top of standard PDL models by adding probability measures over program valuations.
    This is the core semantic foundation stated in the abstract for defining the logic.
  • ad hoc to paper A Hilbert-style system with exactly one infinitary rule is sufficient for soundness and completeness.
    The choice and form of the infinitary rule is specific to this paper's axiomatization.

pith-pipeline@v0.9.0 · 5361 in / 1381 out tokens · 60650 ms · 2026-05-08T13:35:18.343831+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

8 extracted references · 8 canonical work pages

  1. [1]

    Information and computation112(1), 1–36 (1994)

    Abadi, M., Halpern, J.Y.: Decidability and expressiveness for first-order logics of probability. Information and computation112(1), 1–36 (1994)

    work page 1994

  2. [2]

    Studia Logica46(4), 383–393 (1987)

    Fattorosi-Barnaba, M., Amati, G.: Modal operators with probabilistic interpreta- tions, i. Studia Logica46(4), 383–393 (1987)

    work page 1987

  3. [3]

    Jour- nal of computer and system sciences18(2), 194–211 (1979)

    Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Jour- nal of computer and system sciences18(2), 194–211 (1979)

    work page 1979

  4. [4]

    MIT Press (2000)

    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)

    work page 2000

  5. [5]

    Theoretical computer science14(1), 113–118 (1981)

    Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theoretical computer science14(1), 113–118 (1981)

    work page 1981

  6. [6]

    Springer (2016)

    Ognjanović, Z., Rašković, M., Marković, Z.: Probability Logics: Probability-Based Formalization of Uncertain Reasoning. Springer (2016)

    work page 2016

  7. [7]

    Analysis64(2), 113–119 (2004)

    Read, S.: Identity and harmony. Analysis64(2), 113–119 (2004)

    work page 2004

  8. [8]

    The Review of Symbolic Logic9(2), 408–420 (2016)

    Read, S.: Harmonic inferentialism and the logic of identity. The Review of Symbolic Logic9(2), 408–420 (2016)

    work page 2016