On the computational meaning of axioms

Alberto Naibo

Mattia Petrolo

Thomas Seiller

pp. 141-184

in: Juan Redmond, Olga Pombo Martins, Angel Fernández (eds), Epistemology, knowledge and the impact of interaction, Berlin, Springer, 2016

Abstrakt

This paper investigates an anti-realist theory of meaning suitable for both logical and proper axioms. Unlike other anti-realist accounts such as Dummett–Prawitz verificationism, the standard framework of classical logic is not called into question. This account also admits semantic features beyond the inferential ones: computational aspects play an essential role in the determination of meaning. To deal with these computational aspects, a relaxation of syntax is necessary. This leads to a general kind of proof theory, where the objects of study are not typed objects like deductions, but rather untyped ones, in which formulas are replaced by geometrical configurations.