Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses
Faruk Alpay, Baris Basaran
cs.LO
May 4, 2026 · v1
TL;DR
Provides Lean and Alloy companions verifying finite relational lemmas for biprofile deviation logic.
Abstract
Biprofile deviation logic models strategic social choice states as pairs $(R,P)$, where $R$ is the true profile used for welfare comparisons and $P$ is the submitted report profile used by the rule. Coalition modalities replace only the reports of the coalition, and their relations satisfy the fixed law $E_C \circ E_D = E_{C \cup D}$. The paper proves soundness and completeness of $H_{\mathrm{bp}}$ for the abstract frame class $\mathrm{Dev}(N)$, with the reverse-composition midpoint displayed inside the canonical proof. It then separates abstract $\mathrm{Dev}(N)$-components from genuine report-coordinate products by coordinate separation. On the social-choice side, the classical facts supply the source notions; the paper-specific contribution is the audit layer for representation changes: typed manipulation witnesses, a boundary-row theorem for off-domain extensions, and a factor-closure criterion for public deletions. The ancillary material contains the input formats, an executable certificate checker, Lean and Alloy companions for the finite relational lemmas and update patterns, recorded run logs, and checksums.
Problem
Strategic social choice requires comparing a true preference profile with a submitted report profile, but existing modal logics do not cleanly separate these two roles or provide typed audit witnesses for manipulation claims.
Approach
Biprofile deviation logic introduces Kripke states as pairs (R,P) where R is the true profile and P the submitted report. Coalition modalities replace only report coordinates, satisfying E_C compose E_D = E_{C union D}. The paper proves soundness and completeness of a Hilbert system H_bp for the frame class Dev(N), separates abstract frames from genuine coordinate products, and defines an audit layer with typed manipulation witnesses. Lean and Alloy companions verify finite relational lemmas.
Results
The completeness theorem is proved self-contained with an explicit canonical midpoint construction. A coordinate-separation proposition shows abstract Dev(N) components do not recover report coordinates without an extra condition. The audit layer provides a boundary-row theorem for off-domain extensions and a factor-closure criterion for public deletions.
