Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I'm studying logic from the Ebbinghaus's book "Mathematical Logic" and when I tried to solve some of the exercises doubt rises.

Given a calculus C consisting of the following rules:

         and        y  t_i
--------     -------------------- if f belongs to S(set of symbol of the language)
 x   x        y  ft_1, .... , t_n      is n-ary and i goes from 1 to n

Show that for all variables x and all S-terms t , xt is derivable from the calculus C IFF x belongs to the set of variables associated to the S-term t VAR(t).

The function VAR - which associates to each S-term the set of variables occurring in it - is defined as:

    VAR(x) := {x}
    VAR(c) := Empty
    VAR(ft_1...t_n) := VAR(t_1) U ... U VAR(t_n)

As I understood I have to show that a certain property P holds, to accomplish this I have to do the following:

    For each rule of the calculus C_a:

             e_1, e_2, ... e_n
    the following must hold:

            whenever e_1,..., e_n are derivable in C_and have a property P
            then e also has P

For the given problem I tried the following:

Property P is defined as P: "x,t belonging to S can be combined in a string of the type xt"

By the "Premise Free" rule we have that VAR(T) = {x} and we can get a string of the type S = xx. This by definition of VAR and x belongs to VAR(T) = {x}.

For the second rule we have that applying the definition of VAR to a string of the type S_1 = y t_i we lead to: VAR(y t_i) = VAR(y) U VAR(t_1) U ... U VAR(t_n) assumed that the derivation is true since both y and t_i belongs to the set VAR(y t_i)

Considering a term composed by t_k where k goes from 1 to n and an n-ary function symbol f belonging to S we have: VAR(f t_k) = VAR(t_1) U VAR(t_2) U ... U VAR(t_n). Having t_1 = x, t_2 = t and k=2 we lead to a string of the type S_2=xt and x belongs to the set of variables associated to the S-terms t_k VAR(t_k).

I would ask you if the method applied to proof waht is above described is correct. I really don't understand if it is may be a correct way to do what is asked in the exercise.

share|cite|improve this question
Welcome to Math.SE! Here's a quick guide on how to write math on this site:… – Newb Oct 31 '13 at 13:17

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.