Loading [MathJax]/jax/output/HTML-CSS/jax.js
Skip to main content
LibreTexts - Ukrayinska

6.3: Приклади теорій першого порядку

Template:MathJaxZach

Приклад6.3.1

Теорія строгих лінійних порядків в мові\LangL< аксіоматизована множиною.\lforallx¬x<x,\lforallx\lforally((x<yy<x)x=y),\lforallx\lforally\lforallz((x<yy<z)\lifx<z) Вона повністю захоплює передбачувані структури: кожен строгий лінійний порядок є моделлю цієї системи аксіом, і навпаки, якщоR лінійний порядок на множині X, то структура\StructM з\DomainM=X і\Assign<M=R є моделлю цієї теорії.

Приклад6.3.2

Теорія груп у мові\Obj1 (постійний символ), (символ двомісної функції) аксіоматизується\lforallx\eq[(x\Obj1)][x]\lforallx\lforally\lforallz\eq[(x(yz))][((xy)z)]\lforallx\lexistsy\eq[(xy)][\Obj1]

Приклад6.3.3

Теорія арифметики Пеано аксіоматизується наступними реченнями мовою арифметики\LangLA.

\ [\ почати {вирівняний}
&\ 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(\Obj0)\lforallx(A(x)\lifA(x)))\lif\lforallxA(x)

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

Остання аксіома - це явне визначення<.

Приклад6.3.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 {вирівняний}\]

плюс всі речення форми

\lexistsx\lforally(yx\liffA(y))

Перша аксіома говорить, що існує безліч без елементів (тобто існує); друга говорить про те, що множини є extensional; третя, що для будь-яких множинX іY, множина{X,Y} існує; четверта, що для будь-якої множиниX , БезлічX існує, деX відбувається об'єднання всіх елементівX.

Речення, згадані останніми, в сукупності називаються схемою наївного розуміння. Це, по суті, говорить про теA(x), що для кожного\SetabsxA(x) існує безліч - тож на перший погляд справжня, корисна і, можливо, навіть необхідна аксіома. Його називають «наївним», тому що, як виявляється, це робить цю теорію незадовільною: якщоA(y) взяти бути¬yy, ви отримуєте речення,\lexistsx\lforally(yx\liff¬yy) і це речення не задовольняється ні в одній структурі.

Приклад6.3.5

У сфері мереології відношення батьківства є основоположним відношенням. Так само, як теорії множин, існують теорії батьківства, які аксіоматизують різні концепції (іноді суперечливі) цього відношення.

Мова мереології містить єдиний двомісний присудок символ\ObjP, і\Atom\ObjPx,y «означає», щоx є частиноюy. Коли ми маємо на увазі це тлумачення, структура цієї мови називається структурою батьківства. Звичайно, не кожна структура для одного двомісного присудка дійсно заслуговує на це ім'я. Щоб мати шанс захопити «батьківство»,\Assign\ObjPM потрібно задовольнити деякі умови, які ми можемо скласти як аксіоми теорії батьківства. Наприклад, батьківство - це частковий порядок на об'єктах: кожен об'єкт є частиною (хоча і неналежною частиною) самого себе; жодні два різні об'єкти не можуть бути частинами один одного; частина частини об'єкта сама по собі є частиною цього об'єкта. Зауважте, що в цьому сенсі «є частиною» нагадує «є підмножиною», але не нагадує «є елементом», який не є ні рефлексивним, ні перехідним.

\lforallx\Atom\ObjPx,x,\lforallx\lforally((\Partxy\Partyx)\lif\eq[x][y]),\lforallx\lforally\lforallz((\Partxy\Partyz)\lif\Partxz),

Причому будь-які два об'єкти мають мереологічну суму (об'єкт, який має ці два об'єкти як частини, і мінімальний в цьому відношенні).

\lforallx\lforally\lexistsz\lforallu(\Partzu\liff(\Partxu\Partyu))

Це лише деякі основні принципи батьківства, які розглядають метамедики. Подальші принципи, однак, швидко стають важко сформулювати або записати без попереднього введення деяких визначених відносин. Наприклад, більшість металікарів, зацікавлених у мереології, також розглядають наступне як дійсний принцип: всякий раз, коли об'єктx має належну частинуy, він також має частину,z яка не має спільних частинy, і так що злиття зy іz єx.