A Functional Calculus of First Order Based on Strict Implication (Un calcul fonctionnel du premier ordre fondé sur l’implication stricte)

Introduction

Ruth C. Barcan publia ce court article technique dans le Journal of Symbolic Logic en 1946, l’année où elle acheva son doctorat à Yale. Il ajoute des quantificateurs (« pour tout x », « il existe un x ») au système S2 d’implication stricte de C. I. Lewis – une logique où un énoncé n’en implique strictement un autre que s’il est impossible que le premier soit vrai et le second faux – et présente ainsi le premier système formel publié de logique modale quantifiée (« Modalities and Quantification » de Carnap, traduction propre : « Modalités et quantification », parut dans le même volume de la revue quelques mois plus tard). Parmi ses théorèmes figure ce qui est devenu la formule de Barcan : s’il est possible que quelque chose soit F, alors il y a quelque chose qui est possiblement F (◇∃xFx → ∃x◇Fx). Ses conséquences pour la question de savoir si des choses simplement possibles existent sont encore débattues.

Autres œuvres de Ruth Barcan Marcus

• 1961Modalities and Intensional Languages (Modalités et langages intensionnels)