Розділ 04: Правила для квантіфікаторів

Last updated
Save as PDF

Page ID: 52237

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

Для доказів у QL ми використовуємо всі основні правила SL плюс чотири нові основні правила: як введення, так і правила усунення для кожного з квантіфікаторів.

Оскільки всі похідні правила SL походять від основних правил, вони також будуть триматися в QL. Ми додамо ще одне похідне правило, правило заміни, яке називається кількісним запереченням.

екземпляри підміни

Для того, щоб стисло викласти правила для квантіфікаторів, нам потрібен спосіб позначити зв'язок між кількісними реченнями та їх екземплярами. Наприклад, речення\(Pa\) є певним екземпляром загального позову\(xPx\).

Для\(\mathcal{A}\) w, константа та змінна\(\mathcal{c}\), визначте примірник заміщення\(\mathcal{xA}\) або\(\mathcal{xA}\) - це\(\mathcal{x}\) w, що ми отримуємо, замінюючи кожне входження\(\mathcal{x}\) в\(\mathcal{A}\) на\(\mathcal{c}\). Ми викликаємо\(\mathcal{c}\) константу екземпляра.

Щоб підкреслити той факт, що змінна\(\mathcal{x}\) замінена константою екземпляра\(\mathcal{c}\), ми напишемо оригінальні кількісно визначені вирази як\(\mathcal{x}\)\(\mathcal{Ax}\)\(\mathcal{x}\)\(\mathcal{Ax}\) і. І ми напишемо примірник підстановки\(\mathcal{Ac}\).

Зверніть увагу\(\mathcal{A}\), що\(\mathcal{x}\), і\(\mathcal{c}\) всі мета-змінні. Тобто, вони є стійками для будь-якого w, змінна, і постійна взагалі. І коли ми пишемо\(\mathcal{Ac}\), константа\(\mathcal{c}\) може відбуватися кілька разів у\(\mathcal{A}\) w.

Наприклад:
~\(Aa\) →\(Ba\),\(Af\) →\(Bf\), і\(Ak\) →\(Bk\) є усіма примірниками підстановки «\(x\)(\(Ax\)→\(Bx\)); константи екземпляра є\(a\)\(f\), і\(k\), відповідно.

~\(Raj\)\(Rdj\), і\(Rjj\) є примірниками підстановки\(zRzj\); константи екземпляра є\(a\)\(d\), і\(j\), відповідно.

універсальна ліквідація

