Proof-Theoretic Foundations of Intensional Semantics. Counterfactuals of belief and knowledge
Final Report Abstract
Intensional contexts (e.g., belief contexts) are context which may give rise to substitution failures. For example, we are reluctant to conclude from the premisses `Mary believes that Superman can fly' and `Superman is Clark Kent' that `Mary believes that Clark Kent can fly', since Mary may not know that the second premiss holds. The logic and semantics of intensional constructions involving belief or other intensional operators are nowadays usually studied using tools and techniques from model-theoretic semantics. Such approaches typically appeal to truth conditions, semantic ontology, and classical logic. The aim of the project was to contribute to the development of a proof-theoretic semantics for intensional constructions that is in agreement with intuitionistic principles of reasoning. Roughly, in proof-theoretic semantics, unlike in model-theoretic semantics, meaning is explained in terms of derivations and proofs rather than in terms of truth conditions. The work carried out in the project pursues the development of proof-theoretic semantics for intensional constructions further by extending the framework of subatomic natural deduction proposed by the author in earlier work; rather than, as originally intended, his constructive type theoretic formalism; to belief and knowledge constructions which involve multiple agents (agent-relative subatomic systems, agent-labelled rules; sharpening the profile of subatomic proof theory (subatomic operators; subatomic derivation failure), and exploring a first path to giving a proof-theoretic semantics for counterfactuals (modes of assumptions relativized to a reference proof system). The proposed subatomic natural deduction systems enjoy proof-theoretic properties which are central to proof-theoretic semantics (normalization, subformula property) and are all in agreement both with an intuitionistic conception of epistemology and an inferentialist perspective on semantics. Importantly, the systems are semantically autarkic, they do not depend on results which make use of reasoning with model-theoretic structures, and the proof-theoretic semantics based on the systems does not make use of semantic ontology (e.g., possible worlds). Applications to relatively complex and philosophically significant constructions (e.g., intentional identity, counterpossibles, the Trinity) and puzzles (e.g., the three wise men) can be taken to suggest that the systems are quite versatile. It is hoped that the proof-theoretic frameworks described in the papers reporting the results of the project can be developed further in future work so as to contribute to our understanding of intensional phenomena and counterfactual inference from a proof-theoretic perspective.
Publications
- (2021). Intuitionistic multi-agent subatomic natural deduction for belief and knowledge, Journal of Logic and Computation 31(3): 704-770. Special issue on External and Internal Calculi for Non-Classical Logics edited by A. Ciabattoni et al.
Więckowski, B.
(See online at https://doi.org/10.1093/logcom/exab013) - (2021). Subatomic negation, Journal of Logic, Language and Information, 30(1): 207-262
Więckowski, B.
(See online at https://doi.org/10.1007/s10849-020-09325-4)
