Skip to main content
LibreTexts - Ukrayinska

5.1: Вступ

  1. Last updated
  2. Save as PDF
  • Page ID
    52993

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

    Для того, щоб розвинути теорію і метатеорію логіки першого порядку, ми повинні спочатку визначити синтаксис і семантику її виразів. Вирази логіки першого порядку є термінами і формулами. Терміни формуються зі змінних, постійних символів та символів функцій. Формули, в свою чергу, утворюються з присудкових символів разом з членами (вони утворюють найменші, «атомні» формули), а потім з атомних формул ми можемо формувати більш складні, використовуючи логічні зв'язки і квантори. Існує багато різних способів встановити правила формування; ми наводимо лише один можливий. Інші системи вибиратимуть різні символи, вибиратимуть різні набори з'єднань як примітивні, використовуватимуть дужки по-різному (або навіть не зовсім, як у випадку з так званими польськими позначеннями). Однак, що всі підходи мають спільне, полягає в тому, що правила формування визначають набір термінів і формул індуктивно. Якщо все зроблено належним чином, кожен вираз може призвести до суті лише одним способом відповідно до правил формування. Індуктивне визначення, що призводить до виразів, які є однозначно читабельними, означає, що ми можемо дати значення цим виразів за допомогою того ж методу - індуктивного визначення.

    Надання значення виразів - область семантики. Центральне поняття в семантиці - це задоволення в структурі. Структура надає значення будівельним блокам мови: домен - це непорожній набір об'єктів. Квантифікатори інтерпретуються як ранжування над цією областю, постійним символам присвоюються елементи в області, символам функцій присвоюються функції від області до себе, а символам предикатів присвоюються відносини на області. Домен разом із завданнями до базового словникового запасу становить структуру. Змінні можуть з'являтися у формулах, і для того, щоб дати семантику, ми також повинні привласнити їм елементи домену — це присвоєння змінної. Зв'язка задоволення, нарешті, об'єднує їх. Формула може бути задоволена в структурі\(\Struct{M}\) відносно змінної присвоєння\(s\), записаної як\(\Sat[,s]{M}{A}\). Це співвідношення також визначається індукцією на структуру\(A\), використовуючи таблиці істинності для логічних зв'язків, щоб визначити, скажімо, задоволення з\(A \land B\) точки зору задоволення (чи ні)\(A\) і\(B\). Потім з'ясовується, що присвоєння змінної не має значення, якщо формула\(A\) є реченням, тобто не має вільних змінних, і тому ми можемо говорити про те, що пропозиції просто задовольняються (чи ні) в структурах.

    На основі співвідношення задоволеності\(\Sat{M}{A}\) для речень ми можемо визначити основні смислові поняття дійсності, спричинності та задовільності. Речення є дійсним\(\Entails A\), якщо кожна структура його задовольняє. Це тягне за собою набір пропозицій\(\Gamma \Entails A\), якщо кожна структура, яка задовольняє всі пропозиції в\(\Gamma\) також задовольняє\(A\). І набір пропозицій задовольняє, якщо якась структура задовольняє всі пропозиції в ньому одночасно. Оскільки формули індуктивно визначені, а задоволення, в свою чергу, визначається індукцією на структуру формул, ми можемо використовувати індукцію, щоб довести властивості нашої семантики та пов'язати визначені семантичні поняття.