10
$\begingroup$

Using function symbols in first order logic forces us to define "terms" inductively, which makes many proofs longer and much more tedious. 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 $\varphi(f(x))$ write ($\forall x\exists! y(R(x,y))\wedge R(x,y)\wedge\varphi(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).

  • 0
    You can most likely replace functions and constants with predicates, but first order logic is full of notational redundancies that make life easier, such as having both $\exists$ and $\forall$, as well as both $\wedge$ and $\vee$, $\to$, etc.2012-03-29
  • 1
    That only amplifies the point. Usually in the formal definition of FOL most of these symbols are ommited and used only for notational convenience, and the proofs only deal with the minimal set of symbols required. This is not the case for function symbols.2012-03-29
  • 0
    I think you might get into some syntactic trouble if you don't use terms, i.e. omitting functions really changes the feel of first order logic.2012-03-29
  • 0
    Isaac, this is my guess as well, but I'd love to see a concrete example.2012-03-29
  • 0
    Fair enough. I suppose a good example would be that your definition of "quantifier free" would be ridiculously convoluted, and quantifier elimination is really important in model theory and first order logic.2012-03-29
  • 0
    The question is whether you want to talk about structures or models (and theories). If you don't want to talk about theories (yet) then you cannot easily avoid constants and functions, because you'd like the interpretation to somehow be reasonable. If you have theories and are looking at models of them, you can of course replace constants and functions by predicates and add axioms which assert that this predicate has only one element satisfying it; and that predicate has functionality; and this predicate is going to buy a case of beer and a bottle of arak; and so on...2012-03-29
  • 0
    But must I add axioms? Can't I simply adjoin the axioms to any sentence that uses the "function", like in my sketch above?2012-03-29
  • 0
    But then you de facto limit your language, you suddenly cannot write "$\forall x\exists y(R(x,y))$" just like that, you need to verify that $R$ is not a function symbol in disguise. I'd take a language which is abundant over a language which is restrictive in such way.2012-03-29
  • 0
    For proving the Completeness Theorem, function symbols, constant symbols, are awfully handy, since in essence we construct the model out of (equivalence classes of) terms, in fact we introduce Skolem functions precisely to get rid of existential quantifiers.2012-03-29

2 Answers 2