9.3: Правила кількісного визначення

Last updated
Save as PDF

Page ID: 52904

\( \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

Правила для\(\lforall{}{}\)

9.3.1.png

У правилах для\(\lforall{}{}\),\(t\) є підґрунтовим терміном (термін, який не містить жодних змінних), і\(a\) є постійним символом, який не зустрічається у висновку\(\lforall{x}{A(x)}\), або в будь-якому припущенні, що не розряджається в похідній, що закінчується приміщення\(A(a)\). Ми\(a\) називаємо власну змінну\(\Intro{\lforall{}{}}\) висновку.

Правила для\(\lexists{}{}\)

9.3.2.png

Знову ж таки,\(t\) це термін підстави, і\(a\) є постійною, яка не відбувається в приміщенні\(\lexists{x}{A(x)}\), у висновку\(C\), або будь-яке припущення, яке не вичерпується в похідних, що закінчуються двома приміщеннями (крім припущень \(A(a)\)). Ми\(a\) називаємо власну змінну\(\Elim{\lexists{}{}}\) висновку.

Умова про те, що власна змінна не виникає ні в приміщеннях, ні в будь-якому припущенні, що не розряджається в похідних, що ведуть до приміщення для\(\Intro{\lforall{}{}}\) або\(\Elim{\lexists{}{}}\) висновку, називається власнозмінним умовою.

Ми використовуємо термін «власна змінна», хоча\(a\) в вищезазначених правилах є константою. Це має історичні причини.

У\(\Intro{\lexists{}{}}\) і\(\Elim{\lforall{}{}}\) обмежень немає, а термін\(t\) може бути будь-яким, тому нам не доведеться турбуватися ні про які умови. З іншого боку, в\(\Intro{\lforall{}{}}\) правилах\(\Elim{\lexists{}{}}\) і власназмінна умова вимагає, щоб постійний символ\(a\) не виникав ніде в ув'язненні або в нерозрядженому припущенні. Умова необхідна для того, щоб система була здоровою, тобто тільки виводить пропозиції з нерозряджених припущень, з яких вони випливають. Без цієї умови було б дозволено наступне:

9.3.3.png

Однак,\(\lexists{x}{A(x)} \EntailsN \lforall{x}{A(x)}\).