First order logic - why do we need function symbols?Employing function symbols in first order logic necessitates us to delineate "terms" inductively, which renders many proofs more extensive and considerably more irksome. Of course, function symbols simplify matters when trying to use first order logic to describe things, but on the surface it seems to me they could be replaced completely by relations: Instead of f use a relation R f such that instead of writing φ ( f ( x ) ) write ( ∀ x ∃ ! y ( R ( x , y ) ) ∧ R ( x , y ) ∧ φ ( y ). Now use f ( x ) as a shorthand notation, so you can use it in "real life" but avoid it in proofs.I guess I'm missing some deep neccecity here, but what?(The same goes for constant symbols, but they don't really complicate things as function symbols do).

Question

First order logic - why do we need function symbols?Employing function symbols in first order logic necessitates us to delineate &quot;terms&quot; inductively, which renders many proofs more extensive and considerably more irksome. Of course, function symbols simplify matters when trying to use first order logic to describe things, but on the surface it seems to me they could be replaced completely by relations: Instead of     f use a relation       R    f   such that instead of writing   φ  (  f  (  x  )  ) write (  ∀  x  ∃  !  y  (  R  (  x  ,  y  )  )  ∧  R  (  x  ,  y  )  ∧  φ  (  y  ). Now use   f  (  x  ) as a shorthand notation, so you can use it in &quot;real life&quot; but avoid it in proofs.I guess I&#039;m missing some deep neccecity here, but what?(The same goes for constant symbols, but they don&#039;t really complicate things as function symbols do).

kujikazag2h · Accepted Answer

You can always take a first-order theory with constants and function symbols and replace it with a theory using only relation symbols. This is at the expense of complicating the theory, since if, for example, R is the relational symbol representing the binary functional symbol f, we need an axiom of the form  (  ∀  x  )  (  ∀  y  )  (  ∃  z  )  (  ∀  u  )  (  R  (  x  ,  y  ,  u  )  ↔  u  =  z  )  .But since R and f are definable from one another, there would be a natural translation of theorems of one theory into the other.Another expense is the statement of certain theorems of model theory. For example, a theory T is said to admit elimination of quantifiers if for every formula   ϕ  (      x    1    ,  …      x    n    ) there is a quantifier-free formula   ψ  (      x    1    ,  …      x    n    ) such that  T  ⊢  (  ∀      x    1    )  ⋯  (  ∀      x    n    )  (  ϕ  ↔  ψ  )  .The basic example of a theory admitting elimination of quantifiers is the theory of real closed fields. Note that if the underlying language has no constant symbols, then there are no quantifier-free sentences, and therefore no theory without constant symbols can admit elimination of quantifiers. One would have to alter the definition so as to only concern those formulas   ϕ with at least one free variable. One can show that this would be faithful, but it is also a somewhat less natural definition.

Answered question

Answer & Explanation

New Questions in High school geometry