Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

What is the meaning of the white space in the following notation (or what is meant by the rules themselves)?

$$\frac{ }{x\ \ \ x}$$

or

$$\frac{y\ \ \ t_i}{y\ \ \ ft_1...t_n}$$

Where the white space occurs between the variables in rule 1 and the variable and terms in rule two.

I'm self studying from Mathematical Logic by Ebbinghaus, Flum, and Thomas. This particular notation appears on page 23, in Exercise 4.6.

Further background. In a preface comment to Exercise 4.6, the book says: "A means of defining the preceding notions by calculi is indicated in the following exercise". The calculi is what I gave above, and the preceding notions are given below, where the function var "associates with each S-term the set of variables occuring in it":

$$\operatorname{var}(x) :={x}$$ $$\operatorname{var}(c) := \emptyset$$ $$\operatorname{var}(ft_1 \ldots t_n):= \operatorname{var}(t_1)\cup \cdots \cup \operatorname{var}(t_n)$$

share|improve this question

1 Answer 1

up vote 0 down vote accepted

My best guess, given the context, is that the white space should be read as is a variable of. The horizontal line means that the statement below it can be derived from the one above it. Thus, the first rule says that without any prior assumptions one may always conclude that $x$ is a variable of $x$; this matches the rule $$\operatorname{var}(x):=x\;.$$

(Note that this definition is defective: it should read $\operatorname{var}(x)=\{x\}$, as otherwise the final rule makes no sense.)

The second rule says that if $y$ is a variable of $t_i$, then $y$ is a variable of $ft_1\dots t_n$, matching the rule $$\operatorname{var}(ft_1\dots t_n):=\operatorname{var}(t_1)\cup\dots\cup\operatorname{var}(t_n)\;.$$

The point is apparently that the recursive definition of $\operatorname{var}(\varphi)$, the set of variables occurring in $\varphi$, can be replaced by a Gentzen-style calculus that does essentially the same thing.

share|improve this answer

Your Answer

 
discard

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.