drawing tableaus for predicate logic?

55 Views Asked by At

I'm a bit confused about the rules. I know for existential ones, you replace the variable with a new constant and for universal you replace it with a closed term. $\forall x A(x) \to A(t)$ if $t$ is substitutable for $x$ in $A$.

But i dont understand what it means by a closed term. and how do u know if its substitutable? can u replace it with other variables used in the original formula, functions, new constants? any detailed examples would be great!

thanks

1

There are 1 best solutions below

2
On

A term is a variable or a constant or it is built up from already existsing terms and a function symbols.

A closed term is a term without variables: terms have no quantifiers; thus, an occurrence of a variable in a term is always free.

Examples of closed terms in the language of arithmetic are the constants $0$ and $1$ and the term $0+1$, built up from them with the function $+$.

If a term $t$ is closed it is always substitutable for $x$ in $∀xA(x) \to A(t)$.

The proviso about substitutability [for a formal definition, see: Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 113] is required in order to avoid that, substituting a term $t$ with a variable inside (e.g. $y$) in place of $x$ into $\forall x A(x)$, the (free) occurrence of $y$ into $t$ will be "captured" by a quantifier $\forall y$ present into $A$.

If $t$ is closed, there are no variables, and thus no free occurrences of them, and thus no danger of "unwanted capturing".

Consider the following example:

$\forall x \exists y \ (x < y)$,

which is true in $\mathbb N$.

Here $A(x)$ is $\exists y \ (x < y)$ and, according to the definition, $t$ is not substitutable for $x$ in $A$. Why ?

Because the result of the substitution would be:

$\exists y \ (y < y)$

which is clearly false.