# HTS-AT: A hierarchical token-semantic audio transformer
for sound classification and detection

###### Abstract

Audio classification is an important task of mapping audio samples into their
corresponding labels. Recently, the transformer model with self-attention
mechanisms has been adopted in this field. However, existing audio
transformers require large GPU memories and long training time, meanwhile
relying on pretrained vision models to achieve high performance, which limits
the model’s scalability in audio tasks. To combat these problems, we introduce
HTS-AT: an audio transformer with a hierarchical structure to reduce the model
size and training time. It is further combined with a token-semantic module to
map final outputs into class featuremaps, thus enabling the model for the
audio event detection (i.e. localization in time). We evaluate HTS-AT on three
datasets of audio classification where it achieves new state-of-the-art (SOTA)
results on AudioSet and ESC-50, and equals the SOTA on Speech Command V2. It
also achieves better performance in event localization than the previous CNN-
based models. Moreover, HTS-AT requires only 35% model parameters and 15%
training time of the previous audio transformer. These results demonstrate the
high performance and high efficiency of HTS-AT.

Index Terms—  Audio Classification, Sound Event Detection, Transformer, Token-
Semantic Module

##  1 Introduction

Audio classification is an audio retrieval task which aims to learn a mapping
from audio samples to their corresponding labels. Depending on the audio
categories, it involves sound event detection [1], music instrument
classification [2], among others. It establishes a foundation for many
downstream applications including music recommendation [3], keyword spotting
[4], music generation [5, 6], etc.

With burgeoning research in the field of artificial intelligence, we have seen
significant promising progress in audio classification. For data collections,
many datasets with different types of audio (e.g. AudioSet [7], ESC-50 [8],
Speech Command [4], etc.) provide platforms for the training and evaluation of
models on different subtasks. For the model design, the audio classification
task is thriving based on neural-network-based models. Convolutional neural
networks (CNNs) have been widely used in this field, such as DeepResNet [9],
TALNet [10], PANN [11], and PSLA [12]. These models leverage CNN to capture
features on the audio spectrogram, and further improve their performance
through the design of the depth and breadth of the network. Recently, by
introducing the transformer structure [13] into audio classification, the
audio spectrogram transformer (AST) [14] further achieves the best performance
through the self-attention mechanism and the pretrained model from computer
vision. In this paper, we take a further step on a transformer-based audio
classification model by first analyzing remaining problems in the AST.

Fig. 1: The model architecture of HTS-AT.

First, since the transformer takes the audio spectrogram as a complete
sequential data, AST takes a long time to train and consumes large GPU
memories. In practice, it takes about one week to train on the full AudioSet
with four 12GB GPUs. One method to boost training speed is to use the ImageNet
[15] pretrained model in computer vision. However, this also limits the model
to those pretrained hyperparameters, which reduces its scalability in more
audio tasks. Indeed, we find that without pretraining, AST can only achieve
the baseline performance (mAP=0.366 on AudioSet), which raises our attention
to its learning efficiency on the audio data. Second, AST uses a class-token
(CLS) to predict labels, making it unable to predict the start and end time of
events in audio samples. Most CNN-based models naturally support the frame-
level localization by empirically taking the penultimate layer’s output as a
event presence map. This inspires us to design a module that makes every
output token of an audio transformer aware of the semantic meaning of events
(i.e. a token-semantic module [16]) for supporting more audio tasks (e.g.
sound event detection and localization).

In this paper, we propose HTS-AT111https://github.com/RetroCirce/HTS-Audio-
Transformer, a hierarchical audio transformer with a token-semantic module for
audio classification. Our contributions of HTS-AT can be listed as:

  * •

HTS-AT achieves or equals SOTAs on AudioSet and ESC-50, and Speech Command V2
datasets. Moreover, the model without pretraining can still achieve the
performance that is only 1%-2% lower than the best results.

  * •

HTS-AT takes fewer parameters (31M vs. 87M), fewer GPU memories, and less
training time (80 hrs vs. 600 hrs) than AST’s to achieve the best performance.

  * •

HTS-AT further enables the audio transformer to produce the localization
results of event only with weakly-labeled data. And it achieves a better
performance than the previous CNN-based model.

##  2 Proposed Model

###  2.1 Hierarchical Transformer with Window Attention

A typical transformer structure consumes lots of GPU memories and training
time, because the length of input tokens is too long and remains unchanged in
all transformer blocks from beginning to end. As a result, the machine saves
the output and its gradient of each block via large GPU memories, and spends
much calculation time maintaining a large global self-attention matrix. To
combat these problems, as depicted in Figure 1, we propose two key designs: a
hierarchical transformer structure and a window attention mechanism.

####  2.1.1 Encode the Audio Spectrogram

In the left of Figure 1, an audio mel-spectrogram is cut into different patch
tokens with a Patch-Embed CNN of kernel size $(P\times P)$ and sent into the
transformer in order. Different from images, the width and the height of an
audio mel-spectrogram denote different information (i.e. the time and the
frequency bin). And the length of time is usually much longer than that of
frequency bins. Therefore, to better capture the relationship among frequency
bins of the same time frame, we first split the mel-spectrogram into patch
windows $w_{1},w_{2},...,w_{n}$ and then split the patches inside each window.
The order of tokens follows time$\to$frequency$\to$window as shown in Figure
1. With this order, patches with different frequency bins at the same time
frame will be organized adjacently in the input sequence.

####  2.1.2 Patch-Merge and Window Attention

In the middle of Figure 1, the patch tokens are sent into several groups of
transformer-encoder blocks. At the end of each group, we implement a Patch-
Merge layer [17] to reduce the sequence size. This merge operation is applied
by first reshaping the sequence to its original 2D map
$(\frac{T}{P}\times\frac{F}{P},D)$, where $D$ is the latent state dimension.
Then it merges adjacent patches as $(\frac{T}{2P}\times\frac{F}{2P},4D)$ and
finally applies a linear layer to reduce the latent dimension to
$(\frac{T}{2P}\times\frac{F}{2P},2D)$. As illustrated in Figure 1, the shape
of the patch tokens is reduced by 8 times from
$(\frac{T}{P}\times\frac{F}{P},D)$ to $(\frac{T}{8P}\times\frac{F}{8P},8D)$
after 4 network groups, thus the GPU memory consumption is reduced
exponentially after each group.

For each transformer block inside the group, we adopt a window attention
mechanism to reduce the calculation. As shown in different color boxes in the
middle right of Figure 1, we first split the patch tokens (in 2D format) into
non-overlapping $(M\times M)$ attention windows $aw_{1},aw_{2},...,aw_{k}$.
Then we only compute the attention matrix inside each $M\times M$ attention
window. As a result, we have $k$ window attention (WA) matrices instead of a
whole global attention (GA) matrix. The computational complexities of these
two mechanisms in one transformer block for $f\times t$ audio patch tokens
with the initial latent dimension $D$ are:

GA: $\displaystyle{\cal O}(ftD^{2}+(ft)^{2}D)$ (1) WA: $\displaystyle{\cal
O}(ftD^{2}+M^{2}ftD)$ (2)

where the window attention reduces the second complexity term by
$(\frac{ft}{M^{2}})$ times. For audio patch tokens in a time-frequency-window
order, each window attention module will calculate the relation in a certain
range of continuous frequency bins and time frames. As the network goes
deeper, the Patch-Merge layer will merge adjacent windows, thus the attention
relation is calculated in a larger space. In the code implementation, we use
the swin transformer block with a shifted window attention [17], a more
efficient window attention mechanism. This also helps us to use the swin
transformer pretrained vision model in the experiment stage.

###  2.2 Token Semantic Module

The existing AST uses a class-token (CLS) to predict the classification label,
which limits it from further indicating the start and end times of events as
realized in CNN-based models. In the final layer output, each token contains
information about its corresponding time frames and frequency bins. We expect
to convert tokens into activation maps for each label-class (i.e. aware of
semantic meaning [16]). For strong-label datasets, we can let the model
directly calculate the loss in specific time ranges. For weakly-labeled
datasets, we can leverage the transformer to locate via its strong capability
to capture the relation. In HTS-AT, as shown in the right of Figure 1, we
modify the output structure by adding a token-semantic CNN layer after the
final transformer block. It has a kernel size $(3,\frac{F}{8P})$ and a padding
size $(1,0)$ to integrate all frequency bins and map the channel size $8D$
into the event classes $C$. The output $(\frac{T}{8P},C)$ is regarded as a
event presence map. Finally, we average the featuremap as the final vector
$(1,C)$ to compute the binary cross-entropy loss with the groundtruth labels.
Apart from the localization functionality, we also expect the token-semantic
module to improve the classification performance, as it considers the final
output by directly grouping all tokens .

##  3 Experiments

In this section, we evaluate the performance of HTS-AT in four datasets: the
event classification on AudioSet [7], ESC-50 [8]; the keyword spotting on
Speech Command V2 [4]; and additionally, the event detection on DESED [18].

Model | Pretrain | #Params. | mAP | Ensemble-mAP
---|---|---|---|---
Baseline [7] | ✗ | 2.6M | 0.314 | -
DeepRes [9] | ✗ | 26M | 0.392 | -
PANN [11] | ✗ | 81M | 0.434 | -
PSLAP [12] | ✓ | 13.6M | 0.444 | 0.474
AST [14] | ✗ | 87M | 0.366 | -
ASTP [14] | ✓ | 87M | 0.459 | 0.475 (0.485222AST provides a second bigger ensemble result by using models with different patch settings, which is partially comparable with our settings.)
HTS-ATH | ✗ | 28.8M | 0.440 | -
HTS-ATHC | ✗ | 31M | 0.453 | -
HTS-ATHCP | ✓ | 31M | 0.471 | 0.487

Table 1: The mAP results on AudioSet evaluation set.

###  3.1 Event Classification on AudioSet

####  3.1.1 Dataset and Training Detail

The AudioSet contains over two million 10-sec audio samples labeled with 527
sound event classes. In this paper, we follow the same training pipeline in
[11, 12, 14] by using the full-train set (2M samples) to train our model and
evaluating it on the evaluation set (22K samples). All samples are converted
to mono as 1 channel by 32kHz sampling rate. We use 1024 window size, 320 hop
size, and 64 mel-bins to compute STFTs and mel-spectrograms. As a result, the
shape of the mel-spectrogram is $(1024,64)$ as we pad each 1000-frame (10-sec)
sample with 24 zero-frames ($T$=1024, $F$=64). The shape of the output
featuremap is $(1024,527)$ ($C$=527). The patch size is $4\times 4$, the patch
window length is 256 frames, and the attention window size is $8\times 8$.
Since 8 is divisible by 64, the attention window in the first layer will not
span two frames with a large time difference. The latent dimension size is
$D$=96 and the final output latent dimension is $8D$=768, which is consistent
to AST. Finally, we set 4 network groups with 2, 2, 6, 2 swin-transformer
blocks respectively.

