### Abstract

We formulate classical propositional logic as an axiom class. Our class represents a Hilbert-style proof system with the axioms \(\vdash \varphi \to \psi \to \varphi\), \(\vdash (\varphi \to \psi \to \chi) \to (\varphi \to \psi) \to \varphi \to \chi\), and \(\vdash ((\varphi \to \bot) \to \bot) \to \varphi\) along with the rule modus ponens \(\vdash \varphi \to \psi \Longrightarrow \; \vdash \varphi \Longrightarrow \; \vdash \psi\). In this axiom class we provide lemmas to obtain Maximally Consistent Sets via Zorn's lemma. We define the concrete classical propositional calculus inductively and show it instantiates our axiom class. We formulate the usual semantics for the propositional calculus and show strong soundness and completeness. We provide conventional definitions of the other logical connectives and prove various common identities. Finally, we show that the propositional calculus embeds into any logic in our axiom class.

### License

BSD License

### Topics

- Logic/General logic/Classical propositional logic
- Logic/Proof theory

### Session Propositional_Logic_Class

- Implication_Logic
- Classical_Logic
- Classical_Logic_Completeness
- List_Utilities
- Classical_Connectives

### Used by

- Suppes' Theorem For Probability Logic

## Cite

×

Propositional_Logic_Class-AFP

    @article{Propositional_Logic_Class-AFP,
      author  = {Matthew Doty},
      title   = {Class-based Classical Propositional Logic},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Propositional_Logic_Class.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Jan 11, 2023 : Isabelle2022