ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS

✨ Summary

Martin-Löf develops a constructive, proof-theoretic account of logic centered on the distinction between propositions and judgements. A proposition is understood through the conditions that count as its verification, while a judgement records an act of knowledge or understanding. A proof is therefore not merely a formal sequence of formulas: it is an act that makes a judgement evident. On this account, truth is identified with verifiability, and evidence is inherently related to a knowing subject.

The paper gives a systematic semantic explanation of the logical constants. The meaning of implication is explained through hypothetical proof; conjunction requires proofs of both components; disjunction requires a proof of one component together with information about which component was verified; falsehood has no possible verification; universal quantification requires a uniform proof for arbitrary instances; and existential quantification requires a witness together with a proof for the witnessed instance. The introduction rules express how propositions are verified, while the elimination rules are justified by showing how an existing verification can be put into practice. Martin-Löf also distinguishes logical consequence from implication and treats formation rules as genuine rules of inference because judgements such as “A is a proposition” are themselves knowledge claims.

The paper argues that consistency and normalization should be understood semantically rather than solely through metamathematical manipulation of uninterpreted proof figures: when proof rules are endowed with their intended meaning, the impossibility of verifying falsehood and the reduction of proofs toward introductory form become conceptually visible.

The work became an important contribution to the development of proof-theoretic semantics, an approach that explains the meanings of logical constants in terms of proofs and inferential rules rather than truth conditions. Later surveys identify Martin-Löf, alongside Gentzen, Prawitz, and Dummett, as a central figure in this tradition, and describe his account as influential in subsequent discussions of inferential meaning, harmony, logical consequence, and constructive type theory. (plato.stanford.edu) The paper is also routinely cited in literature examining the inferential characterization of logical constants and the relationship between proof-theoretic semantics and type theory. (sciencedirect.com)

The available references document substantial influence on later logical and philosophical research. They do not establish a direct industry adoption attributable specifically to this paper, although related Martin-Löf type-theoretic ideas have contributed to the foundations of computer-assisted proof and functional programming.