View file src/slc/contrad-new.prf - Download

# Logical axioms
! MP ^p ^q (imp p q (p q) = [*])  # Modus ponens
! AI ^p (imp p p = [*])
! AK ^p ^q (imp p (imp q p) = [*])
! AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*])

! Y [[* *] ['* (* *)]]  # Fixed point
! defc (c = Y [imp * false])  

! Ac ( \\\defc ; imp \defc false )  # c = (c => false)

# Proof of false 
# This is a Proof Logic version of the following natural deduction proof :
# 1 | c (hypothesis)
#   |---------------
# 2 | c => false (from 1 because c = (c => false))
# 3 | false (MP 2 1)
# 4 c => false (hypothesis 1 3)
# 5 c (from 4 because c = (c => false))
# 6 false (MP 4 5)

! L1 (AI c) 
! L2 (imp c Ac) 
! L3 ( L2 ; L1 ) 
! L4 (AS c c false)
! L5 (MP (imp c (imp c false)) (imp (imp c c) (imp c false))) 
! L6 (L4 ((imp c (imp c false)) (imp (imp c c) (imp c false)))) 
! L7 ( L6 ; L5 )
! L8 (L3 (imp (imp c c) (imp c false))) 
! L9 ( L8 ; L7 ) 
! L10 (MP (imp c c) (imp c false)) 
! L11 (L9 ((imp c c) (imp c false))) 
! L12 ( L11 ; L10 ) 
! L13 (L1 (imp c false)) 
! L14 ( L13 ; L12 ) 
! L15 ( Ac ; c ) 
! L16 ( L15 ; L14 ) 
! L17 (MP c false) 
! L18 (L14 (c false)) 
! L19 ( L18 ; L17 ) 
! L20 (L16 false) 
! L21 ( L20 ; L19 ) 
! T ( false ; L21 )
T  # false = [*]