Junk

• Individual constants and variables are terms of L.
• If α is an n-place function symbol and τ₁, …, τ_n are terms, then (α τ₁ … τ_n) is a term.
• If τ and τ′ are terms, then (= τ τ′) is a formula of L.
• If π is an n-place predicate and τ₁, …, τ_n are terms, then (π τ₁ … τ_n) is an (atomic) formula.
• (not φ ψ) is a formula of L if φ.
• (and φ ψ) is a formula of L if φ and ψ are. Similarly for the operators or, if, and iff.
• If ν is a variable, then (forall (ν) φ) and (exists (ν φ) are formulas of L if φ is.

Let Trm_L be the terms of L. An interpretation I for L is a 3-tuple 〈D,ext,V〉 satisfying the following conditions. First, D = A ∪ R is a nonempty set such that A ∩ R = ∅. Intuitively, A represents the set of individuals of I and R the set of relations-in-intension (though, as will be seen, it is possible to think of them extensionally as sets). ext is a function from D into D*, though we stipulate that, for all a ∈ A, ext(a) = ∅. Intuitively, ext represents the extension of every relation. However, to smooth the semantics for the highly unrestricted syntax of CL languages, in which there is no syntactic distinction between individual constants and predicates, the individuals of D are assigned extensions as well, albeit always empty ones — thus, the result of predicating one individual of another, while semantically meaningful, will always yield falsehood. ***** Specifically, given an FO language L₁ we will define a mapping * from L₁ into a corresponding CL₁ language L_CL and a mapping from any interpretation M for L₁ into a corresponding interpretation M_CL such that a sentence φ of L is true in M iff φ* is true in M_CL. We will also show a directly analogous result for any given CL₁ language. ***** φ is valid₁ iff φ* is a consequence of Γ. It

[Prove this by showing that the models of Γ are exactly the L₁-agreeable interpretations.] ***** Because we can do away with n-place function symbols in favor of n+1-place predicates, for simplicity (and without loss of generality) we will only consider TFO sublanguages containing no function symbols (i.e., languages where the f-arity function is empty).