Movatterモバイル変換

Substitution (logic)

From Wikipedia, the free encyclopedia

Concept in logic

Asubstitution is asyntactic transformation onformal expressions.Toapply a substitution to anexpression means to consistently replace its variable, or placeholder, symbols with other expressions.^{[citation needed]}

The resulting expression is called asubstitution instance, orinstance for short, of the original expression.

Propositional logic

[edit]

Definition

[edit]

Whereψ andφ representformulas ofpropositional logic,ψ is asubstitution instance ofφif and only ifψ may be obtained fromφ by substituting formulas forpropositional variables inφ, replacing each occurrence of the same variable by an occurrence of the same formula. For example:

ψ: (R → S) & (T → S)

is a substitution instance of

φ: P & Q

That is,ψ can be obtained by replacing P and Q inφ with (R → S) and (T → S) respectively. Similarly:

ψ: (A ↔ A) ↔ (A ↔ A)

is a substitution instance of:

φ: (A ↔ A)

sinceψ can be obtained by replacing each A inφ with (A ↔ A).

In somededuction systems for propositional logic, a new expression (aproposition) may be entered on a line of a derivation if it is a substitution instance of a previous line of the derivation.^[1]^{[failed verification]} This is how new lines are introduced in someaxiomatic systems. In systems that userules of transformation, a rule may include the use of asubstitution instance for the purpose of introducing certain variables into a derivation.

Tautologies

[edit]

A propositional formula is atautology if it is true under everyvaluation (orinterpretation) of its predicate symbols. If Φ is a tautology, and Θ is a substitution instance of Φ, then Θ is again a tautology. This fact implies the soundness of the deduction rule described in the previous section.

First-order logic

[edit]

Infirst-order logic, asubstitution is a total mappingσ:V →T fromvariables toterms; many,^[2]^: 73^[3]^: 445 but not all^[4]^: 250 authors additionally requireσ(x) =x for all but finitely many variablesx. The notation {x₁ ↦ t₁, …,x_k ↦ t_k }^{[note 1]}refers to a substitution mapping each variablex_i to the corresponding termt_i, fori=1,…,k, and every other variable to itself; thex_i must be pairwise distinct. Most authors additionally require each termt_i to be syntactically different fromx_i, to avoid infinitely many distinct notations for the same substitution.Applying that substitution to a termt is written inpostfix notation ast {x₁ ↦ t₁, ...,x_k ↦ t_k }; it means to (simultaneously) replace every occurrence of eachx_i int byt_i.^{[note 2]} The resulttσ of applying a substitutionσ to a termt is called aninstance of that termt.For example, applying the substitution {x ↦ z,z ↦ h(a,y) } to the term

f(	z	,a,g(	x	),y)	yields
f(	h(a,y)	,a,g(	z	),y)	.

Thedomaindom(σ) of a substitutionσ is commonly defined as the set of variables actually replaced, i.e.dom(σ) = {x ∈V |xσ ≠x }.A substitution is called aground substitution if it maps all variables of its domain toground, i.e. variable-free, terms.The substitution instancetσ of a ground substitution is a ground term if all oft's variables are inσ's domain, i.e. ifvars(t) ⊆dom(σ).A substitutionσ is called alinear substitution iftσ is alinear term for some (and hence every) linear termt containing precisely the variables ofσ's domain, i.e. withvars(t) =dom(σ).A substitutionσ is called aflat substitution ifxσ is a variable for every variablex.A substitutionσ is called arenaming substitution if it is apermutation on the set of all variables. Like every permutation, a renaming substitution σ always has aninverse substitutionσ⁻¹, such thattσσ⁻¹ =t =tσ⁻¹σ for every termt. However, it is not possible to define an inverse for an arbitrary substitution.

