# Intuitionistic Propositional Logic in Lean

Preprint · Dafina Trufaş

- Archive id: arxiv:2410.23765
- Published: 2024-10-31
- Venue: EPTCS 410, 2024, pp. 133-149
- DOI: https://doi.org/10.4204/eptcs.410.9
- arXiv: https://arxiv.org/abs/2410.23765
- Source URL: https://arxiv.org/abs/2410.23765
- PDF: https://arxiv.org/pdf/2410.23765
- Provenance: arxiv

## Abstract

In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.