We follow [11, 12] to use the balance sampler, $\alpha=0.5$ mix-up [19],
spectrogram masking [20] with time-mask=128 frames and frequency-mask=16 bins,
and weight averaging. The HTS-AT is implemented in Pytorch and trained via the
AdamW optimizer ($\beta_{1}$=0.9, $\beta_{2}$=0.999, eps=1e-8, decay=0.05)
with a batch size of 128 ($32\times 4$) in 4 NVIDIA Tesla V-100 GPUs. We apply
a warm-up schedule by setting the learning rate as 0.05, 0.1, 0.2 in the first
three epochs, then the learning rate is halved every ten epochs until it
returns to 0.05. We use the mean average precision (mAP) to evaluate the
classification performance.

Model | ESC-50 Acc.(%) | Model | SCV2 Acc.(%)
---|---|---|---
PANN [11] | 90.5 | RES-15 [21] | 97.0
AST [14] | 95.6 $\pm$ 0.4 | AST [14] | 98.1 $\pm$ 0.05
ERANN [22] | 96.1 | KWT-2 [23] | 97.3 $\pm$ 0.03
HTS-AT | 97.0 $\pm$ 0.2 | HTS-AT | 98.0 $\pm$ 0.03

Table 2: The accuracy score results on ESC-50 dataset and Speech Command V2
(SCV2).

Model | Alarm | Blender | Cat | Dishes | Dog | Shaver | Frying | Water | Speech | Cleaner | Average
---|---|---|---|---|---|---|---|---|---|---|---
PANN [11] | 34.3 | 42.4 | 36.3 | 17.6 | 35.8 | 23.8 | 9.3 | 30.6 | 69.7 | 51.0 | 35.1
HTS-AT | 48.6 | 52.9 | 67.7 | 25.0 | 48.0 | 42.9 | 60.3 | 43.0 | 46.8 | 49.1 | 48.4
HTS-AT - Ensemble | 47.5 | 55.1 | 72.4 | 30.9 | 49.7 | 41.9 | 63.2 | 44.3 | 51.3 | 50.6 | 50.7
Zheng et al.* [24] | 41.4 | 54.1 | 72.4 | 29.4 | 47.8 | 61.01 | 49.2 | 33.7 | 69.5 | 65.5 | 52.4
Kim et al.* [24] | 34.7 | 59.8 | 71.6 | 40.4 | 47.3 | 26.2 | 61.8 | 32.8 | 64.9 | 66.7 | 50.6
Lu et al.* [24] | 37.1 | 41.4 | 62.5 | 40.6 | 39.7 | 46.5 | 46.5 | 34.5 | 54.5 | 46.9 | 45.0

Table 3: The event-based F1-scores of each class on the DESED test set. Models
with * are from DCASE 2021 [24], which are partial references since they use
extra training data and are evaluated on DESED test set and its another
private subset.

####  3.1.2 Experimental Results

In Table 1, we compare our HTS-AT with different benchmark models and three
self-ablated variations: (1) $H$: only hierarchical structure; (2) $HC$: with
hierarchical structure and token-semantic module; and (3) $HCP$: (2) with
pretrained vision model (the full setting). Our best setting achieves a new
SOTA mAP 0.471 in a single model as a large increment from 0.459 by AST. We
also ensemble six HTS-ATs with different training random seeds in the same
settings to achieve the mAP as 0.487, and outperforms AST’s 0.475 and 0.485.
We analyze our results in two facets.

##### Token Semantic Module and Pretraining

PSLA, AST and HTS-AT adopt the ImageNet-pretrained model, where PSLA uses the
pretrained EfficientNet [25], AST uses DeiT [26], and our HTS-AT uses the
swin-transformer in Swin-T/C24 setting333https://github.com/microsoft/Swin-
Transformer for $256\times 256$ images ($256\times 256=1024\times 64$ as we
could transfer the same size weights). We can see that the unpretrained single
HTS-AT can achieve an mAP as 0.440. It is improved to 0.453 by the addition of
token semantic module, 1.8% lower than 0.471. Finally the pretrained HTS-AT
achieves the new best mAP as 0.471. However, the unpretrained single AST only
reflects 0.366, 9.3% lower than 0.459. These indicate that: (1) the pretrained
model definitely improves the performance by building a solid prior on pattern
recognition; and (2) HTS-AT shows a far better scalability to different
hyperparameters than AST, since its unpretrained model can still achieve the
third best performance.

##### Parameter Size and Training Time

When comparing the parameter size of each model, the AST has 87M parameters.
And HTS-AT is more lightweight with 31M parameters, which is even compatible
with CNN-based models. As for the estimated training time, PANN takes about
$72$ hours to converge and HST-AT takes about $20\times 4=80$ hours in V-100
GPUs; and AST takes about $150\times 4=600$ hours in 4 TITAN RTX GPUs444We
make memories not exceed 12GB in V-100 in line with TITAN RTX.. The speed
improvement corresponds to the less calculation and GPU memory consumption of
HTS-AT, as we could feed 128 samples instead of only 12 samples in AST per
batch. Therefore, we conclude that HTS-AT consumes less training time and has
fewer parameters than AST’s, which is more efficient.

###  3.2 Evaluations on ESC-50 and Speech Command V2

####  3.2.1 Dataset and Training Detail

The ESC-50 dataset contains 2000 5-sec audio samples labeled with 50
environmental sound classes in 5 folds. We train the model for 5 times by
selecting 4-fold (1600 samples) as training set and the left 1-fold (400
samples) as test set. And we repeat this experiment 3 times with different
random seeds to get the mean performance and deviation. The Speech Command V2
contains 105,829 1-sec spoken word clips labled with 35 common word classes.
It contains 84843, 9981, and 11005 clips for training, validation and
evaluation. Similarly, we train our HTS-AT for 3 times to obtain the
prediction results. We use the mean accuracy score (acc) for the evaluation on
both datasets. For the data processing, we resample the ESC-50 samples into
32kHz and the Speech Command clips 16kHz. And we follow the same setting of
AudioSet to train the model.

####  3.2.2 Experimental Results

We use our best AudioSet-pretrained HTS-AT to train on these two dataset
respectively and compare it with benchmark models (also in AudioSet or extra
data pretraining). Since 1-sec and 5-sec does not take the full 10-sec input
trained on AudioSet, we repeat the 1-sec and 5-sec by 10 and 2 times to make
it 10-sec. As shown in Table 2, the results shows that our HTS-AT achieves a
new SOTA as 97.0% on ESC-50 dataset and equals the SOTA 98.0% on Speech
Command V2. Our deviations are relatively smaller than AST’s, indicating that
HTS-AT is more stable after convergence.

###  3.3 Localization Performance on DESED

We additionally evaluate HTS-AT’s capability to localize the sound event as
start and end time in given audio samples. We use the DESED test set [18],
which contains 692 10-sec test audio samples in 10 classes with the strong
labels. We mainly compare our HTS-AT with PANN. We do not include AST and PSLA
since AST does not directly support the event localization and the PSLA’s code
is not published. We also compare it partially with models in DCASE 2021 [24],
nevertheless they use extra training data and are evaluated on DESED test set
and its another private subset. We use the event-based F1-score on each class
as the evaluation metric, implemented by a Python library
psds_eval555https://github.com/audioanalytic/psds_eval.

The F1-scores on all 10 classes in the DESED by different models are shown in
Table 3. We find that HTS-AT achieves better F1-scores on 8 classes and a
better average F1-score 50.7% than PANN. When compared among leaderboard
models, our model still achieves some highest scores of certain classes.
However, the F1-scores on Speech and Cleaner are relatively low, indicating
that there are still some improvements for a better localization performance.
From the above experiments, we can conclude that HTS-AT is able to produce the
specific localization output via the token-semantic module, which extends the
functionality of the audio transformer.

##  4 Conclusion and Future Work

In this paper, we propose HTS-AT: a hierarchical token-semantic transformer
for audio classification. It achieves a new SOTA on multiple datasets of
different audio classification scenarios. Furthermore, the token-semantic
module enables HTS-AT to locate the events start and end time. Experiments
show that HTS-AT is a high performance, high scalability, and lightweight
audio transformer. In the future, we notice that a partial strong labeled
subset of AudioSet has just been released [27], we decide to conduct a detail
localization training and evaluation work by HTS-AT to further explore its
potential. Combining the audio classification model into more downstreaming
tasks [28, 29] is also considered a future work.

