Levin's and Prucnal's theorems on Medvedev's logic of finite problems

TL;DR

This paper offers a clear, unified presentation of existing proofs regarding Medvedev's logic of finite problems, highlighting their shared foundation without introducing new results.

Contribution

It simplifies and unifies the presentation of classical theorems on Medvedev's logic, making the proofs more accessible by emphasizing their common basis.

Findings

Proof of the structural completeness of Medvedev's logic

Medvedev's logic as the largest extension of Kreisel-Putnam logic with disjunction property

Unified presentation of Levin's and Prucnal's theorems

Abstract

The purpose of this note is to provide a transparent and unified retelling of both Skvortsov's proof of the structural completeness of Medvedev's logic of finite problems, which is a classical result originally due to Prucnal, and of Levin's proof that Medvedev's logic of finite problems is the largest extension of the (weak) Kreisel-Putnam logic with the disjunction property. Presenting both results together allows us to simplify their presentation, as they both hinge on the same lemma. There is no novel content in this note, its purpose is merely to present the material in a more accessible way.