pathterminuspages/logic/aboutcontactabout me

Syntax

31.01.2021

Contents/Index

1. Introduction
2. Propositional Extension
@3. Syntax
4. Semantics
5. Natural Deduction
6. Equivalences

First we introduce the grammar of predicate logic. We have the notion of terms, these are variables, constants and functions. That is

  • Any variable $x,y, \dots$ is a term.
  • Any constant $c$ is a term.
  • If $t_1, t_2 ,\dots , t_n$ are terms, and $f$ is a function of arity $n \geq 1$, then $f(t_1,t_2, \dots , t_n)$ is a term.

Nothing else is a term.

We can now turn our attention to formulas. We have that

  • If $P$ is a predicate symbol of arity $n \geq 1$, and $t_1, t_2 , \dots , t_n$ are terms, then $P(t_1,t_2,\dots , t_n)$ is a formula.
  • If $\phi$ is a formula, then so is $\neg \phi$.
  • If $\phi,\psi$ are formulas, then so are $\phi \land \psi,\phi \lor \psi, \phi \rightarrow \psi$.
  • If $\phi$ is a formula, then so is $(\phi)$.
  • If $\phi$ is a formula and $x$ is a variable, then $\exists x . \phi$ and $\forall x . \phi$ are formulas.

Nothing else is a formula. Again a predicate symbol of arity 0 is the same as a propositional atom. However we do not concern our self with these in this grammar. Note that the arguments of a predicate needs be a term. Hence this logic is of first order. If we allow formulas as arguments, the order is higher. We have that $\forall$ and $\exists$ binds as tight as $\neg$. The rest is as for propositional logic. That is

  • $\neg,\forall x, \exists x$ binds the tightest.
  • $\land,\lor$ binds the next tightest.
  • $\rightarrow$ binds the least tight. This operator is right-associative.

Free and bound variables

The notion of free and bound variables is closely related to that of a scope. We can visualize the idea by drawing parse trees. However I'm somewhat reluctant to do this. The quantifiers $\forall$ and $\exists$ goes into a single branch in the tree. A predicate $P(t_1,t_2,\dots,t_n)$ goes into $n$ branches. If we from any of these terms, $t_i$, can walk up the tree and reach a quantifier that uses this given term, for example $\forall t_i$, then $t_i$ is said to be bound. Otherwise $t_i$ is said to be free. The scope of a quantifier is just the subtree for which this quantifier is the root.

We mark the scope with parentheses, for example $$ (\forall x . P(x) \land Q(x)) \lor \neg P(x) $$ Here $x$ is in the scope of the forall quantifier for $P,Q$. However $x$ in the formula $\neg P(x)$ is free.

Substitution

We often want to substitute a free variable with a term. This term can be of any complexity, for example a function that takes other terms as arguments.

Definition

Given a formula $\phi$, a term $t$ and a variable $x$, we define $\phi[t/x]$ to be the formula obtained by replacing each free occurrence of $x$ with $t$.

The notion $\phi[t/x]$ is not part of the grammar (and hence not part of the language), however $\phi$ with all free occurrences of $x$ replaced with $t$ is part of the grammar.

Again exemplifying this notion requires drawings of parse trees. Which I'm not doing right now :-).

Free for $x$ in $\phi$

Problems can arise when substituting. Say we have the term $t = f(y,y)$. Since $t$ is a term, it cannot contain a quantifier, hence $y$ is free. Say we do $(\exists y . P(x) \lor P(y))[t/x]$. The result is $(\exists y . P(f(y,y)) \lor P(y))$. But now the term $y$ in $f(y,y)$ is bound by the quantifier $\exists$. To deal with this we introduce the definition of being free for.

Definition

Let $t$ be a term, $x$ be a variable and $\phi$ a formula. We say that $t$ is free for $x$ in $\phi$ if no variable $y$ in $t$ will be bound by a quantifier after substituting $x$ with $t$ in $\phi$. That is after $\phi[t/x]$.

CommentsGuest Name:Comment: