5.8: Заміна

Last updated
Save as PDF

Page ID: 53066

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)

Template:MathJaxZach

Визначення\(\PageIndex{1}\): Substitution in a term

Визначимо\(\Subst{s}{t}{x}\), результат підстановки\(t\) для кожного входження\(x\) in\(s\), рекурсивно:

\(\indcase{s}{c}\)\(\Subst{s}{t}{x}\)це просто\(s\).
\(\indcase{s}{y}\)\(\Subst{s}{t}{x}\)також просто\(s\), за умови\(y\) є змінною і\(y \not\ident x\).
\(\indcase{s}{x}\)\(\Subst{s}{t}{x}\)є\(t\).
\(\indcase{s}{\Atom{f}{t_1, \dots, t_n}}\)\(\Subst{s}{t}{x}\)є\(\Atom{f}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).

Визначення\(\PageIndex{2}\)

Термін\(t\) вільний для\(x\) in,\(A\) якщо жодне з вільних випадків in не\(A\) відбувається\(x\) в області квантора, який пов'язує змінну в\(t\).

Приклад\(\PageIndex{1}\)

\(\Obj v_8\)є безкоштовним для\(\Obj v_1\)\(\lexists{\Obj v_3}{}\Atom{\Obj A^2_4}{\Obj v_3,\Obj v_1}\)
\(\Obj f^2_1(\Obj v_1, \Obj v_2)\)не є безкоштовним для\(\Obj v_0\)\(\lforall{\Obj v_2}{}\Atom{\Obj A^2_4}{\Obj v_0,\Obj v_2}\)

Визначення\(\PageIndex{3}\): Substitution in a formula

Якщо\(A\) є формулою,\(x\) є змінною, і\(t\) є вільним\(x\) терміном для in\(A\), то\(\Subst{A}{t}{x}\) є результатом заміни\(t\) всіх вільних входження \(x\)в\(A\).

\(\indcase{A}{\lfalse}\)\(\Subst{\indfrm}{t}{x}\)є\(\lfalse\).
\(\indcase{A}{\Atom{P}{t_1,\dots, t_n}}\)\(\Subst{\indfrm}{t}{x}\)є\(\Atom{P}{\Subst{t_1}{t}{x}, \dots, \Subst{t_n}{t}{x}}\).
\(\indcase{A}{\eq[t_1][t_2]}\)\(\Subst{\indfrmp}{t}{x}\)є\(\Subst{t_1}{t}{x} = \Subst{t_2}{t}{x}\).
\(\indcase{A}{\lnot B}\)\(\Subst{\indfrmp}{t}{x}\)є\(\lnot \Subst{B}{t}{x}\).
\(\indcase{A}{(B \land C)}\)\(\Subst{\indfrmp}{t}{x}\)є\((\Subst{B}{t}{x} \land \Subst{C}{t}{x})\).
\(\indcase{A}{(B \lor C)}\)\(\Subst{\indfrmp}{t}{x}\)є\((\Subst{B}{t}{x} \lor \Subst{C}{t}{x})\).
\(\indcase{A}{(B \lif C)}\)\(\Subst{\indfrmp}{t}{x}\)є\((\Subst{B}{t}{x} \lif \Subst{C}{t}{x})\).
\(\indcase{A}{\lforall{y}{B}}\)\(\Subst{\indfrmp}{t}{x}\)є\(\lforall{y}{\Subst{B}{t}{x}}\), за умови\(y\) є змінною, крім\(x\); інакше\(\Subst{\indfrmp}{t}{x}\) просто\(\indfrm\).
\(\indcase{A}{\lexists{y}{B}}\)\(\Subst{\indfrmp}{t}{x}\)є\(\lexists{y}{\Subst{B}{t}{x}}\), за умови\(y\) є змінною, крім\(x\); інакше\(\Subst{\indfrmp}{t}{x}\) просто\(\indfrm\).

Зверніть увагу, що заміщення може бути вакуумним: якщо\(x\) не відбувається\(A\) взагалі,\(\Subst{A}{t}{x}\) то просто\(A\).

Обмеження, яке\(t\) повинно бути\(A\) безкоштовним для\(x\) in, необхідно для виключення таких випадків. Якщо\(A \ident \lexists{y}{x < y}\) і\(t \ident y\), то\(\Subst{A}{t}{x}\) буде\(\lexists{y}{y < y}\). У цьому випадку вільна змінна «\(y\)захоплюється» квантором\(\lexists{y}{}\) при підстановці, і це небажано. Наприклад, ми хотіли б, щоб це був випадок, коли\(\lforall{x}{B}\) тримає, так і робить\(\Subst{B}{t}{x}\). Але врахуйте\(\lforall{x}{\lexists{y}{x < y}}\) (\(B\)ось\(\lexists{y}{x < y}\)). Це речення, яке вірно стосується, наприклад, натуральних чисел: для кожного числа\(x\) є число\(y\) більше, ніж воно. Якби ми дозволили в\(y\) якості можливої заміни для\(x\), ми б в кінцевому підсумку з\(\Subst{B}{y}{x} \ident \lexists{y}{y < y}\), що є помилковим. Ми запобігаємо цьому, вимагаючи, щоб жодна з вільних\(t\) змінних в кінцевому підсумку не була пов'язана кількісним показником в\(A\).

Ми часто використовуємо таку угоду, щоб уникнути громіздких позначень: Якщо формула з\(A\) вільною змінною\(x\), ми пишемо,\(A(x)\) щоб вказати це. Коли зрозуміло, який\(A\) і\(x\) ми маємо на увазі, і\(t\) є терміном (вважається вільним для\(x\) in\(A(x)\)), то пишемо\(A(t)\) як короткий для\(\Subst{A(x)}{t}{x}\).