请输入您要查询的字词:

 

单词 Substitutability
释义

substitutability


In any logical system, the way to obtain (well-formed) formulasMathworldPlanetmathPlanetmath from existing ones is by attaching logical connectives to existing ones. For example, in classical propositional logicPlanetmathPlanetmath, if φ and ψ are formulas, the following

φψ,¬φ,ψφ

are formed by attaching logical connectives ,¬, and appropriately to φ and ψ.

Another convenient device is substitution:

replace all occurrences of some symbol x in a formula φ by an expression ψ.

We denote the resulting expression by

φ[ψ/x].

For example, in classical propositional logic, if φ is p(¬rp), then φ[(pq)/p] is

(pq)(¬r(pq))

On the other hand, the expressions

  • φ[¬/p], which is ¬(¬r¬), and

  • φ[q/], which is pq(¬rq),

are not formulas. Thus, one must be careful when performing substitutions on formulas lest the resulting expressions are ill-formed. In other words, conditions must be placed on x and ψ in φ[ψ/x] in order that φ[ψ/x] is a (well-formed) formula. These conditions are called the substitutability conditions. In this entry, we will concentrate on substitutability conditions on predicate logic. Details on substitions in propositional logic can be found in here (http://planetmath.org/SubstitutionsInLogic).

Substitution in First-Order Logic

Substitution works pretty much the same way for first-order logic as in propositional logic. However, the substitutability conditions are more subtle. Take a look at the following example:

x(x=1)

If we replace x by 0, we end up with

0(0=1),

which is non-sensical (not a wff). This is because x occurs in the formula as a bound variableMathworldPlanetmath. (one reason why we distinguish the variables occurring in first order formulas into two types: free and bound).

We now formalize the notion of substitution in first-order logic. There are two parts: substitution for terms, and substitution for formulas.

Definition. For any term t, any symbol x, and any expression s, define t[s/x] inductively, as follows:

  1. 1.

    if t is an individual variable or a constant symbol, then t[s/x] is s if t is x, and t[s/x] is t otherwise;

  2. 2.

    if t is f(t1,,tn), where f is an n-ary function symbol, and each ti is a term, then t[s/x] is f(t1[s/x],,tn[s/x]).

For example, if t is x+y, then t[(x-y)/x] is (x-y)+y.

It is easy to see that s is a term and x an individual variable, then t[s/x] is a term. In additionPlanetmathPlanetmath, by inductionMathworldPlanetmath, one can easily show that if the formula s1=s2 is true, so is the formula t[s1/x]=t[s2/x].

Next, we define substitution for formulas. In light of the last example at the beginning of this section, we need to be a little careful.

Definition. Let φ be a formula, x a symbol, and s an expression. The expression φ[s/x] is again define inductively:

  1. 1.

    if φ is t1=t2, then φ[s/x] is t1[s/x]=t2[s/x];

  2. 2.

    if φ is R(t1,,tn), then φ[s/x] is R(t1[s/x],,tn[s/x]);

  3. 3.

    if φ is ¬ψ, then φ[s/x] is ¬(ψ[s/x]);

  4. 4.

    if φ is ψσ, then φ[s/x] is ψ[s/x]σ[s/x];

  5. 5.

    if φ is yψ, then φ[s/x] is y(ψ[s/x]) if xy, and φ[s/x] is φ otherwise.

Again, substitutions involving logical connectives , , and the universal quantifierMathworldPlanetmath can be derived from the rules given above.

For example, if φ is x(x=yy=z), then φ[t/y] is x(x=tt=z), whereas φ[t/x] is just φ.

Given that φ is a formula, it is easy to see that if x is an individual variable, and s is a term, then φ[s/x] is a formula.

In addition, it is easy to see that sentencesMathworldPlanetmath are not affected by substitutions: if φ is a sentence, then φ[s/x] is just φ. In other words, sentences can not be changed into formulas with free variablesMathworldPlanetmath.

Conversely, can a formula with free variables be changed into a sentence by substitution? Certainly. For example, if φ is

x(y<x),

then φ[x/y] is

x(x<x).

Although syntactically correct, this is undesirable in many situations, particularly when we are interested in the interpretationsMathworldPlanetmathPlanetmath of these formulas. In the example above, we have changed x(y<x), which many very well be true in many interpretations, into x(x<x), something with a fixed meaning (and always false if < is interpreted as the usual less than relationMathworldPlanetmath).

The problem with the situation described in the last paragraph arises because a free variable in t becomes bound in φ[t/x]. To eliminate this undesirable situation, we define the notion of “free for”:

Definition. Let x be an individual variable, t a term, and φ a formula. We define the relationt is free for, or substitutable for x in φ, inductively, as follows:

  1. 1.

    φ is an atomic formula;

  2. 2.

    φ is ¬ψ, and t is free for x in ψ;

  3. 3.

    φ is ψσ, and t is free for x in ψ and in σ;

  4. 4.

    φ is yψ, and either

    • xFV(φ) (x does not occur free in φ), or

    • y does not occur in t, and t is free for x in ψ.

In words, t is free for x in φ iff whenever z is a variable in t, no literal subformula of φ of the form zψ contains an occurrence of x which is free in φ.

For example, f(x,y) is free for x in the following formulas:

P(x,y),P(x)¬Q(z),¬x¬R(x,y),and  ¬S(y)yT(y,z),

but not in the following formulas:

yP(x,y),Q(x)zyR(x,y),and  S(y)y(T(y,y)¬Q(x)).

Given any formula φ, we again write φ(x) to mean that variable x occurs in φ. A substitution instance of φ(x) is just φ[t/x], or φ(t) for short. Furthermore, if t is free for x in φ, then φ(t) is called a free substitution instance of φ(x).

It is easy, by induction, to show that if terms t1 and t2 are free for x in φ, and that the formula t1=t2 is true, the substitution instances φ(t1) and φ(t2) are logically equivalent, as intended.

随便看

 

数学辞典收录了18232条数学词条,基本涵盖了常用数学知识及数学英语单词词组的翻译及用法,是数学学习的有利工具。

 

Copyright © 2000-2023 Newdu.com.com All Rights Reserved
更新时间:2025/5/4 15:09:58