#
d534a500 |
|
07-Aug-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|