• Σ be a typed first-order logic language, consisting of ...
  • T_Σ - A set of types
  • V_Σ - A set of variables with types from T_Σ
  • F_Σ - A set of function symbols with signatures from T_Σ
  • P_Σ - A set of predicate symbols with signatures from T_Σ
• Φ be a formula written in Σ
• Ι be an interpretation for Σ, consisting of ...
  • T_Ι - A set of domain types, one for each t ∈ T_Σ
    
    • Let T_Ι→Σ be the type mapping from T_Ι → T_Σ in correspondence to the above.
    • Let T_Σ→Ι be the inverse mapping from T_Σ → T_Ι
  • D_Ι(t) - Sets of domain elements, one for each t ∈ T_Ι
  • F_Ι - For each element f of F_Σ with signature s and arity n, a mapping f^*(D_Ιⁿ) → D_Ι that respects s according to T_Σ→Ι
  • R_Ι - For each element p of P_Σ with signature s and arity n, a mapping p^*(D_Ιⁿ) → {TRUE,FALSE} that respects s according to T_Σ→Ι
  Ι can be a partial interpretation of Σ, but must be enough to interpret Φ.

In the TPTP World an infinite interpretation Ι is represented by an interpretation formulae φ_Ι.

• Let T_φΙ(t) be a set of domain types, one for each t ∈ T_Ι
  
  • Let T_φΙ(t)→Ι be the type mapping from T_φΙ(t) → T_Ι in correspondence to the above.
  • Let T_Ι→φΙ(t) be the inverse mapping from T_Ι → T_φΙ(t)
  • Let T_φΙ(t)→Σ be the type mapping from T_φΙ(t) → T_Σ = T_φΙ(t)→Ι º T_Ι→Σ
  • Let T_Σ→φΙ(t) be the inverse mapping from T_Σ → T_φΙ(t) = T_Σ→Ι º T_Ι→φΙ(t)
• Let D_φΙ(t) be sets of fresh terms of type t ∈ T_φΙ(t), containing one term for each d_i ∈ D_{Ι(TφΙ(t)→Ι(t))}.
  • Let T_φΙ(t)↑Σ be type promotion bijections from D_φΙ(t) → Θ(t), where Θ(t) is set of terms of type T_φΙ(t)→Σ(t)), for each t ∈ T_φΙ(t)
• Let D_Ι→φΙ(t) be mappings from D_Ι(t) → D_φΙ(t), for each t ∈ T_Ι, in correspondence to the above.
• Let D_φΙ→Ι(t) be the inverse mappings from D_φΙ(t) → D_Ι(t), for each t ∈T_φΙ(t)

Define the typed first-order logic language Σ' for φ_Ι,consisting of ...

• T_Σ' = T_Σ ∪ T_φΙ(*)
• V_Σ' = V_Σ
• F_Σ' = F_Σ ∪ D_φΙ(*)
• P_Σ' = P_Σ

Let T_φΙ be the type declarations for T_Σ' and T_φΙ(*)↑Σ These are given first in a TPTP format interpretation. An interpretation formula φ_Ι is the conjunction of:

• Inj_φΙ(t) - ∀ V:t ∃ D:T_Σ→Ι(t) (V = T_Ι↑Σ(t)(D)), for each t ∈ T_Σ
  Sur_φΙ(t) - ∀ D1:t D2:t ((T_Ι↑Σ(t)(D1) = T_Ι↑Σ(t)(D2)) ⇒ (D1 = D2)), for each t ∈ T_Σ
  
• D^|_φΙ(t) - ∀ X:t (X = d₁ | ... | X = d_n), for all d_i ∈ D_φΙ(t), for each t ∈ T_Σ
  
• F^&_φΙ - The conjunction of f(T_Ι↑Σ(*)(D_Ι→φΙ(d_iⁿ))) = T_Ι↑Σ(*)(D_Ι→φΙ(d)), for each (f^*(D_Ιⁿ) → D_Ι) ∈ F_Ι
• P^&_φΙ - The conjunction of p(T_Ι↑Σ(t)(D_Ι→φΙ(d_iⁿ))), for each instance of (p^*(D_Ιⁿ) → TRUE) ∈ P_Ι, and ~p(T_Ι↑Σ(t)(D_Ι→φΙ(d_iⁿ))), for each (p^*(D_Ιⁿ) → FALSE) ∈ P_Ι

Define the interpretation Ι' for Σ', consisting of ...

• D_Ι' = D_Ι
• F_Ι' = F_Ι ∪ D_φΙ→Ι
• R_Ι' = R_Ι

Lemma 1
Ι' ⊢ φ_Ι, or equivalently, Ι' ⊢ D^|_φΙ, and Ι' ⊢ F^&_φΙ, and Ι' ⊢ P^&_φΙ
Proof

• For each d' ∈ D_Ι'
  • X = D_Ι→φΙ(d') is an element of the disjunction in D^|_φΙ,
  • With X set to d'
    d' = D_Ι→φΙ(d') holds iff
    F_Ι'(d') = F_Ι'(D_Ι→φΙ(d')) iff
    F_Ι'(d') = D_φΙ→Ι(D_Ι→φΙ(d')) iff
    d' = d'
    
  • Thus an element of the disjunction in D^|_φΙ holds
  So for all d' ∈ D_Ι', an element of the disjunction in D^|_φΙ holds, i.e., Ι' ⊢ D^|_φΙ
• For each element f(D_Ι→φΙ(d_iⁿ)) = D_Ι→φΙ(d) of the conjunction F^&_φΙ
  • f(D_Ι→φΙ(d_iⁿ)) = D_Ι→φΙ(d) holds iff
    F_Ι'(f(D_Ι→φΙ(d_iⁿ))) = F_Ι'(D_Ι→φΙ(d)) iff
    f^*(F_Ι'(D_Ι→φΙ(d_iⁿ))) = F_Ι'(D_Ι→φΙ(d)) iff
    f^*(D_φΙ→Ι(D_Ι→φΙ(d_iⁿ))) = D_φΙ→Ι(D_Ι→φΙ(d)) iff
    f^*(d_iⁿ) = d
    which holds from the definition of f^*
  • Thus every element of the conjunction F^&_φΙ holds
  So F^&_φΙ holds, i.e., Ι' ⊢ F^&_φΙ
• For each positive element p(D_Ι→φΙ(d_iⁿ)) of the conjunction P^&_φΙ
  • p(D_Ι→φΙ(d_iⁿ)) holds iff
    P_Ι'(p(F_Ι'(D_Ι→φΙ(d_iⁿ))) iff
    p^*(F_Ι'(D_Ι→φΙ(d_iⁿ))) iff
    p^*(D_φΙ→Ι(D_Ι→φΙ(d_iⁿ))) iff
    p^*(d_iⁿ) → TRUE
    which holds from the definition of p^*
  • Thus every positive element of the conjunction P^&_φΙ holds
  • Analogously, every negative element of the conjunction P^&_φΙ holds
  So P^&_φΙ holds, i.e., Ι' ⊢ P^&_φΙ

Theorem
if φ_Ι ⊨ Φ then Ι ⊢ Φ
(this is adequate for the verification task, but needs "iff" for the evaluation task)

Proof

• If φ_Ι ⊨ Φ then Ι' ⊢ Φ
  because every model of φ_Ι is a model of Φ, and Ι' is a model of φ_Ι by the Lemma
• Ι' ⊢ Φ iff Ι ⊢ Φ
  because Φ contains nothing from D_φΙ and Ι' is the same as Ι wrt all other symbols.
• Thus if φ_Ι ⊨ Φ then Ι ⊢ Φ