Логика второго порядка

Логика второго порядка в математической логике — формальная система, расширяющая логику первого порядка возможностью квантификации общности и существования не только над переменными, но и над предикатами и функциональными символами. Логика второго порядка несводима к логике первого порядка. В свою очередь, она расширяется логикой высших порядков и теорией типов.

Язык и синтаксис

Формальные языки логики второго порядка строятся на основе множества функциональных символов






F




{\displaystyle {\mathcal {F}}}

и множества предикатных символов






P




{\displaystyle {\mathcal {P}}}

. С каждым функциональным и предикатным символом связана арность (число аргументов). Также используются дополнительные символы

  • Символы индивидуальных переменных, обычно



     
    x
    ,
    y
    ,
    z
    ,

    x

    1


    ,

    y

    1


    ,

    z

    1


    ,

    x

    2


    ,

    y

    2


    ,

    z

    2




    {\displaystyle \ x,y,z,x_{1},y_{1},z_{1},x_{2},y_{2},z_{2}}

    и т. д.

  • Символы функциональных переменных



     
    F
    ,
    G
    ,
    H
    ,

    F

    1


    ,

    G

    1


    ,

    H

    1


    ,

    F

    2


    ,

    G

    2


    ,

    H

    2




    {\displaystyle \ F,G,H,F_{1},G_{1},H_{1},F_{2},G_{2},H_{2}}

    и т. д. Каждой функциональной переменной соответствует некоторое положительное число — арность функции.

  • Символы предикатных переменных



     
    P
    ,
    R
    ,
    S
    ,

    P

    1


    ,

    R

    1


    ,

    S

    1


    ,

    P

    2


    ,

    R

    2


    ,

    S

    2




    {\displaystyle \ P,R,S,P_{1},R_{1},S_{1},P_{2},R_{2},S_{2}}

    и т. д. Каждой предикатной переменной соответствует некоторое положительное число — арность предиката.

  • Пропозициональные связи:




    ,

    ,
    ¬
    ,



    {\displaystyle \lor ,\land ,\neg ,\to }

    ,

  • Кванторы общности






    {\displaystyle \forall }

    и существования







    {\displaystyle \exists }

    ,

  • Служебные символы: скобки и запятая.

Перечисленные символы вместе с символами






P




{\displaystyle {\mathcal {P}}}

и






F




{\displaystyle {\mathcal {F}}}

образуют алфавит логики первого порядка. Более сложные конструкции определяются индуктивно.

  • Терм — это символ индивидуальной переменной, либо выражение, которое имеет вид



     
    f
    (

    t

    1


    ,

    ,

    t

    n


    )


    {\displaystyle \ f(t_{1},\ldots ,t_{n})}

    , где




     
    f


    {\displaystyle \ f}

     — функциональный символ арности




     
    n


    {\displaystyle \ n}

    , а




     

    t

    1


    ,

    ,

    t

    n




    {\displaystyle \ t_{1},\ldots ,t_{n}}

     — термы либо выражение вида




     
    F
    (

    t

    1


    ,

    ,

    t

    n


    )


    {\displaystyle \ F(t_{1},\ldots ,t_{n})}

    , где




     
    F


    {\displaystyle \ F}

     — функциональная переменная арности




     
    n


    {\displaystyle \ n}

    , а




     

    t

    1


    ,

    ,

    t

    n




    {\displaystyle \ t_{1},\ldots ,t_{n}}

     — термы.

  • Атом — имеет вид



     
    p
    (

    t

    1


    ,

    ,

    t

    n


    )


    {\displaystyle \ p(t_{1},\ldots ,t_{n})}

    , где




    p


    {\displaystyle p}

     — предикатный символ арности




     
    n


    {\displaystyle \ n}

    , а




     

    t

    1


    ,

    ,

    t

    n




    {\displaystyle \ t_{1},\ldots ,t_{n}}

     — термы или




     
    P
    (

    t

    1


    ,

    ,

    t

    n


    )


    {\displaystyle \ P(t_{1},\ldots ,t_{n})}

    , где




    P


    {\displaystyle P}

     — предикатная переменная арности




     
    n


    {\displaystyle \ n}

    , а




     

    t

    1


    ,

    ,

    t

    n




    {\displaystyle \ t_{1},\ldots ,t_{n}}

     — термы.

  • Формула — это или атом, или одна из следующих конструкций:



    ¬
    A
    ,
    (

    A

    1




    A

    2


    )
    ,
    (

    A

    1




    A

    2


    )
    ,
    (

    A

    1




    A

    2


    )
    ,

    x
    A
    ,

    x
    A
    ,

    F
    A
    ,

    F
    A
    ,

    P
    A
    ,

    P
    A


    {\displaystyle \neg A,(A_{1}\lor A_{2}),(A_{1}\land A_{2}),(A_{1}\to A_{2}),\forall xA,\exists xA,\forall FA,\exists FA,\forall PA,\exists PA}

    , где




     
    A
    ,

    A

    1


    ,

    A

    2




    {\displaystyle \ A,A_{1},A_{2}}

     — формулы, а




     
    x
    ,
    F
    ,
    P


    {\displaystyle \ x,F,P}

     — индивидуальная, функциональная и предикатная переменные. (Конструкции





    F
    A
    ,

    F
    A
    ,

    P
    A
    ,

    P
    A


    {\displaystyle \forall FA,\exists FA,\forall PA,\exists PA}

    являются формулами второго и не первого порядка).

Аксиоматика и доказательство формул

Семантика

В классической логике интерпретация формул логики второго порядка задаётся на модели второго порядка, которая определяется следующими данными.

  • Базовое множество





    D




    {\displaystyle {\mathcal {D}}}

    ,

  • Семантическая функция



    σ


    {\displaystyle \sigma }

    , которая отображает

    • каждый



      n


      {\displaystyle n}

      -арный функциональный символ




      f


      {\displaystyle f}

      из






      F




      {\displaystyle {\mathcal {F}}}

      в




      n


      {\displaystyle n}

      -арную функцию




      σ
      (
      f
      )
      :


      D


      ×

      ×


      D





      D




      {\displaystyle \sigma (f):{\mathcal {D}}\times \ldots \times {\mathcal {D}}\rightarrow {\mathcal {D}}}

      ,

    • каждый



      n


      {\displaystyle n}

      -арный предикатный символ




      p


      {\displaystyle p}

      из






      P




      {\displaystyle {\mathcal {P}}}

      в




      n


      {\displaystyle n}

      -арное отношение




      σ
      (
      p
      )



      D


      ×

      ×


      D




      {\displaystyle \sigma (p)\subseteq {\mathcal {D}}\times \ldots \times {\mathcal {D}}}

      .

Свойства

В отличие от логики первого порядка, логика второго порядка не имеет свойств полноты и компактности. Также в этой логике является неверным утверждение теоремы Лёвенгейма — Скулема.

Примечания

Литература

  1. Henkin, L. (1950). «Completeness in the theory of types». Journal of Symbolic Logic 15 (2): 81-91.
  2. Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
  3. Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0.
  4. Rossberg, M. (2004). «First-Order Logic, Second-Order Logic, and Completeness». in V. Hendricks et al., eds.. First-order logic revisited. Berlin: Logos-Verlag.
  5. Vaananen, J. (2001). «Second-Order Logic and Foundations of Mathematics». Bulletin of Symbolic Logic 7 (4): 504—520.


Рассказать друзьям:
Смотреть:
Моллюски