A graphical approach to intuitionistic propositional logic is presented. The system GrIn is a deep inference system and it is formulated in terms of Peirce’s existential graphs. GrIn is shown to be sound and complete with respect to the class of all Heyting algebras. Moreover, the system GrIn is shown to be equivalent to the Gentzen sequent calculus G3ip via translations between intuitionistic graphs and intuitionistic formulas. We also discuss the intuitionistic interpretation of logical constants proposed by this graphical approach.
Peirce’s linear versions of the language of his Existential Graphs (EGs), presented in 1902, are examined. Differences between linear and non-linear languages are explained by permutational invariance and type- vs. occurrence-referentiality: Standard EGs are permutationally invariant with respect to linear EGs, while the Beta part of the system, which corresponds to first-order quantificational theory with identity, is occurrence-referential. However, occurrence-referentiality of Beta graphs constitutes a defect of expressivity: since the meaning of a quantifier is inextricably connected to the meaning of the sign of identity, certain complex assertions cannot be expressed in the language of Beta graphs without a new extension of its standard notation.
The received notion of axiomatic method stemming from Hilbert is not fully adequate to the recent successful practice of axiomatizing mathematical theories. The axiomatic architecture of Homotopy type theory (HoTT) does not ft the pattern of formal axiomatic theory in the standard sense of the word. However this theory falls under a more general and in some respects more traditional notion of axiomatic theory, which I call after Hilbert and Bernays constructive and demonstrate using the Classical example of the First Book of Euclid’s Elements. I also argue that HoTT is not unique in the respect but represents a wider trend in today’s mathematics, which also includes Topos theory and some other developments. On the basis of these modern and ancient examples I claim that the received semantic oriented formal axiomatic method defended recently by Hintikka is not self-sustained but requires a support of constructive method.
Finally, I provide an epistemological argument showing that the constructive axi omatic method is more apt to present scientifc theories than the received axiomatic method.
The pragmatic notion of assertion has an important inferential role in logic. There are also many notational forms to express assertions in logical systems. This paper reviews, compares and analyses languages with signs for assertions, including explicit signs such as Frege’s and Dalla Pozza’s logical systems and implicit signs with no specific sign for assertion, such as Peirce’s algebraic and graphical logics and the recent modification of the latter termed Assertive Graphs. We identify and discuss the main ‘points’ of these notations on the logical representation of assertions, and evaluate their systems from the perspective of the philosophy of logical notations. Pragmatic assertions turn out to be useful in providing intended interpretations of a variety of logical systems.
Nous proposons une logique épistémique quadrivalente AR4 , sur la base d’une sémantique qui définit les valeurs des énoncés en termes de réponses à des questions posées. Les propriétés de ce système sont exposées et interprétées dans le cadre d’une épistémologie sociale ; celle-ci comporte une variété d’agents, ainsi qu’un ensemble de relations entre eux. Les notions de justification (forte et faible) et de quasi-vérité sont également revues à la lumière de ce système logique.