Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Substitution (logic)
Summary
A substitution is a syntactic transformation on formal expressions.
To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols with other expressions.
The resulting expression is called a substitution instance, or instance for short, of the original expression.
Where ψ and φ represent formulas of propositional logic, ψ is a substitution instance of φ if and only if ψ may be obtained from φ by substituting formulas for symbols in φ, replacing each occurrence of the same symbol by an occurrence of the same formula. For example:
(R → S) & (T → S)
is a substitution instance of:
P & Q
and
(A ↔ A) ↔ (A ↔ A)
is a substitution instance of:
(A ↔ A)
In some deduction systems for propositional logic, a new expression (a proposition) may be entered on a line of a derivation if it is a substitution instance of a previous line of the derivation (Hunter 1971, p. 118). This is how new lines are introduced in some axiomatic systems. In systems that use rules of transformation, a rule may include the use of a substitution instance for the purpose of introducing certain variables into a derivation.
In first-order logic, every closed propositional formula that can be obtained from an open propositional formula φ by substitution is said to be a substitution instance of φ. If φ is a closed propositional formula we count φ itself as its only substitution instance.
A propositional formula is a tautology if it is true under every valuation (or interpretation) 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.
In first-order logic, a substitution is a total mapping σ: V → T from variables to terms; many, but not all authors additionally require σ(x) = x for all but finitely many variables x. The notation { x1 ↦ t1, ..., xk ↦ tk }
refers to a substitution mapping each variable xi to the corresponding term ti, for i=1,...
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Ontological neighbourhood
Related courses (1)
EE-566: Adaptation and learning
In this course, students learn to design and master algorithms and core concepts related to inference and learning from data and the foundations of adaptation and learning theories with applications.