Complete port of HOL Light FOL compactness material

Also add a finite entailment property:

INFINITE 𝕌(:α) ⇒
(entails (:α) Γ ϕ ⇔ ∃Γ₀. FINITE Γ₀ ∧ Γ₀ ⊆ Γ ∧ entails (:α) Γ₀ ϕ)

You only need a finite number of hypotheses to get to a conclusion.
This is obvious if you have a proof system, but is true thanks to
compactness if you are just working with models.

Complete port of HOL Light material on skolemization

A couple more files to go.

More progress with FOL compactness port

Progress with port of HOL Light compactness etc theories

Start port of material about f.o. compactness from HOL Light

See commit

https://github.com/jrh13/hol-light/commit/013324af7ff715346383fb963d323138cf011732

Thanks to John for making this available (some of it is behind his
TPHOLs 1998 paper.)