## References

  * [1] Annamaria Mesaros, Toni Heittola, Tuomas Virtanen, and Mark D. Plumbley,  “Sound event detection: A tutorial,”  IEEE Signal Process. Mag. 2021.
  * [2] Perfecto Herrera, Geoffroy Peeters, and Shlomo Dubnov,  “Automatic classification of musical instrument sounds,”  Journal of New Music Research, 2010.
  * [3] Ke Chen, Beici Liang, Xiaoshuan Ma, and Minwei Gu,  “Learning audio embeddings with user listening data for content-based music recommendation,”  in ICASSP 2021.
  * [4] Pete Warden,  “Speech commands: A dataset for limited-vocabulary speech recognition,”  CoRR, vol. abs/1804.03209, 2018.
  * [5] Ke Chen, Cheng-i Wang, Taylor Berg-Kirkpatrick, and Shlomo Dubnov,  “Music sketchnet: Controllable music generation via factorized representations of pitch and rhythm,”  in ISMIR 2020.
  * [6] Hao-Wen Dong, Ke Chen, Julian J. McAuley, and Taylor Berg-Kirkpatrick,  “Muspy: A toolkit for symbolic music generation,”  in ISMIR 2020.
  * [7] Jort F. Gemmeke, Daniel P. W. Ellis, and Dylan Freedman et al.,  “Audio set: An ontology and human-labeled dataset for audio events,”  in ICASSP 2017.
  * [8] Karol J. Piczak,  “ESC: dataset for environmental sound classification,”  in ACM MM 2015. ACM.
  * [9] Logan Ford, Hao Tang, and François Grondin et al.,  “A deep residual network for large-scale acoustic scene analysis,”  in Interspeech 2019.
  * [10] Yun Wang, Juncheng Li, and Florian Metze,  “A comparison of five multiple instance learning pooling functions for sound event detection with weak labeling,”  in ICASSP 2019.
  * [11] Qiuqiang Kong, Yin Cao, and Turab Iqbal et al.,  “Panns: Large-scale pretrained audio neural networks for audio pattern recognition,”  IEEE TASLP 2020.
  * [12] Yuan Gong, Yu-An Chung, and James Glass,  “Psla: Improving audio tagging with pretraining, sampling, labeling, and aggregation,”  IEEE TASLP 2021.
  * [13] Ashish Vaswani, Noam Shazeer, and Niki Parmar et al.,  “Attention is all you need,”  in NeurIPS 2017.
  * [14] Yuan Gong, Yu-An Chung, and James Glass,  “Ast: Audio spectrogram transformer,”  in Interspeech 2021.
  * [15] Jia Deng, Wei Dong, and Richard Socher et al.,  “Imagenet: A large-scale hierarchical image database,”  in CVPR 2009.
  * [16] Wei Gao, Fang Wan, and Xingjia Pan et al.,  “Ts-cam: Token semantic coupled attention map for weakly supervised object localization,”  in ICCV 2021.
  * [17] Ze Liu, Yutong Lin, and Yue Cao et al.,  “Swin transformer: Hierarchical vision transformer using shifted windows,”  CoRR, vol. abs/2103.14030, 2021.
  * [18] Romain Serizel, Nicolas Turpault, Ankit Parag Shah, and Justin Salamon,  “Sound event detection in synthetic domestic environments,”  in ICASSP 2020.
  * [19] Hongyi Zhang, Moustapha Cissé, Yann N. Dauphin, and David Lopez-Paz,  “mixup: Beyond empirical risk minimization,”  in ICLR 2018.
  * [20] Daniel S. Park et al.,  “Specaugment: A simple data augmentation method for automatic speech recognition,”  in Interspeech 2019.
  * [21] Roman Vygon and Nikolay Mikhaylovskiy,  “Learning efficient representations for keyword spotting with triplet loss,”  in SPECOM 2021. Springer.
  * [22] Sergey Verbitskiy and Viacheslav Vyshegorodtsev,  “Eranns: Efficient residual audio neural networks for audio pattern recognition,”  CoRR, vol. abs/2106.01621, 2021.
  * [23] Axel Berg, Mark O’Connor, and Miguel Tairum Cruz,  “Keyword transformer: A self-attention model for keyword spotting,”  in Interspeech 2021.
  * [24] “Dcase 2021 challenge task 4: Sound event detection and separation in domestic environments,” http://dcase.community/challenge2021.
  * [25] Mingxing Tan and Quoc V. Le,  “Efficientnet: Rethinking model scaling for convolutional neural networks,”  in ICML 2019. PMLR.
  * [26] Hugo Touvron, Matthieu Cord, and Matthijs Douze et al.,  “Training data-efficient image transformers & distillation through attention,”  in ICML 2021.
  * [27] Shawn Hershey, Daniel P. W. Ellis, and Eduardo Fonseca et al.,  “The benefit of temporally-strong labels in audio event classification,”  in ICASSP 2021.
  * [28] Ke Chen, Xingjian Du, Bilei Zhu, Zejun Ma, Taylor Berg-Kirkpatrick, and Shlomo Dubnov,  “Zero-shot audio source separation through query-based learning from weakly-labeled data,”  in AAAI 2022.
  * [29] Ke Chen, Gus Xia, and Shlomo Dubnov,  “Continuous melody generation via disentangled short-term representations and structural conditions,”  in IEEE ICSC 2020.


University of Genoa, Italy and
https://logicosimo.gitlab.ioperinibrogi@dima.unige.ithttps://orcid.org/0000-0001-7883-5727
Cosimo Perini Brogi [500]Theory of computation Proof theory [500]Theory of
computation Modal and temporal logics [500]Theory of computation Type theory
[300]Theory of computation Categorical semantics

###### Acknowledgements.

