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 = [*]