Formalizing Axiomatic Systems

Asta Halkjær From, Agnes Moesgård Eschen & Jørgen Villadsen (DTU Compute)

We describe 12 axiomatic systems for classical propositional logic with soundness and completeness theorems formalized in the proof assistant Isabelle/HOL.

The Isabelle/HOL Formalization

1. Install Isabelle (link to Isabelle website)
2. Unzip the 13 Isabelle theory files (link to zip file)
3. Open the "Systems" theory file (link to introductory video)

The 12 Axiomatic Systems

Frege

p → ( q → p )

( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )

( p → q ) → ( ¬ q → ¬ p )

¬ ¬ p → p

p → ¬ ¬ p

Hilbert

p → ( q → p )

( p → ( q → r ) ) → ( q → ( p → r ) )

( q → r ) → ( ( p → q ) → ( p → r ) )

p → ( ¬ p → q )

( p → q ) → ( ( ¬ p → q ) → q )

Łukasiewicz 1

( p → q ) → ( ( q → r ) → ( p → r ) )

( ¬ p → p ) → p

p → ( ¬ p → q )

Łukasiewicz 2

( ( p → q ) → r ) → ( ¬ p → r )

( ( p → q ) → r ) → ( q → r )

( ¬ p → r ) → ( ( q → r ) → ( ( p → q ) → r ) )

Łukasiewicz 3

p → ( q → p )

( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )

( ¬ p → ¬ q ) → ( q → p )

Łukasiewicz Variant

( p → q ) → ( ( q → r ) → ( p → r ) )

( ¬ p → q ) → ( ( q → p ) → p )

p → ( ¬ p → q )

Mendelson

p → ( q → p )

( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )

( ¬ p → ¬ q ) → ( ( ¬ p → q ) → p )

Mendelson Variant

p → ( q → p )

( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )

( ¬ p → q ) → ( ( ¬ p → ¬ q ) → p )

Russell

p → ( q → p )

( p → q ) → ( ( q → r ) → ( p → r ) )

( p → ( q → r ) ) → ( q → ( p → r ) )

¬ ¬ p → p

( p → ¬ p ) → ¬ p

( p → ¬ q ) → ( q → ¬ p )

Sobociński 1

¬ p → ( p → q )

p → ( q → ( r → p ) )

( ¬ p → r ) → ( ( q → r ) → ( ( p → q ) → r ) )

Sobociński 2

( p → q ) → ( ¬ q → ( p → r ) )

p → ( q → ( r → p ) )

( ¬ p → q ) → ( ( p → q ) → q )

Sobociński Variant

¬ q → ( ( p → q ) → ( p → r) )

p → ( q → ( r → ( s → p ) ) )

( ¬ p → q ) → ( ( p → q ) → q )

References

https://en.wikipedia.org/wiki/List_of_Hilbert_systems

https://github.com/logic-tools/axiom