def Henkin {n : ℕ} {U : Type} (R : (Fin n → U) → (Fin n → U) → Prop) : Prop

Equations

• Henkin R = ∃ (Y : Fin n → U → U), ∀ (x : Fin n → U), R x fun (k : Fin n) => Y k (x k)

theorem l₀ {U : Sort u_1} (x y : Fin 0 → U) : x = y

theorem l₁ {U : Sort u_1} (a x : Fin 0 → U) (R : (Fin 0 → U) → (Fin 0 → U) → Prop) (y : Fin 0 → U) : R a x → R a y

theorem zero_not_enough : ¬∃ (U : Type), ∃ (R : (Fin 0 → U) → (Fin 0 → U) → Prop), (∀ (x : Fin 0 → U), ∃ (y : Fin 0 → U), R x y) ∧ ¬Henkin R

theorem one_not_enough : ¬∃ (U : Type), ∃ (R : (Fin 1 → U) → (Fin 1 → U) → Prop), (∀ (x : Fin 1 → U), ∃ (y : Fin 1 → U), R x y) ∧ ¬Henkin R