Logique combinatoire symbolique

et application à une logique résistante aux propositions p=~p

• Notations :
  • abc=(ab)c
  • (pt x.a=b) = (lambda x. a = lambda x. b)
  • lambda x. x = I
  • lambda x. y = K y si y ne contient pas x
  • lambda x. (a b) = S (lambda x.a) (lambda x. b)
  • lambda x. (f x) = f

• Axiomes :
  • a=b -> b=a
  • a=b, b=c -> a=c
  • f=g, a=b -> fa=gb
  • I=I
  • K=K
  • S=S
  • Z=Z
  • a=a' -> Ia=a'
  • a=a', b=b' -> Kab=a'
  • a=a', b=b', c=c' -> Sabc=a'c'(b'c')

• Une logique permettant de manipuler des propositions p=~p :
  • Idée : distinguer l'affirmation d'une implication p=!>q (si on a pu démontrer p, alors on peut affirmer q) et l'interrogation p=?>q (en faisant l'hypothèse p, on peut démontrer q)
  • axiomes :
    • Modus ponens : p=!>q, p -> q
    • p =?> p
    • p =!> (q =?> p)
    • (p =?> (q =!> r) ) =!> ((p =?> q) =!> (p =?> r)) - on peut appliquer le modus ponens sous l'hypothèse p

• Représentation en logique combinatoire :
  • Les propositions sont des égalités a=b
  • a=b =*> c=d est représenté par E* a b c = E* a b d
  • ~(a=b) est représenté par E! a b K = E! a b (K I) ou E? a b K = E? a b (K I)
  • les axiomes deviennent :
    • Modus ponens : S E! I = K I ou E! a a b = b
    • pt a. pt b. (E? a b a = E? a b b)
    • le troisième axiome devient inutile
    • pt a. pt b. pt f. pt x. (E? a b (f x) = E? a b f (E? a b x))