For example, {x ↦ 2,y ↦ 3+4 } is a ground substitution, {x ↦ x₁,y ↦ y₂+4 } is non-ground and non-flat, but linear,{x ↦ y₂,y ↦ y₂+4 } is non-linear and non-flat, {x ↦ y₂,y ↦ y₂ } is flat, but non-linear, {x ↦ x₁,y ↦ y₂ } is both linear and flat, but not a renaming, since it maps bothy andy₂ toy₂; each of these substitutions has the set {x,y} as its domain. An example for a renaming substitution is {x ↦ x₁,x₁ ↦ y,y ↦ y₂,y₂ ↦ x }, it has the inverse {x ↦ y₂,y₂ ↦ y,y ↦ x₁,x₁ ↦ x }. The flat substitution {x ↦ z,y ↦ z } cannot have an inverse, since e.g. (x+y) {x ↦ z,y ↦ z } =z+z, and the latter term cannot be transformed back tox+y, as the information about the origin az stems from is lost. The ground substitution {x ↦ 2 } cannot have an inverse due to a similar loss of origin information e.g. in (x+2) {x ↦ 2 } = 2+2, even if replacing constants by variables was allowed by some fictitious kind of "generalized substitutions".

Two substitutions are consideredequal if they map each variable tosyntactically equal result terms, formally:σ =τ ifxσ =xτ for each variablex ∈V.Thecomposition of two substitutionsσ = {x₁ ↦ t₁, …,x_k ↦ t_k } andτ = {y₁ ↦ u₁, …,y_l ↦ u_l } is obtained by removing from the substitution {x₁ ↦ t₁τ, …,x_k ↦ t_kτ,y₁ ↦ u₁, …,y_l ↦ u_l } those pairsy_i ↦ u_i for whichy_i ∈ {x₁, …,x_k }.The composition ofσ andτ is denoted byστ. Composition is anassociative operation, and is compatible with substitution application, i.e. (ρσ)τ =ρ(στ), and (tσ)τ =t(στ), respectively, for every substitutionsρ,σ,τ, and every termt.Theidentity substitution, which maps every variable to itself, is theneutral element of substitution composition. A substitutionσ is calledidempotent ifσσ =σ, and hencetσσ =tσ for every termt. Whenx_i≠t_i for alli, the substitution {x₁ ↦ t₁, …,x_k ↦ t_k } is idempotent if and only if none of the variablesx_i occurs in anyt_j. Substitution composition is not commutative, that is,στ may be different fromτσ, even ifσ andτ are idempotent.^[2]^: 73–74^[3]^{: 445–446}

For example, {x ↦ 2,y ↦ 3+4 } is equal to {y ↦ 3+4,x ↦ 2 }, but different from {x ↦ 2,y ↦ 7 }. The substitution {x ↦ y+y } is idempotent, e.g. ((x+y) {x↦y+y}) {x↦y+y} = ((y+y)+y) {x↦y+y} = (y+y)+y, while the substitution {x ↦ x+y } is non-idempotent, e.g. ((x+y) {x↦x+y}) {x↦x+y} = ((x+y)+y) {x↦x+y} = ((x+y)+y)+y. An example for non-commuting substitutions is {x ↦ y } {y ↦ z } = {x ↦ z,y ↦ z }, but {y ↦ z} {x ↦ y} = {x ↦ y,y ↦ z }.

Mathematics

[edit]

Inmathematics, there are two common uses of substitution:substitution ofvariables forconstants (also calledassignment for that variable), and thesubstitution property ofequality,^[5] also calledLeibniz's Law.^[6]

Considering mathematics as aformal language, a variable is asymbol from analphabet, usually a letter likex,y, andz, which denotes a range of possiblevalues.^[7] If a variable isfree in a givenexpression orformula, then it can be replaced with any of the values in its range.^[8] Certain kinds of bound variables can be substituted too. For instance,parameters of an expression (like thecoefficients of apolynomial), or theargument of afunction. Moreover, variables beinguniversally quantified can be replaced with any of the values in its range, and the result will a truestatement. (This is calledUniversal instantiation)

For a non-formalized language, that is, in most mathematical texts outside ofmathematical logic, for an individual expression it is not always possible to identify which variables are free and bound. For example, in ${\textstyle \sum _{i<k}a_{ik}}$ , depending on the context, the variable ${\textstyle i}$ can be free and ${\textstyle k}$ bound, or vice-versa, but they cannot both be free. Determining which value is assumed to be free depends on context andsemantics.

