Pré-Publication, Document De Travail Année : 2025

Projective Unification in Bi-Intuitionistic Logic

Résumé

The bi-intuitionistic propositional calculus bi-IPC is the natural symmetric extension of the intuitionistic logic IPC. We provide both an axiomatic and semantic characterization of the consistent axiomatic extensions of bi-IPC which admit projective unification. They are exactly those which contain a theorem of the form (¬ ∼)n p → (¬ ∼)^{n+1} p, for some n ∈ N -or, equivalently, which are valid on Kripke frames of n-bounded zigzag depth, a simple order-theoretic condition. We also prove that bi-IPC does not have a unitary unification type by showing that while the formula ¬ ∼p → (¬ ∼) p is a unifiable formula in bi-IPC, it cannot have a most general unifier.
Fichier principal
Vignette du fichier
unification-biIPC-2.pdf (509) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-04957607 , version 1 (19-02-2025)

Licence

Identifiants

  • HAL Id : hal-04957607 , version 1

Citer

Damiano Fornasiere, Quentin Gougeon, Miguel Martins. Projective Unification in Bi-Intuitionistic Logic. 2025. ⟨hal-04957607⟩
0 Consultations
0 Téléchargements

Partager

More