John Q. Open and Joan R. Access 2 42nd Conference on Very Important Topics
(CVIT 2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging, United
Kingdom 42 23

# Natural deduction for intuitionistic belief: proof theory and proof-
theoretic semantics

Cosimo Perini Brogi

###### Abstract

Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an
extension of intuitionistic propositional logic by means of the distributivity
scheme K, and of co-reflection $A\rightarrow\Box A$. This way, belief is
interpreted as a result of verification, and it fits an extended Brouwer-
Heyting-Kolmogorov interpretation for intuitionistic propositional logic with
an epistemic modality. In the present paper, structural properties of a
natural deduction system $\mathsf{IEL}^{-}$ for intuitionistic belief are
investigated also in the light of categorical semantics. The focus is on the
analyticity of the calculus, so that the normalization theorem and the
subformula property are proven firstly. From these, decidability and
consistency of the logic follow as corollaries. Finally, disjunction
properties, $\Box$-primality, and admissibility of reflection rule are
established by using purely proof-theoretic methods.

###### keywords:

Proof Theory, Intuitionistic Modal Logic, Proofs-as-Programs

###### category:

## Introduction

Brouwer-Heyting-Kolmogorov (BHK) interpretation provides a semantics of
mathematical statements in which the computational aspects of proving and
refuting are highlighted.111See e.g. [15]. In this perspective, reasoning
intuitionistically is similar to a safe mode of program execution which always
terminates, and this analogy can be made precise by means of the so-called
Curry-Howard correspondence between proof and programs of type theory [13].

On the other hand, Kripke semantics for intuitionistic logic [5] captures the
informal idea of a process of growth of knowledge in time which characterises
the mental life of the mathematician according to the founders of
intuitionism.

It is worth-noting that the focuses of these semantics are quite different:
BHK interpretation stresses the importance of the concept of proof in the
semantics for intuitionistic logic; Kripke’s approach highlights the epistemic
process behind the provability of a statement.

Artemov and Protopopescu’s [1] suggests that the two views can safely coexist
once a good computational interpretation of epistemic states is given. Their
starting point is thus a BHK interpretation of epistemic statements in which
knowledge and belief are considered as (different) results of a process of
verification. The general idea is that a proof of a (mathematical) statement
is a most strict type of verification, and that verifying a statement is a
sufficient condition for _believing_ it. At the same time, _knowing_ that a
statement is true means, according to this intuitionistic reading, that this
very statement cannot be false, since we have a verification of it.

Hence, the proposed intuitionistic account of epistemic states validates a
principle of “constructivity of truth”

$A\rightarrow\Box A$

and of “intuitionistic factivity of knowledge”

$\Box A\rightarrow\neg\neg A.$

The mentioned paper [1] covers only axiomatic calculi and Kripke semantics for
intuitionistic epistemic logics. Afterwards, the present author has given a
formal analysis of the computational reading of intuitionistic belief in [10],
where a natural deduction system $\mathsf{IEL}^{-}$ for the intuitionistic
logic of belief is developed and designed with the intent of translating it
into a functional calculus of $\mathsf{IEL}^{-}$-deductions.

In the same work, it is given a very quick proof of the strong normalization
theorem for that very natural deduction calculus, and it is shown that the
belief modality can be interpreted also as a specific pointed monoidal
endofunctor on the syntactic category of $\mathsf{IEL}^{-}$-proofs.

In the present paper, we _prove something more_. We address the question of
analyticity for $\mathsf{IEL}^{-}$, and in order to achieve a precise result,
we will develop a different and modular proof of strong normalization, from
which we are able to derive in a the subformula property of normal
$\mathsf{IEL}^{-}$-deductions.

By using this full normalization result, we give then syntactic proofs of
several proof-theoretic properties for the system and investigate the
structural behaviour of our natural deduction for intuitionistic belief.

In more details, we succeed in:

  * •

Developing a proof of strong normalization for $\mathsf{IEL}^{-}$-deduction
w.r.t. both detour elimination and $\vee,\bot$-permutations;

  * •

Proving that $\mathsf{IEL}^{-}$ is analytical – for enjoying the subformula
property – by the latter full normalization result;

  * •

Developing syntactic proofs of several proof-theoretic properties of
$\mathsf{IEL}^{-}$, namely

    * –

decidability;

    * –

canonicity of proofs;

    * –

consistency;

    * –

disjunction property;

    * –

admissibility of the reflection rule  $\Box A$ $A$ ;

    * –

weak disjunction property;

    * –

$\Box$-primality.

The paper is then organised as follows: after recalling the natural deduction
system $\mathsf{IEL}^{-}$ and its type theoretic counterpart for proof-terms
in Section 1, we proceed with Section 2 in proving that, in
$\mathsf{IEL}^{-}$-deductions, detours can be eliminated, and that the
permutations involving absurdity and disjunction can be safely converted, so
that strong normalization holds for proof terms. In Section 3, we use that
normalization result to derive the subformula property for normal deductions,
and prove the structural properties of $\mathsf{IEL}^{-}$ previously
mentioned; also, we recall the proof-theoretic semantics based on category
theory for $\mathsf{IEL}^{-}$-deductions, to see that having permutations does
not harm the semantic adequacy of those structures. Finally, some remarks on
future investigations and related works are made.

##  1 System $\mathsf{IEL}^{-}$

In [1], intuitionistic belief is axiomatized as a calculus $\mathbb{IEL}^{-}$
given by:

  * •

Axiom schemes for intuitionistic propositional logic;

  * •

Axiom scheme $\mathsf{K}:\Box(A\rightarrow B)\rightarrow\Box A\rightarrow\Box
B$;

  * •

Axiom scheme of co-reflection: $A\rightarrow\Box A$;

  * •

Modus Pones  $A\rightarrow B$ $A$ ${\mathit{MP}}$ $B$ as the only inference
rule.

We write $\Gamma\vdash_{\mathbb{IEL}^{-}}A$ when $A$ is derivable in
$\mathbb{IEL}^{-}$ assuming the set of hypotheses $\Gamma$, and we write
$\mathbb{IEL}^{-}\vdash A$ when $\Gamma=\varnothing$.

These principles are chosen to axiomatise the idea that belief is the result
of a verification in an intuitionistic framework where truth is given by
provability, as expressed by the Brouwer-Heyting-Kolmogorov interpretation of
intuitionistic logic. Accordingly, co-reflection states that whatever is
proven, it is also believed, since a proof is a most strict type of
verification. Within this extended BHK interpretation, the epistemic clause
reads as follows [1]:

a proof of $\Box A$ is conclusive evidence of verification that $A$ has a
proof.

Notice that under this reading, the classical reflection scheme $\Box
A\rightarrow A$ does not hold: $A$ can be verified without disclosing a
specific proof.

Besides its potential applications even outside mathematics, in [1]
$\mathbb{IEL}^{-}$ is proven to be a normal modal logic which is sound and
complete w.r.t. a specific relational semantics. Moreover, its proper
extension $\mathbb{IEL}$ is introduced to capture the state of knowledge by
adding the scheme of intuitionistic factivity of truth $\Box
A\rightarrow\neg\neg A$; as for belief, an adequate relational semantic is
given, and some properties of the logics are discussed.

###  1.1 System $\mathsf{IEL}^{-}$

Since in that first work on intuitionistic belief the starting point for
discussing epistemic states is a BHK interpretation of them – therefore, an
implicit computational semantics for belief and knowledge – it seems natural
to develop natural deduction systems that have straightforward type-theoretic
counterparts: this way, it is possible to make rigorous the computational
interpretation of the modal operators introduced by the axioms systems and the
relational structures pf [1].

In the present paper, we focus on the the belief modality, and we introduce
first the following natural deduction system:

######  Definition 1.1.

Let $\mathsf{IEL}^{-}$ be the calculus extending the propositional fragment of
$\mathsf{NJ}$ – the natural deduction calculus for intuitionistic logic as
presented in [14] – by the following rule:

$\Gamma_{1}$ $\vdots$ $\Box A_{1}$ $\cdots$ $\Gamma_{n}$ $\vdots$ $\Box A_{n}$
$[A_{1},\cdots,A_{n}],\Delta$ $\vdots$ $B$ ${\Box-intro}$ $\Box B$

where $\Gamma$ and $\Delta$ are _sets of occurrences of formulae_ , and all
$A_{1},\cdots,A_{n}$ are discharged.

This is the calculus introduced in [10], and it differs from the system
defined in [3] for $\mathbb{IK}$ by allowing the set $\Delta$ of additional
hypotheses is the subdeduction of $B$.

As for the axiomatic system, we write $\Gamma\vdash_{\mathsf{IEL}^{-}}A$ when
$A$ is derivable in $\mathsf{IEL}^{-}$ from the set of hypotheses $\Gamma$,
and $\mathsf{IEL}^{-}\vdash A$ when $\Gamma=\varnothing$.

It is straightforward to check that $\mathsf{IEL}^{-}$ is logically equivalent
to $\mathbb{IEL}^{-}$:

######  Proposition 1.2.

$\Gamma\vdash_{\mathsf{IEL}^{-}}A$ iff $\Gamma\vdash_{\mathbb{IEL}^{-}}A$.

######  Proof 1.3.

For both the directions we reason by induction on the derivation. See [10] for
the details.

###  1.2 Modal $\lambda$-calculus

Despite lacking a certain symmetry pertaining to traditional natural deduction
calculi, deductions in the system $\mathsf{IEL}^{-}$ can be easily turned into
derivation rules for $\lambda$-terms for a modal type theory involving the
belief operator. In other terms, it is possible to extend the correspondence
between intuitionistic natural deduction and typed $\lambda$-calculus –
namely, the Curry-Howard correspondence – to cover $\mathsf{IEL}^{-}$ in a
very natural way.

The correspondence for propositional operators can be summarised as follows

$f\equiv A$ | $\longmapsto$ |  $x_{i}^{A}$, |  where $i$ is the parcel of the hypothesis $A$
---|---|---|---
$f\equiv$ $f_{1}$ $A$ $f_{2}$ $B$ $A\wedge B$ | $\longmapsto$ |  $\langle t^{A},s^{B}\rangle$, |  where $t^{A}$, $s^{B}$ correspond to $f_{1}$ and $f_{2}$ resp.
$f\equiv$ $f^{\prime}$ $A\wedge B$ $A$ | $\longmapsto$ |  $\pi_{1}.t^{A\times B}$, |  where $t^{A\times B}$ corresponds to $f^{\prime}$
$f\equiv$ $f^{\prime}$ $A\wedge B$ $B$ | $\longmapsto$ |  $\pi_{2}.t^{A\times B}$, |  where $t^{A\times B}$ corresponds to $f^{\prime}$
$f\equiv$ $f^{\prime}$ $B$ $A\rightarrow B$ | $\longmapsto$ |  $\lambda x_{i}^{A}.t^{B}$, |  where $t^{B}$ corresponds to $f^{\prime}$ and $i$ is the parcel of discharged hypotheses $A$
$f\equiv$ $f_{1}$ $A\rightarrow B$ $f_{2}$ $A$ $B$ | $\longmapsto$ |  $t^{A\rightarrow B}s^{A}$, |  where $t^{A\rightarrow B}$, $s^{A}$ correspond to $f_{1}$ and $f_{2}$ resp.
$f\equiv$ $f^{\prime}$ $A$ $A\vee B$ | $\longmapsto$ |  $\;\mathsf{in}_{1}.t^{A}$, |  where $t^{A}$ corresponds to $f^{\prime}$
$f\equiv$ $f^{\prime}$ $B$ $A\vee B$ | $\longmapsto$ |  $\;\mathsf{in}_{2}.s^{B}$, |  where $s^{B}$ corresponds to $f^{\prime}$
$f\equiv$ $f^{\prime}$ $A\vee B$ $[A]$ $\vdots$ $C$ $[B]$ $\vdots$ $C$ $C$ | $\longmapsto$ | $\mathsf{C}_{x^{A},y^{B}}(t,t_{1},t_{2})$ |  where $\mathsf{C}$ bounds all occurrences of $x$ in $t_{1}$ and all occurrences of $y$ in $t_{2}$, and $t,t_{1},t_{2}$ correspond to $f^{\prime}$, the subdeduction of $C$ from $A$, and the subdeduction of $C$ from $B$, resp.
$f\equiv$ $f^{\prime}$ $\bot$ $A$ | $\longmapsto$ | $\mathsf{E}_{A}t$ |  where $t$ corresponds to $f^{\prime}$
$f\equiv$ $f^{\prime}$ $A$ $\top$ | $\longmapsto$ | $(\mathsf{U}t)$ |  where $t$ correspond to $f^{\prime}$.

The $\lambda$-term corresponding to $\Box$-introduction is then ruled by:

$\Gamma_{1}\vdash t_{1}:\Box A_{1}$ $\cdots$ $\Gamma_{n}\vdash t_{n}:\Box
A_{n}$ $x_{1}:A_{1},\cdots,x_{n}:A_{n},\Delta\vdash s:B$
$\Gamma_{1},\cdots,\Gamma_{n},\Delta\vdash\mathsf{B}_{x_{1},\cdots,x_{n}}(t_{1},\cdots,t_{n})\,\mathsf{in}\,s\;:\Box
B$

Here we see that just by decorating $\mathsf{IEL}^{-}$-deductions with proof
names we have a term-calculus making clear the computational interpretation of
the belief operator.

##  2 Normalization for $\mathsf{IEL}^{-}$-deductions

The modal $\lambda$-calculus just presented gives a neat notation for
investigating the structural properties of $\mathsf{IEL}^{-}$ by allowing an
equational reasoning on proof-terms.

As it is known, by imposing rewriting rules on $\mathsf{NJ}$-deductions – as
defined in [11] –, we obtain the complete engine of $\lambda$-calculus
associated to that natural deduction.

For our modal $\lambda$-calculus, we just need to add to system corresponding
to the propositional fragment of $\mathsf{NJ}$ the following rewritings:

######  Definition 2.1 (Modal rewritings).

  1. 1.

$\mathsf{B}_{x_{1},\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},(\mathsf{B}_{\vec{y}}(\vec{s})\;\mathsf{in}\;t_{i}),t_{i+1},\cdots,t_{n})\;\mathsf{in}\;r\,\\\
>_{M}\mathsf{B}_{x_{1},\cdots,x_{i-1},\vec{y},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},\vec{s},t_{i+1},\cdots,t_{n})\;\mathsf{in}\;r[x_{i}:=t_{i}]$

  2. 2.

$\mathsf{B}_{x}t\;\mathsf{in}\;x>_{M}t$

In [10], the present author already gave a quick proof of strong normalization
of the full modal $\lambda$-calculus corresponding to $\mathsf{IEL}^{-}$ by
tweaking a proof strategy due to [4] for the implicational fragment of
intuitionistic minimal modal logic $\mathbb{IK}$. Therefore, we already know
that every $\mathsf{IEL}^{-}$-deductions has a unique normal form, as
required.

That system of rewritings, however, does not suffice to establish the
subformula property for $\mathsf{IEL}^{-}$: in order to achieve that, we need
further reductions between proof-terms involving $\bot$\- and
$\vee$-elimination. Unfortunately, the translation adopted in that context
does not preserve these additional rewritings, so that a different proof is
required.

Our strategy consists of an extension of the method developed in [2], and, as
in that paper, we use a modified CPS translation into simple type theory that
is arithmetizable without using higher-order reasoning.

We commit the next pages to develop such a proof.

###  2.1 Normalization for $\vee$-permutations

Let $\lambda^{\Box\rightarrow\wedge\vee}$ denote the type theory corresponding
to the fragment of $\mathsf{IEL}^{-}$ with $\Box$-modality, implication,
conjunction and disjunctions as operators.

Its syntax is given by the following grammar:

$T::=p\;|\;A\rightarrow B\;|\;A\times B\;|\;A+B\;|\;\Box A$ $t::=\;$ | $x\;|\;\lambda x:A.t:B\;|\;t_{1}t_{2}\;|\;\langle t_{1},t_{2}\rangle\;|\;\pi_{1}(t)\;|\;\pi_{2}(t)\;|\;\mathsf{in}_{1}(a:A)\;|\;\mathsf{in}_{2}(b:B)\;|\;\mathsf{C}_{x,y}(t,t_{1},t_{2})\;|\;$
---|---
|  $\mathsf{B}_{\vec{x}:\vec{A}}\,\vec{t}:\vec{\Box
A}\;\mathsf{in}\;(s:B):\Box B$ .

As stated before, in order to obtain the subformula property for our natural
deduction, the rewritings introduced in definition 2.1 are not enough.
Therefore we add the following reductions:

######  Definition 2.2 (Permutations for
$\lambda^{\Box\rightarrow\wedge\vee}$).

  1. 1.