Якщо у вас є\(xAx\), законно зробити висновок, що щось є\(A\). Можна зробити висновок\(A\) _a,\(A\) _b,\(A\) _z,\(Ad\) ₃. Ви можете зробити висновок про будь-який примірник заміни,\(A\(\mathcal{c}\) для будь-якої константи\(\mathcal{c}\).

Це загальна форма правила універсальної елімінації (E):

Використовуючи правило E, ви пишете замінене речення з константою, що\(\mathcal{c}\) замінює всі входження змінної\(\mathcal{x}\) в\(\mathcal{A}\). Наприклад:

екзистенціальне введення

Законно зробити висновок,\(xPx\) якщо ви знаєте, що щось є\(P\). Це може бути якась конкретна річ взагалі. Наприклад, якщо у вас є в\(Pa\) наявності доказ, то\(xPx\) слід.

Це екзистенціальне правило введення (I):

Важливо зауважити, що\(\mathcal{x}\) змінна не потребує заміни всіх входжень константи\(\mathcal{c}\). Ви можете вирішити, які випадки замінити, а які залишити на місці. Наприклад:

Універсальне введення

Універсальна претензія на\(xPx\) кшталт «Була б доведена, якби кожен примірник його заміщення був доведений. Тобто, якби кожне речення\(Pa\)\(Pb\),,... було доступне в доказі, то ви, безумовно, мали б право претендувати\(xPx\). На жаль, надії довести кожен примірник підміни немає. Це вимагатиме доведення\(Pa\)\(Pb\),,...,\(P\) j ₂,...,\(Ps\) ₇,..., і так далі до нескінченності. У QL нескінченно багато констант, і тому цей процес ніколи не закінчиться.

Розглянемо замість цього простий аргумент:\(xMx\),.. 3\(yMy\)

Це не робить ніякої різниці в значенні речення, чи використовуємо ми змінну\(x\) чи змінну\(y\), тому цей аргумент, очевидно, є дійсним. Припустимо, ми починаємо таким чином:

Ми вивели\(Ma\). Ніщо не заважає нам використовувати те саме виправдання, щоб отримати\(Mb\),...,\(Mj\) ₂,...,\(Ms\) ₇,..., і так далі, поки у нас не закінчиться простір або терпіння. Ми ефективно показали спосіб довести\(M\)\(\mathcal{c}\) для будь-якої константи\(\mathcal{c}\). З цього\(yMy\) випливає «».

Тут важливо, щоб\(a\) була якась довільна константа. Особливих припущень з цього приводу ми не робили. \(Ma\)Якби передумова аргументу, то це нічого не показувало б про всіх\(y\). Наприклад:

Це схематична форма правила універсального введення (I):

∗ Постійна не\(\mathcal{c}\) повинна відбуватися в жодному нерозрядженому припущенні.

Зверніть увагу, що ми можемо зробити це для будь-якої константи, яка не зустрічається в нерозрядженому припущенні і для будь-якої змінної.

Зверніть увагу також, що константа може не відбуватися в будь-якому нерозрядженому припущенні, але це може відбуватися як припущення про піддоказ, який ми вже закрили. Наприклад, ми можемо довести «\(z\)(\(Dz\)→\(Dz\)) без будь-яких приміщень.

Екзистенціальна ліквідація

Речення з екзистенціальним кількісним показником говорить нам, що є якийсь член УД, який задовольняє формулу. Наприклад,\(xSx\) говорить нам (приблизно), що є принаймні один\(S\). Однак це не говорить нам, який член УД задовольняє\(S\). Ми не можемо відразу зробити висновок\(Sa\),\(Sf\) ₂₃, або будь-який інший примірник підміни речення. Що ми можемо зробити? Припустимо, що ми знали\(xSx\) і, і\(x\) (\(Sx\)→\(Tx\)). Ми могли б міркувати таким чином:

Так як\(xSx\), є щось, що є\(S\). Ми не знаємо, які константи посилаються на цю річ, якщо такі роблять, тому називайте цю річ «Ізмаїл». З\(x\) (\(Sx\)→\(Tx\)) випливає, що якщо Ізмаїл є\(S\), то це a\(T\). Тому Ізмаїл - це\(T\). Тому що Ізмаїл є\(T\), ми знаємо, що\(xTx\).

У цьому пункті ми ввели назву для речі, яка є\(S\). Ми дали йому довільну назву («Ізмаїл»), щоб ми могли міркувати про це і отримати деякі наслідки від того, що існує\(S\). Оскільки «Ізмаїл» - це лише фіктивне ім'я, введене з метою доказу, а не справжня константа, ми не могли згадати про це у висновку. Але ми могли б вивести речення, яке не згадує Ізмаїла; а саме,\(xTx\). Це речення випливає з двох приміщень.

Ми хочемо, щоб екзистенціальне правило ліквідації працювало аналогічним чином. Однак, оскільки англійські слова, такі як «Ізмаїл», не є символами QL, ми не можемо використовувати їх у формальних доказах. Замість цього ми будемо використовувати константи QL, які інакше не відображаються в proof.

Константа, яка використовується для того, щоб стояти за все, що задовольняє екзистенціальну претензію, називається проксі. Міркування з проксі повинні відбуватися всередині піддоказу, і проксі не може бути постійною, яка робить роботу в іншому місці доказу.

Це схематична форма правила екзистенціального усунення (E):

∗ Константа не\(\mathcal{c}\) повинна з'являтися в\(\mathcal{xAx}\), in або в\(\mathcal{B}\) будь-якому нерозрядженому припущенні.

Оскільки константа проксі - це лише власник місця, який ми використовуємо всередині піддоказ, це не може бути те, про що ми знаємо щось конкретне. Тож це не може з'явитися в оригінальному реченні\(\mathcal{xAx}\) або в нерозрядженому припущенні. Більш того, ми нічого не дізнаємося про константу проксі за допомогою правила E. Таким чином, це не може з'явитися в реченні\(\mathcal{B}\), яке ви доводите, використовуючи E.

Найпростіший спосіб задовольнити ці вимоги - вибрати абсолютно нову константу, коли ви починаєте піддоказ, а потім не використовувати цю постійну де-небудь ще в доказі. Після того, як ви закриєте підзахисний пристрій, не згадуйте його знову.

За допомогою цього правила ми можемо дати формальний доказ того,\(xSx\)\(x\) щоі(\(Sx\) →\(Tx\)) разом тягне за собою x\(Tx\).

Зверніть увагу, що це фактично має ту саму структуру, що і англомовний аргумент, з якого ми почали, за винятком того, що subproof використовує константу проксі-сервера «\(i\)», а не фіктивне ім'я «Ізмаїл».

Кільтіфікатор заперечення

При перекладі з англійської на QL ми відзначили, що\(x\) ¬¬\(\mathcal{A}\) логічно еквівалентно\(x\)\(\mathcal{A}\). У QL вони доказово еквівалентні. Ми можемо довести половину еквівалентності досить жахливим доказом:

Для того, щоб показати, що ці два речення дійсно еквівалентні, нам потрібен другий доказ, який передбачає\(x\) ¬¬\(\mathcal{A}\) і виводить\(x\)\(\mathcal{A}\). Ми залишаємо цей доказ як вправу для читача.

Часто буде корисно перекладати між квантифікаторами, додаючи або віднімаючи заперечення таким чином, тому ми додаємо два похідних правила для цієї мети. Ці правила називаються кількісним запереченням (QN):

¬\(\mathcal{xA}\)\(\mathcal{x}\) ⇒¬\(\mathcal{A}\)
\(\mathcal{xA}\) ¬⇒¬\(\mathcal{x}\) ¬\(\mathcal{A}\) QN

Оскільки QN є правилом заміни, його можна використовувати на цілих реченнях або на підформулах.