Thesubstitution property of equality, orLeibniz's Law (though the latter term is usually reserved forphilosophical contexts), generally states that, if two things are equal, then any property of one, must be a property of the other. It can be formally stated inlogical notation as: $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ For every ${\textstyle a}$ and ${\textstyle b}$ , and anywell-formed formula ${\textstyle \phi (x)}$ (with a free variable x). For example: For allreal numbersa andb, ifa =b, thena ≥ 0 impliesb ≥ 0 (here, $\phi (x)$ isx ≥ 0). This is a property which is most often used inalgebra, especially in solvingsystems of equations, but is applied in nearly every area of math that uses equality. This, taken together with thereflexive property of equality, forms theaxioms of equality in first-order logic.^[9]

Substitution is related to, but not identical to,function composition; it is closely related toβ-reduction inlambda calculus. In contrast to these notions, however, the accent in algebra is on the preservation of algebraic structure by the substitution operation, the fact that substitution gives ahomomorphism for the structure at hand (in the case of polynomials, thering structure).^{[citation needed]}

Algebra

[edit]

Substitution is a basic operation inalgebra, in particular incomputer algebra.^[10]^[11]

A common case of substitution involvespolynomials, where substitution of a numerical value (or another expression) for the indeterminate of a univariate polynomial amounts to evaluating the polynomial at that value. Indeed, this operation occurs so frequently that the notation for polynomials is often adapted to it; instead of designating a polynomial by a name likeP, as one would do for other mathematical objects, one could define

P(X)=X^{5}-3X^{2}+5X-17

so that substitution forX can be designated by replacement inside "P(X)", say

P(2)=13

P(X+1)=X^{5}+5X^{4}+10X^{3}+7X^{2}+4X-14.

Substitution can also be applied to other kinds of formal objects built from symbols, for instance elements offree groups. In order for substitution to be defined, one needs an algebraic structure with an appropriateuniversal property, that asserts the existence of unique homomorphisms that send indeterminates to specific values; the substitution then amounts to finding the image of an element under such a homomorphism.

Proof of substitution in ZFC

[edit]

The following is a proof of the substitution property of equality in ZFC (as defined in first-order logic without equality), which is adapted fromIntroduction to Axiomatic Set Theory (1982) by Gaisi Takeuti and Wilson M. Zaring.^[12]

Theorem—if $a=b$ , then, for any well-formed formula $\phi$ , $\phi (a)\Rightarrow \phi (b)$ .

SeeZermelo–Fraenkel set theory § Formal language for the definition of formulas in ZFC. Thedefinition is recursive, so a proof byinduction is used. In ZFC in first-order logic without equality, "set equality" is defined to mean that two sets have the same elements, written symbolically as "for all z, z is in x if and only if z is in y". Then, the Axiom of Extensionality asserts that if two sets have the same elements, then they belong to the same sets:

Definition— $(x=y):=\forall z[z\in x\Leftrightarrow z\in y]$

Axiom— $(x=y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)$

Base formulas

Let $X, Y, Z {\displaystyle X,Y,Z}$ , be metavariables for any variables or sets, such that $X=Y$

Case 1: $\phi (X):(Z\in X)$

Assume $Z\in X$ , then, by the definition of equality, $Z\in Y$ , thus $(X=Y)\implies {\bigl [}Z\in X\Rightarrow Z\in Y{\bigr ]}$

Case 2: $\phi (X):(X\in Z)$

Assume $X\in Z$ , then by the axiom of extensionality, $Y\in Z$ , thus $(X=Y)\implies {\bigl [}X\in Z\Rightarrow Y\in Z{\bigr ]}$

Recursive formulas

Let $\psi ,\varphi$ be meta variables for any formulas with the property that $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ . Let $X, Y {\displaystyle X,Y}$ , be metavariables for any variables or sets, such that $X=Y$ , and let $z {\displaystyle z}$ be a metavariable for any variable.

Case 1: $\neg (\psi )$

