FOF Proof

Let ...

Σ be an untyped first-order logic language, consisting of ...
- V_Σ - A set of variables
- F_Σ - A set of function symbols with arity
- P_Σ - A set of predicate symbols with arity
Φ be a formula written in Σ
Ι be an interpretation for Σ, consisting of ...
- D_Ι - A set of domain elements.
- F_Ι - For each element f of F_Σ with arity n, a mapping f^*(D_Ιⁿ) → D_Ι
- R_Ι - For each element p of P_Σ with arity n, a mapping p^*(D_Ιⁿ) → {TRUE,FALSE}
Ι can be a partial interpretation of Σ, but must be enough to interpret Φ.

Click for example

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

Let D_{φ_Ι} be a set of fresh terms, one for each d_i ∈ D_Ι.
Let D_{Ι→φ_Ι} be a mapping from D_Ι → D_{φ_Ι} in correspondence to the above.
Let D_{φ_Ι→Ι} be the inverse mapping from D_{φ_Ι} → D_Ι

Click for example

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

V_Σ' = V_Σ
F_Σ' = F_Σ ∪ D_{φ_Ι}
P_Σ' = P_Σ

Click for example

An interpretation formula φ_Ι is the conjunction of:

D^|_{φ_Ι} - ∀ X (X = d₁ | ... | X = d_n), for all d_i ∈ D_{φ_Ι}
F^&_{φ_Ι} - The conjunction of f(D_{Ι→φ_Ι}(d_iⁿ)) = D_{Ι→φ_Ι}(d), for each (f^*(D_Ιⁿ) → D_Ι) ∈ F_Ι
P^&_{φ_Ι} - The conjunction of p(D_{Ι→φ_Ι}(d_iⁿ)), for each instance of (p^*(D_Ιⁿ) → TRUE) ∈ P_Ι, and ~p(D_{Ι→φ_Ι}(d_iⁿ)), for each (p^*(D_Ιⁿ) → FALSE) ∈ P_Ι

Click for example

fof(phiI,interpretation,
    ( ! [X] : (X = "face" | X = "stickman")
    & ( geoff = "face"
      & brotherOf("face") = "stickman" & brotherOf("stickman") = "face" )
    & ( ~ taller("face","face") & ~ taller("face","stickman")
      & taller("stickman","face") & ~ taller("stickman","stickman") ) ) ).

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

D_Ι' = D_Ι
F_Ι' = F_Ι ∪ D_{φ_Ι→_Ι}
R_Ι' = R_Ι

Click for example

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^&_{φ_Ι}

Click for example

For 😀 ∈ {😀, 🕺}
- X = "face" is an element of the disjunction (X = "face" | X = "stickman")
- With X set to 😀
  😀 = "face" holds iff
  F_Ι'(😀) = F_Ι'("face") iff
  F_Ι'(😀) = D_{φ_Ι→_Ι}("face") iff
  😀 = 😀
- Thus an element of (😀 = "face" | 😀 = "stickman") holds
Analogously for 🕺 ∈ {😀, 🕺}
So for all d' ∈ {😀, 🕺}, an element of the disjunction (X = "face" | X = "stickman") holds, i.e.,
Ι' ⊢ ! [X] : (X = "face" | X = "stickman")
For the element brotherOf("face") = "stickman" of the conjunction
(geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face")
- brotherOf("face") = "stickman" holds iff
  F_Ι'(brotherOf("face")) = F_Ι'("stickman") iff
  brotherOf^*(F_Ι'("face")) = F_Ι'("stickman") iff
  brotherOf^*(D_{φ_Ι→_Ι}("face")) = D_{φ_Ι→_Ι}("stickman") iff
  brotherOf^*(😀) = 🕺
  which holds from the definition of brotherOf^*
- Thus brotherOf("face") = "stickman" holds
- Analogously for the other elements of
  (geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face")
So (geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face") holds, i.e.,
Ι' ⊢ (geoff = "face" & brotherOf("face") = "stickman" & brotherOf("stickman") = "face")
For the element taller("stickman","face") of the conjunction
(~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman"))
- taller("stickman","face") holds iff
  P_Ι'(taller(F_Ι'("stickman","face"))) iff
  taller^*(F_Ι'("stickman","face")) iff
  taller^*(D_{φ_Ι→_Ι}("stickman","face")) iff
  taller^*(🕺,😀)
  which holds from the definition of taller^*
- Analogously for the other elements of
  (~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman"))
So (~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman")) holds, i.e.,
Ι' ⊢ (~ taller("face","face") & ~ taller("face","stickman") & taller("stickman","face") & ~ taller("stickman","stickman"))

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 Ι ⊢ Φ

Click for example