Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Substitution (logic)
Résumé
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,...
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.