5.7: Безкоштовні змінні та речення

Last updated
Save as PDF

Page ID: 53011

$ \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}$: Free occurrences of a variable

Вільні входження змінної у формулі визначаються індуктивно наступним чином:

$\indcaseA{A}{$A$ is atomic}$всі входження змінних у$\indfrm$ вільні.
$\indcase{A}{\lnot B}$вільні випадки змінних$\indfrm$ є саме такими$B$.
$\indcase{A}{(B \ast C)}$вільні випадки змінних$\indfrm$ є ті, що$B$ разом з тими, в$C$.
$\indcase{A}{\lforall{x}{B}}$вільні входження змінних в$\indfrm$ є всі ті,$B$ за винятком випадків$x$.
$\indcase{A}{\lexists{x}{B}}$вільні входження змінних в$\indfrm$ є всі ті,$B$ за винятком випадків$x$.

Визначення$\PageIndex{2}$: Bound Variables

Входження змінної у формулі$A$ пов'язане, якщо вона не є вільною.

Проблема$\PageIndex{1}$

Дайте індуктивне визначення випадків зв'язаних змінних за лініями Definition$\PageIndex{1}$.

Визначення$\PageIndex{3}$: Scope

Якщо$\lforall{x}{B}$ є входження підформули у формулі$A$, то відповідне входження$B$ in$A$ називається сферою відповідного виникнення$\lforall{x}{}$. Аналогічно для$\lexists{x}{}$.

Якщо$B$ є сферою виникнення кількісного$\lforall{x}{}$$\lexists{x}{}$ показника або в$A$, то вільні випадки$x$$B$ in пов'язані в$\lforall{x}{B}$ і$\lexists{x}{B}$. Ми говоримо, що ці випадки пов'язані згаданим кількісним випадком.

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

Розглянемо наступну формулу:\[\lexists{\Obj v_0}{\underbrace{\Atom{\Obj A^2_0}{\Obj v_0,\Obj v_1}}_{B}}\nonumber\]$B$ представляє сферу застосування$\lexists{\Obj v_0}{}$. Квантор пов'язує виникнення$\Obj v_0$ in$B$, але не пов'язує виникнення$\Obj v_1$. Так$\Obj v_1$ це вільна змінна в даному випадку.

Тепер ми можемо побачити, як це може працювати в більш складній формулі$A$:\[\lforall{\Obj v_0}{\underbrace{(\Atom{\Obj A^1_0}{\Obj v_0} \lif \Atom{\Obj A^2_0}{\Obj v_0, \Obj v_1})}_{B}} \lif \lexists{\Obj v_1}{\underbrace{(\Atom{\Obj A^2_1}{\Obj v_0, \Obj v_1} \lor \lforall{\Obj v_0}{\overbrace{\lnot \Atom{\Obj A^1_1}{\Obj v_0}}^{D}})}_{C}}\nonumber\]$B$ це сфера дії першого$\lforall{\Obj v_0}{}$,$C$ це сфера дії$\lexists{\Obj v_1}{}$, і$D$ є сферою дії другого $\lforall{\Obj v_0}{}$. Перший$\lforall{\Obj v_0}{}$ пов'язує входження$\Obj v_0$ в$B$,$\lexists{\Obj v_1}{}$ виникнення$\Obj v_1$ in$C$, а другий$\lforall{\Obj v_0}{}$ пов'язує виникнення$\Obj v_0$ в $D$. Перше виникнення$\Obj v_1$ і четверте виникнення$\Obj v_0$ вільні в$A$. Останнє виникнення$\Obj v_0$ є вільним в$D$, але пов'язане в$C$ і$A$.

Визначення$\PageIndex{4}$: Sentence

Формула$A$ - це речення, якщо воно не містить вільних входжень змінних.