A Constructive Type-Theoretical Formalism for the Interpretation of Subatomically Sensitive Natural Language Constructions

作者：Wieckowski Bartosz^*

来源：Studia Logica, 2012, 100(4): 815-853.

DOI：10.1007/s11225-012-9431-x

• Constructive type theory
• Proof-theoretic semantics of natural language
• Subatomic semantics
• Type-theoretical grammar

The analysis of atomic sentences and their subatomic components poses a special problem for proof-theoretic approaches to natural language semantics, as it is far from clear how their semantics could be explained by means of proofs rather than denotations. The paper develops a proof-theoretic semantics for a fragment of English within a type-theoretical formalism that combines subatomic systems for natural deduction [20] with constructive (or Martin-Lof) type theory [8, 9] by stating rules for the formation, introduction, elimination and equality of atomic propositions understood as types (or sets) of subatomic proof-objects. The formalism is extended with dependent types to admit an interpretation of non-atomic sentences. The paper concludes with applications to natural language including internally nested proper names, anaphoric pronouns, simple identity sentences, and intensional transitive verbs.

• 出版日期2012-8