“introduction rule”的概念、定义、翻译、参考文献-科学参考

introduction rule

Logic

A rule of inference that governs when one may add a connective $\circ$ to a formula. For example, the introduction rules for disjunction $\lor$ in classical logic are:
$\frac{φ}{φ \lor ψ} \frac{ψ}{φ \lor ψ}$
These rules describe the conditions under which a disjunction may be introduced in a proof. Introduction rules are dual to elimination rules, which describe cases in which a formula may be simplified by eliminating its main connective.
In sequent calculi, there are no elimination rules but two types of introduction rules: left-introduction and right-introduction. Returning to disjunction, the left introduction rule for disjunction is represented as:
$\frac{Γ, φ \Rightarrow Δ Σ, ψ \Rightarrow Π}{Γ, Σ, φ \lor ψ \Rightarrow Δ, Π} \lor L$
while the right introduction rules are:
$\frac{Γ \Rightarrow φ, Δ}{Γ \Rightarrow φ \lor ψ, Δ} \lor R_{0} \frac{Γ \Rightarrow ψ, Δ}{Γ \Rightarrow φ \lor ψ, Δ} \lor R_{1}$

单词	introduction rule
释义	introduction rule Logic A rule of inference that governs when one may add a connective $\circ$ to a formula. For example, the introduction rules for disjunction $\lor$ in classical logic are: $\frac{φ}{φ \lor ψ} \frac{ψ}{φ \lor ψ}$ These rules describe the conditions under which a disjunction may be introduced in a proof. Introduction rules are dual to elimination rules, which describe cases in which a formula may be simplified by eliminating its main connective. In sequent calculi, there are no elimination rules but two types of introduction rules: left-introduction and right-introduction. Returning to disjunction, the left introduction rule for disjunction is represented as: $\frac{Γ, φ \Rightarrow Δ Σ, ψ \Rightarrow Π}{Γ, Σ, φ \lor ψ \Rightarrow Δ, Π} \lor L$ while the right introduction rules are: $\frac{Γ \Rightarrow φ, Δ}{Γ \Rightarrow φ \lor ψ, Δ} \lor R_{0} \frac{Γ \Rightarrow ψ, Δ}{Γ \Rightarrow φ \lor ψ, Δ} \lor R_{1}$
随便看	benzpyrene benzvalene benzyl alcohol benzylamine benzyne Beowulf cluster BepiColombo BeppoSAX BER Berber Berdyaev, Nikolai (1874–1948) Beregovoy, Georgy Timofeyevich (1921–95) Berezovoi, Anatoly (1942–2014) Bergen School Berger, Hans Berger, James Orvis (1950– ) Bergeron theory Bergeron, Tor Harold Percival Bergeron–Findeisen theory Bergius, Friedrich Karl Rudolf (1884–1949) Bergius, Friedrich Karl Rudolph Bergius, Friedrich Karl Rudolph (1884–1949) Bergius process Bergmann, Gustav (1906–87) Bergmann, Max