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.