3
$\begingroup$

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)$$

$\endgroup$
1
  • $\begingroup$ I was confused by THIS EXACT SAME ISSUE!!! Same exercise, same everything lol thank you guy from over almost 13 years ago. $\endgroup$ Commented Dec 1, 2023 at 3:14

1 Answer 1

3
$\begingroup$

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\}\;.$$

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.

$\endgroup$
2
  • $\begingroup$ math.stackexchange alerted me to this thread when I was composing my latest one. It turns out that the original question above had a MathJax error. After I fixed the error, some of your answer did not correspond to the question, so I edited your answer as well. I hope you're OK with these edits. $\endgroup$
    – kjo
    Commented Mar 26, 2022 at 14:51
  • 1
    $\begingroup$ @kjo: Yes, that’s fine; thank you. $\endgroup$ Commented Mar 26, 2022 at 19:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .