6.3: Приклади теорій першого порядку
- Page ID
- 52716
Приклад\(\PageIndex{1}\)
Теорія строгих лінійних порядків в мові\(\Lang L_<\) аксіоматизована множиною.\[\begin{aligned} & \lforall{x}{\lnot x < x}, \\ & \lforall{x}{\lforall{y}{((x < y \lor y < x) \lor x = y)}}, \\ & \lforall{x}{\lforall{y}{\lforall{z}{((x < y \land y < z) \lif x < z)}}}\end{aligned}\] Вона повністю захоплює передбачувані структури: кожен строгий лінійний порядок є моделлю цієї системи аксіом, і навпаки, якщо\(R\) лінійний порядок на множині \(X\), то структура\(\Struct M\) з\(\Domain M = X\) і\(\Assign{<}{M} = R\) є моделлю цієї теорії.
Приклад\(\PageIndex{2}\)
Теорія груп у мові\(\Obj 1\) (постійний символ),\(\cdot\) (символ двомісної функції) аксіоматизується\[\begin{aligned} & \lforall{x}{\eq[(x \cdot \Obj 1)][x]}\\ & \lforall{x}{\lforall{y}{\lforall{z}{\eq[(x \cdot (y \cdot z))][((x \cdot y) \cdot z)]}}}\\ & \lforall{x}{\lexists{y}{\eq[(x \cdot y)][\Obj 1]}}\end{aligned}\]
Приклад\(\PageIndex{3}\)
Теорія арифметики Пеано аксіоматизується наступними реченнями мовою арифметики\(\Lang L_A\).
\ [\ почати {вирівняний}
&\ lforall {x} {\ lforall {y} {(\ eq [x'] [y']\ lif\ eq [x] [y])}}\\
&\ lforall {x} {\ eQN [\ Obj 0] [x ']}\\
&\ lforall {x} {\ eq [+\ Обж 0)] [x]}\\
&\ lforall {x} {\ lforall {y} {\ eq [(x + y')] [(x + y)']}}\\
&\ lforall {x} {\ eq [(x\ times\ Obj 0)] [\ Obj 0]}\\
&\ lforall {x} {\ lforall {\ eq [(x\ times y')] [(x\ times y) + x)]}}\\
&\ lforall {x} {\ lforall {y} {(x < y\ liff\ лексисти {z} {\ eq [(z' + x)] [y])}}}
\ кінець {вирівняний}\]
плюс всі речення форми
\[(A(\Obj 0) \land \lforall{x}{(A(x) \lif A(x'))}) \lif \lforall{x}{A(x)}\nonumber\]
Оскільки пропозицій останньої форми нескінченно багато, то ця система аксіом нескінченна. Остання форма називається схемою індукції. (Насправді, схема індукції трохи складніше, ніж ми пускаємо тут.)
Остання аксіома - це явне визначення\(<\).
Приклад\(\PageIndex{4}\)
Теорія чистих множин відіграє важливу роль в основах (і в філософії) математики. Набір чистий, якщо всі його елементи також чисті набори. Отже, порожній набір вважається чистим, але набір, який має щось як елемент, який не є набором, не буде чистим. Таким чином, чисті множини - це ті, які утворюються тільки з порожнього набору і ніяких «уреелементів», тобто об'єктів, які самі не є множинами.
Наступне можна розглядати як систему аксіом для теорії чистих множин:
\ [\ почати {вирівняні}
&\ лексисти {x} {\ lnot\ лексисти {y} {y\ in x}}\\
&\ lforall {x} {\ lforall {y} {(\ lforall {z} {} (z\ in x\ liff z\ in y)\ lif\ eq [x] [y])}\\
&\ lford всі {x} {\ lforall {y} {\ лексисти {z} {\ lforall {u} {(u\ in z\ liff (\ eq [u] [x]\ lor\ eq [u] [y]))}}}\\
&\ lforall {x} {\ лексисти {y} {\ lforall {z} {(z\ in y\ liff\ лексисти {u} {(z\ in u\ land u\ in x)}}}}\ end {вирівняний}\]
плюс всі речення форми
\[\lexists{x}{\lforall{y}{(y \in x \liff A(y))}}\nonumber\]
Перша аксіома говорить, що існує безліч без елементів (тобто\(\emptyset\) існує); друга говорить про те, що множини є extensional; третя, що для будь-яких множин\(X\) і\(Y\), множина\(\{X, Y\}\) існує; четверта, що для будь-якої множини\(X\) , Безліч\(\cup X\) існує, де\(\cup X\) відбувається об'єднання всіх елементів\(X\).
Речення, згадані останніми, в сукупності називаються схемою наївного розуміння. Це, по суті, говорить про те\(A(x)\), що для кожного\(\Setabs{x}{A(x)}\) існує безліч - тож на перший погляд справжня, корисна і, можливо, навіть необхідна аксіома. Його називають «наївним», тому що, як виявляється, це робить цю теорію незадовільною: якщо\(A(y)\) взяти бути\(\lnot y \in y\), ви отримуєте речення,\[\lexists{x}{\lforall{y}{(y \in x \liff \lnot y \in y)}}\nonumber\] і це речення не задовольняється ні в одній структурі.
Приклад\(\PageIndex{5}\)
У сфері мереології відношення батьківства є основоположним відношенням. Так само, як теорії множин, існують теорії батьківства, які аксіоматизують різні концепції (іноді суперечливі) цього відношення.
Мова мереології містить єдиний двомісний присудок символ\(\Obj P\), і\(\Atom{\Obj P}{x, y}\) «означає», що\(x\) є частиною\(y\). Коли ми маємо на увазі це тлумачення, структура цієї мови називається структурою батьківства. Звичайно, не кожна структура для одного двомісного присудка дійсно заслуговує на це ім'я. Щоб мати шанс захопити «батьківство»,\(\Assign{\Obj P}{M}\) потрібно задовольнити деякі умови, які ми можемо скласти як аксіоми теорії батьківства. Наприклад, батьківство - це частковий порядок на об'єктах: кожен об'єкт є частиною (хоча і неналежною частиною) самого себе; жодні два різні об'єкти не можуть бути частинами один одного; частина частини об'єкта сама по собі є частиною цього об'єкта. Зауважте, що в цьому сенсі «є частиною» нагадує «є підмножиною», але не нагадує «є елементом», який не є ні рефлексивним, ні перехідним.
\[\begin{aligned} & \lforall{x}{\Atom{\Obj P}{x,x}}, \\ & \lforall{x}{\lforall{y}{((\Part{x}{y} \land \Part{y}{x}) \lif \eq[x][y])}}, \\ & \lforall{x}{\lforall{y}{\lforall{z}{((\Part{x}{y} \land \Part{y}{z}) \lif \Part{x}{z})}}},\end{aligned}\]
Причому будь-які два об'єкти мають мереологічну суму (об'єкт, який має ці два об'єкти як частини, і мінімальний в цьому відношенні).
\[\lforall{x}{\lforall{y}{\lexists{z}{\lforall{u}{(\Part{z}{u} \liff (\Part{x}{u} \land \Part{y}{u}))}}}}\nonumber\]
Це лише деякі основні принципи батьківства, які розглядають метамедики. Подальші принципи, однак, швидко стають важко сформулювати або записати без попереднього введення деяких визначених відносин. Наприклад, більшість металікарів, зацікавлених у мереології, також розглядають наступне як дійсний принцип: всякий раз, коли об'єкт\(x\) має належну частину\(y\), він також має частину,\(z\) яка не має спільних частин\(y\), і так що злиття з\(y\) і\(z\) є\(x\).