?
Two “Styles” of axiomatization: Rules versus Axioms. A Modern Perspective.
In a Hilbert-style non-logical axiomatic theory the semantics of logical symbols is rigidly
fixed, while the interpretation of non-logical symbols usually varies giving rise to different
models of the given theory. All non-logical content of such a theory is comprised in its
non-logical axioms (e.g., axioms of ZF) while rules, which generate from these axioms new
theorems, belong to the logical part of the theory (aka underlying logic).
An alternative approach to axiomatization due to Gentzen amounts to a presentation of
formal calculi in the form of systems of rules without axioms. Gentzen did not try to extend
his approach to non-logical theories by considering specific non-logical rules as a replacement
for non-logical axioms. However the more recent work in Univalent Foundations of
Mathematics [2] suggests that the Gentzen-style rule-based approach to formal presentation
of theories may have important applications also outside the pure logic.
Areasonwhy onemay prefer a rule-based formal representation is that it ismore computerfriendly.
This, in particular, motivates the recent work on the constructive justification of
the Univalence Axiom via the introduction of new operations on types and contexts [1].
However this pragmatic argument does not meet the related epistemological worries. What
kind of knowledge may represent a theory having the form of a bare system of rules? Is such
a formof a theory appropriate for representing a knowledge of objective human-independent
reality? How exactly truth features in rule-based non-logical theories?
Using HoTT as a motivating example I provide some answers to these questions and show
that the Gentzen-style rule-based approach provides a viable alternative to the standard
axiomatic approach not only in logic but also in science more generally.