$\mathsf{C}_{x,y}(t,t_{1},t_{2})s\,>_{P}\,\mathsf{C}_{x,y}(t,t_{1}s,t_{2}s)$

  2. 2.

$\pi_{i}\mathsf{C}_{x,y}(t,t_{1},t_{2})\,>_{P}\,\mathsf{C}_{x,y}(t,\pi_{i}t_{1},\pi_{i}t_{2})$
for $i=1,2$

  3. 3.

$C_{u,v}(C_{x,y}(t,t_{1},t_{2}),s_{1},s_{2})\,>_{P}\,\mathsf{C}_{x,y}(t,\mathsf{C}_{u,v}(t_{1},s_{1},s_{2}),\mathsf{C}_{u,v}(t_{2},s_{1},s_{2}))$

  4. 4.

$\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}\,(t_{1},\cdots,t_{i-1},\mathsf{C}_{x,y}(t,s_{1},s_{2}),t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s\,>_{P}\\\
\mathsf{C}_{x,y}(t,\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{1},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s,\\\
\;\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{2},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s)$.

We now assign a norm to $\lambda^{\Box\rightarrow\wedge\vee}$-terms.

######  Definition 2.3 (Permutation degree for
$\lambda^{\Box\rightarrow\wedge\vee}$).

  1. 1.

$|x|=1$

  2. 2.

$|\lambda x.t|=|t|$

  3. 3.

$|ts|=|t|+\\#t\times|s|$

  4. 4.

$|\langle t,s\rangle|=|t|+|s|$

  5. 5.

$|\pi_{i}t|=|t|+\\#t$ for $i=1,2$

  6. 6.

$|\mathsf{in}_{i}t|=|t|$ for $i=1,2$

  7. 7.

$|\mathsf{C}_{x,y}(t,t_{1},t_{2})|=|t|+\\#t\times(|t_{1}|+|t_{2}|)$

  8. 8.

$|\mathsf{B}_{x_{1},\cdots,x_{n}}\,(t_{1},\cdots,t_{n})\,\mathsf{in}\,s|=|s|\times\prod^{n}_{i=0}|t_{i}|+\prod_{i=0}^{n}\\#t_{i}$

where

  9. 9.

$\\#x=1$

  10. 10.

$\\#\lambda x.t=1$

  11. 11.

$\\#ts=\\#t$

  12. 12.

$\\#\langle t,s\rangle=1$

  13. 13.

$\\#\pi_{i}t=\\#t$ for $i=1,2$

  14. 14.

$\\#\mathsf{in}_{i}t=1$ for $i=1,2$

  15. 15.

$\\#\mathsf{C}_{x,y}(t,t_{1},t_{2})=2\times\\#t\times(\\#t_{1}+\\#t_{2})$

  16. 16.

$\\#\mathsf{B}_{x_{1},\cdots,x_{n}}\,(t_{1},\cdots,t_{n})\,\mathsf{in}\,s=\\#s\times\prod_{i=0}^{n}\\#t_{i}$

Now we prove that this norm decreases after a permutation.

######  Lemma 2.4.

For any $\lambda^{\Box\rightarrow\wedge\vee}$-terms $t,s$, if $t>_{P}s$, then
$\\#t=\\#s$.

######  Proof 2.5.

Cases involving traditional operators are dealt with in [2, lemma 4].

We just have to prove the claim for the $\Box,\vee$-permutation:

$\\#\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}\,(t_{1},\cdots,t_{i-1},\mathsf{C}_{x,y}(t,s_{1},s_{2}),t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s$ | $=$ |
---|---|---
$\\#s\times\\#\mathsf{C}_{x,y}(t,s_{1},s_{2})\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}$ | $=$ |
$\\#s\times 2\times\\#t\times(\\#s_{1}+\\#s_{2})\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}$ . |  |

$\\#\mathsf{C}_{x,y}(t,\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{1},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s,$ |  |
---|---|---
$\qquad\,\,\,\,\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{2},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s)$ | $=$ |
$2\times\\#t\times(\\#\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{1},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s\;+$ |  |
$\qquad\qquad\,\\#\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{2},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s)$ | $=$ |
$2\times\\#t\times(\\#s\times\prod_{j=0}^{i-1}\\#t_{j}\times\\#s_{1}\times\prod_{j=i+1}^{n}\\#t_{j}+\\#s\times\prod_{j=0}^{i-1}\\#t_{j}\times\\#s_{2}\times\prod_{j=i+1}^{n}\\#t_{j})$ | $=$ |
$\\#s\times 2\times\\#t\times(\\#s_{1}+\\#s_{2})\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}$ . |  |

######  Lemma 2.6.

For any $\lambda^{\Box\rightarrow\wedge\vee}$-terms $t,s$, if $t>_{P}s$, then
$|t|>|s|$.

######  Proof 2.7.

As for lemma 2.4, cases involving traditional operators are dealt with in [2,
lemma 5]. It remains to prove the claim for the $\Box,\vee$-permutation only:

$|\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}\,(t_{1},\cdots,t_{i-1},\mathsf{C}_{x,y}(t,s_{1},s_{2}),t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s|$ | $=$ |
---|---|---
$|s|\times|\mathsf{C}_{x,y}(t,s_{1},s_{2})|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|$ | $=$ |
$|s|\times|\mathsf{C}_{x,y}(t,s_{1},s_{2})|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|+\prod_{j=0}^{i-1}\\#t_{j}\times\\#\mathsf{C}_{x,y}(t,s_{1},s_{2})\times\prod_{j=i+1}^{n}\\#t_{j}$ | $=$ |
$(|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times(|t|+\\#t\times(|s_{1}|+|s_{2}|))\;+$ |  |
$\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times(2\times\\#t\times(\\#s_{1}+\\#s_{2})))$ | $=$ |
$(|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|t|\;+$ |  |
$\\#t\times|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{1}|+\\#t\times|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{2}|\,+$ |  |
$2\times\\#t\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{1}+2\times\\#t\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{1})$ | $>$ |
$(|t|+\\#t\times|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{1}|+\\#t\times|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{2}|\;+$ |  |
$\\#t\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{1}+\\#t\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{2})$ | $=$ |
$(|t|+\\#t\times(|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{1}|+|s|\times\prod_{j=0}^{i-1}|t_{j}|\times\prod_{j=i+1}^{n}|t_{j}|\times|s_{2}|\;+$ |  |
$\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{1}+\times\prod_{j=0}^{i-1}\\#t_{j}\times\prod_{j=i+1}^{n}\\#t_{j}\times\\#s_{2}))$ | $=$ |
$(|t|+\\#t\times(|\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{1},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s|\;+$ |  |
$|\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{2},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s|))$ | $=$ |
$|(\mathsf{C}_{x,y}(t,\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{1},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s,$ |  |
$\qquad\,\,\,\,\mathsf{B}_{x1,\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},s_{2},t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s)|$, |  |

as required.

As an immediate consequence we have strong normalization w.r.t.
$\vee$-permutations:

######  Lemma 2.8.

$\lambda^{\Box\rightarrow\wedge\vee}$-calculus is strongly normalizing w.r.t.
$>_{P}$.

Notice that this result does not involve types, but it, as previously stated,
is mandatory for obtaining the subformula property for the typed system.

###  2.2 Detour elimination

We want to eliminate useless steps of computation from our
$\mathsf{IEL}^{-}$-deductions. For the moment, we shall restrict to the
$\lambda^{\Box\rightarrow\wedge\vee}$-calculus for proof-terms, and extend the
standard rewritings for the corresponding fragment of intuitionistic natural
deduction by the reduction $>_{M}$ introduced in definition 2.1. The resulting
system is then the following:

######  Definition 2.9 (Detour conversions for
$\lambda^{\Box\rightarrow\wedge\vee}$).

  1. 1.

$(\lambda x.t)s\,>_{D}\,t[x:=s]$

  2. 2.

$\pi_{i}\langle t_{1},t_{2}\rangle\,>_{D}\,t_{i}$ for $i=1,2$

  3. 3.

$C_{x_{1},x_{2}}(\mathsf{in}_{i}t,t_{1},t_{2})\,>_{P}\,t_{i}[x_{i}=t]$ for
$i=1,2$

  4. 4.

$\mathsf{B}_{x_{1},\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},(\mathsf{B}_{\vec{y}}(\vec{s})\;\mathsf{in}\;t_{i}),t_{i+1},\cdots,t_{n})\;\mathsf{in}\;r\,\\\
>_{D}\mathsf{B}_{x_{1},\cdots,x_{i-1},\vec{y},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},\vec{s},t_{i+1},\cdots,t_{n})\;\mathsf{in}\;r[x_{i}:=t_{i}]$

  5. 5.

$\mathsf{B}_{x}t\;\mathsf{in}\;x>_{D}t$

In general, $>_{\ldots}$ will denote a one-step reduction relation between
$\lambda$-terms. In the following, we use $\overset{{+}}{>_{\ldots}}$ for the
transitive closure of $>_{\ldots}$, and $\gg_{\ldots}$ for its reflexive
transitive closure.

As stated before, it is possible to show that $\mathsf{IEL}^{-}$-deductions do
normalise w.r.t. $>_{D}$ by simulating modal rewritings as
$\rightarrow$-rewritings in simple type theory [10]. But since we want to
consider permutations also, that strategy must be enforced to make the
underlying translation compatible with $>_{P}$.

In the following, we will see that it is possible to reduce
$\lambda^{\Box\rightarrow\wedge\vee}$ to simple type theory – where
$\rightarrow$ is the only type – by a modified general negative translation
that is able to map normal forms into normal forms. Again, we accommodate the
definitions in [2, §4] to cover the modal constructions.

######  Definition 2.10 (CPS-translation).

Let $\overline{A}$ be the translation for the type $A$ of
$\lambda^{\Box\rightarrow\wedge\vee}$ defined by:

$\overline{A}\,=\,\sim\sim A^{\circ}$

where $\sim A=A\rightarrow q$ for a specific atomic type $q$, and where

  * •

$p^{\circ}=p$

  * •

$(A\rightarrow B)^{\circ}=\overline{A}\rightarrow\overline{B}$

  * •

$(A\wedge B)^{\circ}=\,\sim(\overline{A}\rightarrow\sim\overline{B})$

  * •

$(A\vee B)^{\circ}=\,\sim\overline{A}\rightarrow\sim\sim\overline{B}$

  * •

$(\Box A)^{\circ}=\,\sim\sim\overline{A}$

For terms, we define

  * •

$\overline{x}=\lambda k.xk$

  * •

$\overline{\lambda x.t}=\lambda k.k(\lambda x.\overline{t}$

  * •

$\overline{ts}=\lambda k.\overline{t}(\lambda m.m\overline{s}k)$

  * •

$\overline{\langle t,s\rangle}=\lambda k.k(\lambda
u.u\overline{t}\overline{s})$

  * •

$\overline{\pi_{1}t}=\lambda k.\overline{t}(\lambda u.u(\lambda i.\lambda
j.ik))$

  * •

$\overline{\pi_{1}t}=\lambda k.\overline{t}(\lambda u.u(\lambda i.\lambda
j.jk))$

  * •

$\overline{\mathsf{in}_{1}t}=\lambda k.k(\lambda i.\lambda j.i\overline{t})$

  * •

$\overline{\mathsf{in}_{1}t}=\lambda k.k(\lambda i.\lambda j.j\overline{t})$

  * •

$\overline{\mathsf{C}_{x,y}(t,t_{1},t_{2})}=\lambda k.\overline{t}(\lambda
m.m(\lambda x.\overline{t_{1}}k)(\lambda y.\overline{t_{2}}k))$

  * •

$\overline{\mathsf{B}_{x_{1},\cdots,x_{n}}(t_{1},\cdots,t_{n})\,\mathsf{in}\,s}=\lambda
k.\overline{t_{1}}(\lambda x_{1}.\cdots\overline{t_{n}}(\lambda
x_{n}.k\overline{s})\cdots)$ where $k,m,u,i,j$ are fresh variables.

It is now easy to prove that this translation preserves typing:

######  Proposition 2.11.

Let $t$ be a $\lambda^{\Box\rightarrow\wedge\vee}$-term with type $A$ in
context $\Gamma$. Then $\overline{t}$ is a term of simple type theory with
type $\overline{A}$ in context $\overline{\Gamma}$.

######  Proof 2.12.

By induction on the structure of $t$. We consider the case
$t=\mathsf{B}_{x_{1},\cdots,x_{n}}(t_{1},\cdots,t_{n})\,\mathsf{in}\,s$:

$\overline{\Gamma_{1}}\vdash\overline{t_{1}}:\,\sim\sim\overline{A_{1}}$
$\overline{\Gamma_{n}}\vdash\overline{t_{n}}:\,\sim\sim\overline{A_{n}}$
$x_{1}:\overline{A_{1}},\cdots,x_{n}:\overline{A_{n}},\overline{\Delta}\vdash\overline{s}:\overline{B}$
$k:\,\sim\overline{B}\vdash k:\,\sim\overline{B}$
$x_{1}:\overline{A_{1}},\cdots,x_{n}:\overline{A_{n}},\overline{\Delta},k:\,\sim\overline{B}\vdash
k\overline{s}:q$
$x_{1}:\overline{A_{1}},\cdots,x_{n-1}:\overline{A_{n-1}},\overline{\Delta},k:\,\sim\overline{B}\vdash\lambda
x_{n}.k\overline{s}:\,\sim\overline{A_{n}}$
$\overline{\Gamma_{n}},x_{1}:\overline{A_{1}},\cdots,x_{n-1}:\overline{A_{n-1}},\overline{\Delta},k:\,\sim\overline{B}\vdash
t_{n}(\lambda x_{n}.k\overline{s}):q$
$\overline{\Gamma_{n}},x_{1}:\overline{A_{1}},\cdots,x_{n-2}:\overline{A_{n-2}},\overline{\Delta},k:\,\sim\overline{B}\vdash\lambda
x_{n-1}.t_{n}(\lambda x_{n}.k\overline{s}):\,\sim\overline{A_{n-1}}$ $\vdots$
$\overline{\Gamma_{2}},\cdots\overline{\Gamma_{n}},\overline{\Delta},k:\,\sim\overline{B}\vdash(\lambda
x_{1}.\cdots\overline{t_{n}}(\lambda
x_{n}.k\overline{s})\cdots):\,\sim\overline{A_{1}}$
$\overline{\Gamma_{1}},\cdots\overline{\Gamma_{n}},\overline{\Delta},k:\,\sim\overline{B}\vdash\overline{t_{1}}(\lambda
x_{1}.\cdots\overline{t_{n}}(\lambda x_{n}.k\overline{s})\cdots):q$
$\overline{\Gamma_{1}},\cdots\overline{\Gamma_{n}},\overline{\Delta}\vdash\lambda
k.\overline{t_{1}}(\lambda x_{1}.\cdots\overline{t_{n}}(\lambda
x_{n}.k\overline{s})\cdots):\,\sim\sim\overline{B}$

For terms we need some accommodations:

######  Definition 2.13 (Modified CPS-translation).

The modified CPS-translation $\overline{\overline{t}}$ for any
$\lambda^{\Box\rightarrow\wedge\vee}$-term is

$\overline{\overline{t}}\,=\,\lambda k.(M:k),$

where $k$ is a fresh variable, and where the infix operator $:$ is defined by
induction on the structure of $t$:

  * •

$x:r=xr$

  * •

$\lambda x.t:r=r(\lambda x.\overline{\overline{t}})$

  * •

$ts:r=t:\lambda m.m\overline{\overline{s}}r$

  * •

$\langle t,s\rangle:r=r(\lambda
u.u\overline{\overline{t}}\overline{\overline{s}})$

  * •

$\pi_{1}t:r=t:\lambda u.u(\lambda i.\lambda j.ir)$

  * •

$\pi_{1}t:r=t:\lambda u.u(\lambda i.\lambda j.jr)$

  * •

$\mathsf{in}_{1}t:r=r(\lambda i.\lambda j.i\overline{\overline{t}})$

  * •

$\mathsf{in}_{1}t:r=r(\lambda i.\lambda j.j\overline{\overline{t}})$

  * •

$\mathsf{C}_{x,y}(t,t_{1},t_{2}):r=t:\lambda m.(\lambda x.(t_{1}:r))(\lambda
y.(t_{2}:r))$

  * •

$\mathsf{B}_{x_{1},\cdots,x_{n}}(t_{1},\cdots,t_{n})\,\mathsf{in}\,s:r=t_{1}:(\lambda
x_{1}.\cdots t_{n}:(\lambda x_{n}.r\overline{\overline{s}})\cdots)$

where $m,u,i,j$ are fresh variables and $x,y,x_{1},\cdots,x_{n}$ do not occur
free in $r$.

Now we see that this modified translation deletes $\beta$-redexes from the
previous CPS-translation.

######  Lemma 2.14.

Let $t,r$ be $\lambda^{\Box\rightarrow\wedge\vee}$-terms. Then

  1. 1.

$\overline{t}\gg_{\beta\eta}\overline{\overline{t}}$

  2. 2.

$\overline{t}r\gg_{\beta\eta}t:r$

######  Proof 2.15.

By simultaneous induction for property 1 and property 2 on the structure of
$t$.

Moreover, typing is respected by the modified translation, as expected.

######  Proposition 2.16.

Let $t$ be a $\lambda^{\Box\rightarrow\wedge\vee}$-term with type $A$ in
context $\Gamma$. Then $\overline{\overline{t}}$ is a term of simple type
theory with type $\overline{A}$ in context $\overline{\Gamma}$.

######  Proof 2.17.

By proposition 2.11, and lemma 2.14.

The next lemmas show that we can simulate detours by $\beta\eta$-reductions.

######  Lemma 2.18.

For $\lambda^{\Box\rightarrow\wedge\vee}$-terms $t,s$ and any term $r$ of
simple type theory that has no free occurrences of $x$, the following hold:

  1. 1.

$(t:r)[x:=\overline{\overline{s}}]\gg_{\beta\eta}\,(t[x:=s]):r$

  2. 2.

$\overline{\overline{t}}[x:=\overline{\overline{s}}]\gg_{\beta\eta}\overline{\overline{t[x:=s]}}.$

######  Proof 2.19.

Property 1 is proven by induction on the structure of $t$. Property 2 then
follows.

######  Lemma 2.20.

For any terms $r,s$ of simple type theory such that
$r\overset{{+}}{>}_{\beta\eta}s$, we have
$t:r\,\overset{{+}}{>}_{\beta\eta}\,t:s$ for any
$\lambda^{\Box\rightarrow\wedge\vee}$-term $t$.

######  Proof 2.21.

By straightforward induction on the structure of $t$.

######  Lemma 2.22.

Let $t,s$ be two $\lambda^{\Box\rightarrow\wedge\vee}$-terms such that
$t>_{D}s$. Then:

  1. 1.

$t:r\overset{{+}}{>}_{\beta\eta}s:r$ for any term $r$ of simple type theory,

  2. 2.

$\overline{\overline{t}}\overset{{+}}{>}_{\beta\eta}\overline{\overline{s}}$.

######  Proof 2.23.

Property 2 follows from property 1, which is proven by distinguishing cases of
$>_{D}$. By [2, Lemma 15], we can only consider the modal rewritings:

  * •

$(\mathsf{B}_{x}t\,\mathsf{in}\,x):r=t:\lambda
x.r\overline{\overline{x}}=t:\lambda x.r(\lambda
h.xh)\overset{{+}}{>}_{\beta\eta}t:r.$

  * •

To improve readability, we consider the term
$\mathsf{B}_{x}(\mathsf{B}_{y}t\,\mathsf{in}\,s_{1})\,\mathsf{in}\,s$, since
the case with multiple variables and subterms is an easy generalization:

$(\mathsf{B}_{x}(\mathsf{B}_{y}t\,\mathsf{in}\,s_{1})\,\mathsf{in}\,s):r=(\mathsf{B}_{y}t\,\mathsf{in}\,s_{1}):\lambda
x.r\overline{\overline{s}}=t:\lambda y.(\lambda
x.r\overline{\overline{s}})\overline{\overline{s_{1}}}>_{\beta}t:\lambda
y.r\overline{\overline{s}}[x:=\overline{\overline{s_{1}}}]\underset{\textrm{lem.}\ref{lem13}}{\gg_{\beta\eta}}\\\
t:\lambda
y.k\overline{\overline{s[x:=s_{1}]}}\,=\,(\mathsf{B}_{y}.t\,\mathsf{in}\,s[x:=s_{1}]):r$

as required.

Normalization w.r.t. detours is now an easy consequence of the previous lemma:

######  Proposition 2.24.

$\lambda^{\Box\rightarrow\wedge\vee}$ is strongly normalizing w.r.t.
$>_{D}$-reductions.

######  Proof 2.25.

By lemma 2.22, every detour elimination from a
$\lambda^{\Box\rightarrow\wedge\vee}$-term corresponds to a
$\beta\eta$-reduction in simple type theory, which is strongly normalizing
[13].

At this point we have to combine the previous results in order to obtain
normalization for both permutations and detours. That is, basically, the
reason for the next lemma.

######  Lemma 2.26.

For any $\lambda^{\Box\rightarrow\wedge\vee}$-terms $t,s$ such that $t>_{P}s$,
we have the following:

  * •

$t:r=s:r$ for any term $r$ of simple type theory,

  * •

$\overline{\overline{t}}=\overline{\overline{s}}$.

######  Proof 2.27.

Property 2 follows from property 1, which is proven by distinguishing the
cases for $>_{P}$. By [2, lemma 17], we shall limit to the
$\Box,\vee$-permutations, and, as before, we consider the $\Box$-term
$\mathsf{B}_{z}(\mathsf{C}_{x,y}(t,s_{1},s_{2}))\,\mathsf{in}\,s$, since the
result for the more general structure follows the same pattern:
$\mathsf{B}_{z}(\mathsf{C}_{x,y}(t,s_{1},s_{2}))\,\mathsf{in}\,s:r=\mathsf{C}_{x,y}(t,s_{1},s_{2}):\lambda
z.r\overline{\overline{s}}=\\\ =t:\lambda m.m(\lambda x.(s_{1}:\lambda
z.r\overline{\overline{s}}))(\lambda y.(s_{2}:\lambda
z.r\overline{\overline{s}}))\underset{{\alpha}}{=}t:\lambda m.m(\lambda
x.(s_{1}:\lambda u.r\overline{\overline{s}}))(\lambda y.(s_{2}:\lambda
w.r\overline{\overline{s}}))=\\\ =t:\lambda m.m(\lambda
x.(\mathsf{B}_{u}s_{1}\,\mathsf{in}\,s:r))(\lambda
y.\mathsf{B}_{w}s_{2}\,\mathsf{in}\,s:r))=\mathsf{C}_{x,y}(t,\mathsf{B}_{u}s_{1}\,\mathsf{in}\,s,\mathsf{B}_{w}s_{2}\,\mathsf{in}\,s):r$

as desired.

Normalization is now a direct consequence.

######  Theorem 2.28.

$\lambda^{\Box\rightarrow\wedge\vee}$ is strongly normalizing w.r.t. the
reduction relation induced by the union of detour- and permutation-
conversions.

######  Proof 2.29.

Suppose that it is not in the case. Then there would exist an infinite
sequence of detour- and permutation-conversions starting at, say, $t$. By
proposition 2.24, in such a sequence, there must be a finite number of detour-
conversions, so that we must have an infinite number of permutation-
conversions in it, contra lemma 2.8.

###  2.3 Normalization for $\bot$-conversions

The previous theorem establishes that the $\bot$-free fragment of
$\mathsf{IEL}^{-}$ enjoys the subformula property, along with normalization of
proofs.

In order to obtain the same results for the full calculus, we need some
further efforts, but the general idea is the same as before.

Let $\lambda^{\Box\rightarrow\wedge\vee\bot}$ denote the type theory
corresponding to the full natural deduction for intuitionistic belief.

Its syntax is an extension of that for $\lambda^{\Box\rightarrow\wedge\vee}$
by the type $\bot$ and the term $\mathsf{E}(t:A)$ – corresponding, as usual,
to $\bot$-elimination in the natural deduction.

For permutations, we need to add to definition 2.2 the following permutation:

$\mathsf{E}(\mathsf{C}_{x,y}(t,t_{1},t_{2}))>_{P}\mathsf{C}_{x,y}(t,\mathsf{E}(t_{1}),\mathsf{E}({t_{2}})).$
(1)

In [2], de Groote proves that $\mathsf{NJ}$ is strongly normalizing w.r.t. the
reduction relation induced by these extended permutation-conversions and
detour-elimination.222The strategy is again a modified CPS translation of the
full calculus and a definition of a norm on untyped term: see [2, § 7] for the
details.

To these ones, further $\bot$-conversions are added in order to obtain the
subformula property for $\mathsf{NJ}$-normal proofs. For $\mathsf{IEL}^{-}$,
we proceed similarly, and the next definition integrates the additional
$\bot$-conversions for $\mathsf{NJ}$ with a specific reduction involving the
typing rule for the belief modality.

######  Definition 2.30 ($\bot$-conversions for
$\lambda^{\Box\rightarrow\wedge\vee\bot}$).

  1. 1.

$\mathsf{E}(t)s>_{\bot}\mathsf{E}(t)$

  2. 2.

$\pi_{i}\mathsf{E}(t)>_{\bot}\mathsf{E}(t)$ for $i=1,2$

  3. 3.

$\mathsf{C}_{x,y}(\mathsf{E}(t),t_{1},t_{2})>_{\bot}\mathsf{E}(t)$

  4. 4.

$\mathsf{E}(\mathsf{E}(t)>_{\bot}\mathsf{E}(t)$

  5. 5.

$\mathsf{B}_{x_{1},\cdots,x_{i-1},x_{i},x_{i+1},\cdots,x_{n}}(t_{1},\cdots,t_{i-1},\mathsf{E}(t_{i}),t_{i+1},\cdots,t_{n})\,\mathsf{in}\,s>_{\bot}\mathsf{E}(t_{i}).$

We immediately have

######  Proposition 2.31.

$\lambda^{\Box\rightarrow\wedge\vee\bot}$ is strongly normalising w.r.t.
$\bot$-conversions.

######  Proof 2.32.

Straightforward, for having, in any $\bot$-reduction, a term of smaller
complexity on the right hand side of $>_{\bot}$ than that one on the left hand
side.

##  3 Analyticity and corollaries

As it is clear from the definition, $\bot$-conversions are introduced because
the permutations of definition 2.2 extended by (1) determine the subformula
property for $\mathsf{IEL}^{-}$ _only if_ $\bot$-elimination introduces just
atomic formulas. On the other hand, the reductions of definition 2.30 – though
necessary for establishing the subformula property of normal
$\mathsf{IEL}^{-}$-deductions – break down the modified CPS translation of
$\lambda^{\Box\rightarrow\wedge\vee\bot}$-terms into terms of simple type
theory, for normal $\mathsf{IEL}^{-}$-deductions are no longer translated into
normal deductions of the implicational fragment of $\mathsf{NJ}$.

Following again [2], in the next sections, we see how to solve the issue, so
that we can apply our full computational analysis of intuitionistic belief to
establish further properties of the system: the forthcoming lemmas are
committed to that.

###  3.1 Subformula property

Gentzen introduced sequent systems in order to give a neat proof of the
subformula principle by means of cut-elimination; for intuitionistic and
classical logic, it is possible indeed to translate normal deductions into
cut-free derivations in the appropriate sequent calculus and vice-versa, this
way obtaining the subformula property for the corresponding natural deduction
systems.

In spite of this, it is sometimes possible to give a more direct proof of the
principle reasoning about the very natural deduction calculus: here we adopt
just this strategy.

Recall first from proposition 2.31 that $\mathsf{IEL}^{-}$ is strongly
normalizable w.r.t. $\bot$-conversions. In order to obtain the subformula
property for our calculus we only need to show that we can postpone those
conversions, as proven by the following lemmas.

######  Lemma 3.1.

For any $\lambda^{\Box\rightarrow\wedge\vee\bot}$-terms $t,s,r$ such that
$t>_{\bot}s$, we have $t[x:=r]>_{\bot}s[x:=r]$.

######  Proof 3.2.

Straightforward, after distinguishing the cases for $>_{\bot}$.

######  Lemma 3.3.

For any $\lambda^{\Box\rightarrow\wedge\vee\bot}$-terms $t,s,r$ such that
$s>_{\bot}r$, we have
$t[x:=s]\gg_{\bot}t[x:=r]$.

######  Proof 3.4.

By induction on $t$.

######  Lemma 3.5.

Let $R\in\\{D,P\\}$ and let $r,s,t$ be
$\lambda^{\Box\rightarrow\wedge\vee\bot}$-terms such that $r>_{\bot}s>_{R}t$.
Then there exists a $\lambda^{\Box\rightarrow\wedge\vee\bot}$-term $k$ such
that $r\overset{{+}}{>}_{R}k\gg_{\bot}t$.

######  Proof 3.6.

After [2, lemma 57], we only consider the following critical pair:

$\begin{matrix}\mathsf{B}_{z}(\mathsf{E}(\mathsf{C}_{x,y}(t_{1},t_{2},t_{3})))\,\mathsf{in}\,s_{1}&>_{P}&\mathsf{B}_{z}(\mathsf{C}_{x,y}(t_{1},\mathsf{E}(t_{2}),\mathsf{E}(t_{3})))\,\mathsf{in}\,s_{1}\\\
&>_{P}&\mathsf{C}_{x,y}(t_{1},\mathsf{B}_{z}(\mathsf{E}(t_{2})\,\mathsf{in}\,s_{1},\mathsf{B}_{z}(\mathsf{E}(t_{3})\,\mathsf{in}\,s_{1}))\\\
&>_{\bot}&\mathsf{C}_{x,y}(t_{1},\mathsf{E}(t_{2}),\mathsf{E}(t_{3}))\\\
\end{matrix}$

whenever

$\begin{matrix}\mathsf{B}_{z}(\mathsf{E}(\mathsf{C}_{x,y}(t_{1},t_{2},t_{3})))\,\mathsf{in}\,s_{1}&>_{\bot}&\mathsf{E}(\mathsf{C}_{x,y}(t_{1},t_{2},t_{3}))\\\
&>_{P}&\mathsf{C}_{x,y}(t_{1},\mathsf{E}(t_{2}),\mathsf{E}(t_{3}))\\\
\end{matrix}$

The case for the general modal term is proven similarly.

At this point, we can finally state our main results.

######  Theorem 3.7 (Full normalization for $\mathsf{IEL}^{-}$).

$\mathsf{IEL}^{-}$ is strongly normalizing w.r.t. the reduction relation
induced by the union of detour-, permutation-, and $\bot$-conversions.

######  Proof 3.8.

Suppose otherwise. By applying repeatedly lemma 3.5, we would construct an
infinite sequence of $R$-reductions for $R\in\\{D,P\\}$, contra theorem 2.28.
Therefore, we must have an infinite sequence of $\bot$-conversions, but this
is not in the case by proposition 2.31.

######  Corollary 3.9 (Subformula property for $\mathsf{IEL}^{-}$).

Every formula occurring in a normal $\mathsf{IEL}^{-}$-deduction of $A$ from
assumptions $\Gamma$ is a subformula of $A$ or of some formula in $\Gamma$.

######  Proof 3.10.

We use the main theorem and reason as in [11, § II.3].

######  Corollary 3.11.

The calculus $\mathsf{IEL}^{-}$ is decidable.

######  Proof 3.12.

By the subformula property, proof search for $\mathsf{IEL}^{-}$ is bounded by
the complexity of the formula we wish to deduce in the very calculus.

###  3.2 Further properties

Having established both normalization and the subformula principle for
$\mathsf{IEL}$, it is now relatively easy to investigate on some further
proof-theoretic properties of the system.

First recall that a deduction is said to be neutral iff it consists of a
simple assumption, or its last rule is an elimination rule of the natural
deduction calculus.

We immediately have the following fact.

######  Proposition 3.13.

In any normal and neutral $\mathsf{IEL}^{-}$-deduction of $A$ from $\Gamma$,
$\Gamma\not=\varnothing$.

######  Proof 3.14.

Straightforward induction on the height of the deduction.

From this, we can establish a canonicity result for
$\mathsf{IEL}^{-}$-deductions.

######  Lemma 3.15 (Canonicity).

In any normal $\mathsf{IEL}^{-}$-deduction of $A$, the last rule applied is
the introduction rule for the main connective of $A$.

######  Proof 3.16.

By proposition 3.13, since $\Gamma=\varnothing$ here, and the deduction is
normal, its last rule cannot be an elimination.

######  Lemma 3.17 (Consistency).

$\mathsf{IEL}^{-}$ is consistent.

######  Proof 3.18.

Consistency follows from canonicity and full normalization, since if we had a
deduction of $\bot$, we could normalize it and find a canonical proof, but
there is no introduction rule for absurdity in the calculus.

As further corollaries, we can give syntactic proofs of some structural
properties of $\mathsf{IEL}^{-}$.

######  Corollary 3.19.

Reflection rule is admissible in $\mathsf{IEL}^{-}$: If
$\mathsf{IEL}^{-}\vdash\Box A$, then $\mathsf{IEL}^{-}\vdash A$.

######  Corollary 3.20 (Disjunction property).

If $\mathsf{IEL}^{-}\vdash A\vee B$, then $\mathsf{IEL}^{-}\vdash A$ or
$\mathsf{IEL}^{-}\vdash B$.

######  Corollary 3.21 ($\Box$-primality).

If $\mathsf{IEL}^{-}\vdash\Box A\vee\Box B$, then $\mathsf{IEL}^{-}\vdash A$
or $\mathsf{IEL}^{-}\vdash B$.

######  Proof 3.22.

All these results follow by the disjunction property and the admissibility of
the reflection rule.

######  Corollary 3.23 (Weak disjunction property).

If $\mathsf{IEL}^{-}\vdash\Box(A\vee B)$, then $\mathsf{IEL}^{-}\vdash\Box A$
or $\mathsf{IEL}^{-}\vdash\Box B$.

######  Proof 3.24.

If we have a deduction of $\Box(A\vee B)$, the by the reflection rule we have
a deduction of $A\vee B$. By the disjunction property we have a deduction of
$A$ or a deduction of $B$. In each case, by applying the necessitation rule we
have the desired result.

###  3.3 Proof-theoretic semantics

In [10], a categorical semantics for proofs in $\mathsf{IEL}^{-}$ is given. As
stated before, that work was focused on the computational aspects of the
formal system for intuitionistic belief, so that the strong normalization
theorem was established for the reduction relation induced by detour-
conversions with the modal rewritings here recalled in definition 2.1.

Accordingly, that categorical interpretation for our calculus was developed
for $\mathsf{IEL}^{-}$-deductions modulo normalization of the restricted
reduction relation.

The structures we were interested in are then the following one:333The
interested reader in filling all the defining concepts involved in the
definition is referred to e.g. [7].

######  Definition 3.25.

An $\mathsf{IEL}^{-}$-category is given by a bi-Cartesian closed category
$\mathcal{C}$ together with a monoidal pointed endofunctor $\mathfrak{K}$
whose point $\kappa$ is monoidal.

Indeed, it is proven that these structures capture our deductions in a sound
and complete way [10, § 3.2].

Considering the normalization result shown in the present paper, we see that
nothing has to be tweaked from the categorical perspective: the permutation-
and $\bot$-conversions that we have considered here are clearly captured by
the universal property of colimits.444This is another evidence that
permutations for $\vee$ and $\bot$ do not have computational relevance, as we
could have already inferred from the previous results for the CPS translation.
Therefore we can state the following adequacy theorem.

######  Theorem 3.26 (Categorical adequacy).

Given an $\mathsf{IEL}^{-}$-category $\mathcal{C}$, any two
$\mathsf{IEL}^{-}$-deductions which are equal modulo full normalization are
canonically interpreted as $\mathcal{C}$-arrows which are equal. Conversely,
if the interpretation of any two $\mathsf{IEL}^{-}$-deductions is equal in all
$\mathsf{IEL}^{-}$-categories, then the two deductions are equal modulo full
normalization.

######  Proof 3.27.

By what we have just remarked about colimits, we can reason just as in [10, §
3.2].

## Conclusion and related works

In the present paper we have investigated a deduction system for
intuitionistic belief which satisfies many good proof-theoretic properties.

In particular, we have seen that deductions strongly normalise, and that
proofs in normal forms satisfy the subformula principle. From these results,
we have syntactically proven that the logic is consistent and decidable, along
with some structural properties of the system – namely, canonicity;
disjunction property; admissibility of the reflection rule; $\Box$-primality;
weak disjunction property.

As a consequence, we can say to have succeeded in developing a ‘proof-
theoretically tractable’ system for intuitionistic belief that can be easily
turned into a modal $\lambda$-calculus, and that is analytic by design.

Moreover, considering normal deductions w.r.t. both detour elimination and
permutations has shown not to invalidate the categorical interpretation of our
calculus as introduced in [10].

A natural extension of this investigation goes towards intuitionistic
_knowledge_ as presented in [1]. As a matter of fact, having a natural
deduction for belief, it is not hard to extend our system with an elimination
rule corresponding to the principle of intuitionistic factivity of knowledge.

For this extended logic, a cut-free sequent calculus is introduced in [6]. In
that perspective, it might be stimulating to develop a sequent calculus on the
basis of $\mathsf{IEL}^{-}$ – following the strategy of [9] for intuitionistic
logic – and checking the interplay between the Gentzen’s formalisms for both
intuitionistic belief _and_ knowledge. In fact, it is clearly possible to give
a labelled sequent calculus for intuitionistic epistemic states following the
pioneering work of [8], and obtaining interesting results on the structural
behaviour of these modalities by using the powerful insight of formalizing the
relational semantics introduced in [1]. However, what we have just surveyed in
the present paper suggests that sticking to the purely syntactic formalism of
Gentzen’s systems is still a practicable path when dealing with this kind of
logics.

The results contained in [12] – where a natural deduction for intuitionistic
belief is discussed along with algebraic and categorical semantics – are
closer to our viewpoint. Actually, the present author gave talks555Preliminary
results were discussed on May 2019 – during the Logic and Philosophy of
Science seminar at the University of Florence. They were then refined during
the poster session of The Proof Society Summer School at Swansea University on
September 2019, where valuable feedback from the participants made the author
opt for a single ruled calculus. on the normalization and categorical
interpretation for the same calculus there discussed, but soon realised that
having a system with a single rule for the belief modality, though lacking a
certain symmetry, gives a kind of ‘kernel’ that can be easily extended in
several directions – i.e. by using various sorts of elimination rules –
enlarging the perspective on the co-reflection scheme beyond the epistemic
reading. As expected, having a single rule as ours, or adding, as in [12], an
elimination rule to the system for $\mathbb{IK}$ defined in [3] does not
affect the categorical interpretation of the modality.

A fine grained analysis of the pros and cons of those different formal calculi
for the intuitionistic epistemic states remains then among future work.

## References

  * [1] Sergei Artemov and Tudor Protopopescu.  Intuitionistic epistemic logic.  The Review of Symbolic Logic, 9.2:266–298, 2016.
  * [2] Philippe de Groote.  On the strong normalisation of intuitionistic natural deduction with permutation-conversions.  Information and Computation, 178.2:441–464, 2002.
  * [3] Valeria de Paiva and Eike Ritter.  Basic constructive modality.  Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday, pages 411–428, 2011.
  * [4] Yoshihiko Kakutani.  Calculi for intuitionistic normal modal logic.  arXiv preprint arXiv:1606.03180, 2016.
  * [5] Saul A. Kripke.  Semantical analysis of intuitionistic logic i.  In Studies in Logic and the Foundations of Mathematics, volume 40, pages 92–130. Elsevier, 1965.
  * [6] Vladimir N Krupski and Alexey Yatmanov.  Sequent calculus for intuitionistic epistemic logic iel.  In International Symposium on Logical Foundations of Computer Science, pages 187–201. Springer, 2016.
  * [7] Saunders Mac Lane.  Categories for the working mathematician, volume 5.  Springer Science & Business Media, 2013.
  * [8] Sara Negri.  Proof analysis in modal logic.  Journal of Philosophical Logic, 34(5):507–544, 2005.
  * [9] Sara Negri, Jan Von Plato, and Aarne Ranta.  Structural proof theory.  Cambridge University Press, 2008.
  * [10] Cosimo Perini Brogi.  Curry-Howard-Lambek correspondence for intuitionistic belief, 2020\.  arXiv:2006.02417.
  * [11] Dag Prawitz.  Ideas and results in proof theory.  In Studies in Logic and the Foundations of Mathematics, volume 63, pages 235–307. Elsevier, 1971.
  * [12] Daniel Rogozin.  Categorical and algebraic aspects of the intuitionistic modal logic iel—and its predicate extensions.  Journal of Logic and Computation, 31(1):347–374, 2021.
  * [13] Morten H. Sørensen and Pawel Urzyczyn.  Lectures on the Curry-Howard isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 2006.
  * [14] Dirk van Dalen.  Logic and Structure.  Springer, 4th edition, 2008.
  * [15] Dirk van Dalen and Anne Troelstra.  Constructivism in Mathematics. An Introduction I, volume 121 of Studies in Logic and the Foundations of Mathematics.  Elsevier, 1988.