An anti-realist theory of meaning suitable for both logical and proper axioms is investigated. As opposed to other anti-realist accounts, like Dummett-Prawitz verificationism, the standard framework of classical logic is not called into question. In particular, semantical features are not limited solely to inferential ones, but also computational aspects play an essential role in the process of determination of meaning. In order to deal with such computational aspects, a relaxation of syntax is shown to be 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 have been replaced by geometrical configurations. (shrink)

We introduce a graph-theoretical representation of proofs of multiplicative linear logic which yields both a denotational semantics and a notion of truth. For this, we use a locative approach related to game semantics and the Danos–Regnier interpretation of GoI operators as paths in proof nets . We show how we can retrieve from this locative framework both a categorical semantics for Multiplicative Linear Logic with distinct units and a notion of truth. Moreover, we show how a restricted version of our (...) model can be reformulated in the exact same terms as Girardʼs geometry of interaction . This shows that this restriction of our framework gives a combinatorial approach to J.-Y. Girardʼs geometry of interaction in the hyperfinite factor, while using only graph-theoretical notions. (shrink)