# Russellian Propositional Logic and the BHK Interpretation

## TL;DR

This paper develops a hierarchical propositional logic framework based on Russellian typed languages to interpret the BHK proof hierarchy, introducing new logics and establishing their soundness and completeness.

## Contribution

It introduces hierarchical counterparts of key propositional logics using a typed language with multiple implications, linking syntax to the proof hierarchy in BHK interpretation.

## Key findings

- Defined hierarchical propositional logics for BHK interpretation
- Proved soundness and completeness theorems for these logics
- Showed how different logics model various proof hierarchies

## Abstract

The BHK interpretation interprets propositional statements as descriptions of the world of proofs; a world which is hierarchical in nature. It consists of different layers of the concept of proof; the proofs, the proofs about proofs and so on. To describe this hierarchical world, one approach is the Russellian approach in which we use a typed language to reflect this hierarchical nature in the syntax level. In this case, since the connective responsible for this hierarchical behavior is implication, we will use a typed language equipped with a hierarchy of implications, $\{\rightarrow_n\}_{n=0}^{\infty}$. In fact, using this typed propositional language, we will introduce the hierarchical counterparts of the logics $\mathbf{BPC}$, $\mathbf{EBPC}$, $\mathbf{IPC}$ and $\mathbf{FPL}$ and then by proving their corresponding soundness-completeness theorems with respect to their natural BHK interpretations, we will show how these different logics describe different worlds of proofs embodying different hierarchical behaviors.