Since $X=Y$ , then $Y=X$ by symmetry of equality, therefore ${\bigl [}\psi (Y)\Rightarrow \psi (X){\bigr ]}$ , by the induction hypothesis, therefore ${\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$ bycontraposition, thus $(X=Y)\implies {\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$

Case 2: $\psi \land \varphi$

Since $X=Y$ , then ${\bigl [}\psi (X)\Rightarrow \psi (Y){\bigr ]}$ and ${\bigl [}\varphi (X)\Rightarrow \varphi (Y){\bigr ]}$ , which implies ${\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$ , thus $(X=Y)\implies {\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$

Case 3: $\exists z(\psi )$

Since $X=Y$ , $\psi (X,z)\Rightarrow \psi (Y,z)$ assume byway of contradiction that the result is false, that is $\exists z(\psi (X,z))$ is true but $\exists z(\psi (Y,z))$ is false. Byexistential instantiation, let $z_{0}$ denote the value such that $\psi (X,z_{0})$ is true. Then $\psi (Y,z_{0})$ is false by asumption, and therefore $\psi (X,z_{0})\Rightarrow \psi (Y,z_{0})$ is false, which contradicts our induction hypothesis, and the result follows.

Notes

[edit]

^Some authors use [t₁/x₁, …,t_k/x_k ] to denote that substitution, e.g.M. Wirsing (1990). Jan van Leeuwen (ed.).Algebraic Specification. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675–788., here: p. 682.
^From aterm algebra point of view, the setT of terms is thefree term algebra over the setV of variables, hence for each substitution mapping σ:V →T there is a uniquehomomorphismσ:T →T that agrees with σ onV ⊆T; the above-defined application ofσ to a termt is then viewed as applying the functionσ to the argumentt.

Citations

[edit]

^Hunter, Geoffrey (1996) [1971].Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press (published 1973). p. 118.ISBN 9780520023567.OCLC 36312727. (accessible to patrons with print disabilities)
^^a ^bDavid A. Duffy (1991).Principles of Automated Theorem Proving. Wiley.
^^a ^bFranz Baader,Wayne Snyder (2001).Alan Robinson andAndrei Voronkov (ed.).Unification Theory(PDF). Elsevier. pp. 439–526. Archived fromthe original(PDF) on 2015-06-08. Retrieved2014-09-24.
^N. Dershowitz; J.-P. Jouannaud (1990). "Rewrite Systems". InJan van Leeuwen (ed.).Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.
^Sobolev, S. K. (2001) [1994],"Equality axioms",Encyclopedia of Mathematics,EMS Press
^Deutsch, Harry and Pawel Garbacz, "Relative Identity", The Stanford Encyclopedia of Philosophy (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman (eds.), forthcoming URL:https://plato.stanford.edu/entries/identity-relative/#StanAccoIden
^Sobolev, S. K. (2001) [1994],"Individual variable",Encyclopedia of Mathematics,EMS Press
^Sobolev, S. K. (2001) [1994],"Free variable",Encyclopedia of Mathematics,EMS Press
^Fitting, M.,First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990),pp. 198–200.
^Margret H. Hoft; Hartmut F.W. Hoft (6 November 2002).Computing with Mathematica. Elsevier.ISBN 978-0-08-048855-4.
^Andre Heck (6 December 2012).Introduction to Maple. Springer Science & Business Media.ISBN 978-1-4684-0484-5.substitution.
^Takeuti, Gaisi; Zaring, Wilson M. (1982)."Introduction to Axiomatic Set Theory".Graduate Texts in Mathematics:6–9.doi:10.1007/978-1-4613-8168-6.ISSN 0072-5285. Archived fromthe original on 2014-08-06.

References

[edit]

Crabbé, M. (2004).On the Notion of Substitution. Logic Journal of the IGPL, 12, 111–124.
Curry, H. B. (1952)On the definition of substitution, replacement and allied notions in an abstract formal system. Revue philosophique de Louvain 50, 251–269.
Kleene, S. C. (1967).Mathematical Logic. Reprinted 2002, Dover.ISBN 0-486-42533-9
Robinson, Alan J. A.; Voronkov, Andrei (2001-06-22).Handbook of Automated Reasoning. Elsevier.ISBN 978-0-08-053279-0

External links

[edit]

Substitution at thenLab

Logic

History

Major fields

Logics	Classical Informal Critical thinking Reason Mathematical Non-classical Philosophical
Theories	Argumentation Metalogic Metamathematics Set

Foundations

Lists

Topics	Mathematical logic Boolean algebra Set theory
Other	Logicians Rules of inference Paradoxes Fallacies Logic symbols

Mathematical logic

General

Theorems (list)
and paradoxes

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types ofsets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps and cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Set theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive