Documentation

Marginis.PaulyZiegler2013

def Henkin {n : } {U : Type} (R : (Fin nU)(Fin nU)Prop) :
Equations
  • Henkin R = ∃ (Y : Fin nUU), ∀ (x : Fin nU), R x fun (k : Fin n) => Y k (x k)
theorem l₀ {U : Sort u_1} (x : Fin 0U) (y : Fin 0U) :
x = y
theorem l₁ {U : Sort u_1} (a : Fin 0U) (x : Fin 0U) (R : (Fin 0U)(Fin 0U)Prop) (y : Fin 0U) :
R a xR a y
theorem zero_not_enough :
¬∃ (U : Type) (R : (Fin 0U)(Fin 0U)Prop), (∀ (x : Fin 0U), ∃ (y : Fin 0U), R x y) ¬Henkin R
theorem one_not_enough :
¬∃ (U : Type) (R : (Fin 1U)(Fin 1U)Prop), (∀ (x : Fin 1U), ∃ (y : Fin 1U), R x y) ¬Henkin R