**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

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.

Related publications (3)

Related concepts (15)

Related courses (1)

Related lectures (18)

Interpretation (logic)

An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics. The most commonly studied formal logics are propositional logic, predicate logic and their modal analogs, and for these there are standard ways of presenting an interpretation.

Term (logic)

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact. A first-order term is recursively constructed from constant symbols, variables and function symbols. An expression formed by applying a predicate symbol to an appropriate number of terms is called an atomic formula, which evaluates to true or false in bivalent logics, given an interpretation.

Rewriting

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects. Rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable.

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.

Avoiding Variable Capture

Explores variable capture in higher-order functions and the importance of variable renaming.

Sequent Calculus with Equality

Covers Sequent Calculus with Equality, focusing on atomic formulas and substitution rules.

Predicate Calculus: Basics

Covers the basics of predicate calculus, including propositions, formulas, terms, and semantic evaluation.

The syn-anti ratio of 7-(R-substituted)-norcaranes (I, R = Ph. F, Cl) formed in the cycloaddn. of cyclohexene (II) with PhCH2F, PhCH2Cl, PhCHBrF, PhCHBr2, FCHBr2, ClCHBr2, or CH2Cl and BuLi in various solvents under N was examd. with respect to influences ...

1970A formalized theory of alpha-conversion for the pi-calculus in Isabelle/HOL is presented. Following a recent proposal by Gabbay and Pitts, substitutions are modelled in terms of permutations, and alpha-equivalence is defined over all but finitely many name ...

2001Jieping Zhu, Juliette Ferial Blanchet

The following chapter summarizes the various methodologies allowing the reductive cleavage of various carbon---hetereroatom single bonds or multiple bonds naming the transformation of C---N bond, C---P, C---As, C---Sb, C---Bi, C---C, C---Si, C---Ge, C---B, ...