View file src/slc/contrad.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 = [*]