Π§ΠΈΡ‚Π°ΠΉΡ‚Π΅ ΠΊΠ½ΠΈΠ³ΠΈ ΠΎΠ½Π»Π°ΠΉΠ½ Π½Π° Bookidrom.ru! БСсплатныС ΠΊΠ½ΠΈΠ³ΠΈ Π² ΠΎΠ΄Π½ΠΎΠΌ ΠΊΠ»ΠΈΠΊΠ΅

Π§ΠΈΡ‚Π°Ρ‚ΡŒ ΠΎΠ½Π»Π°ΠΉΠ½ Β«ΠŸΠ ΠžΠ“Π ΠΠœΠœΠ˜Π ΠžΠ’ΠΠΠ˜Π• НА Π―Π—Π«ΠšΠ• ΠŸΠ ΠžΠ›ΠžΠ“Β». Π‘Ρ‚Ρ€Π°Π½ΠΈΡ†Π° 62

Автор Π£ Клоксин

ГЛАВА 10. ΠŸΠ ΠžΠ›ΠžΠ“ И ΠœΠΠ’Π•ΠœΠΠ’Π˜Π§Π•Π‘ΠšΠΠ― Π›ΠžΠ“Π˜ΠšΠ

Π―Π·Ρ‹ΠΊ программирования ΠŸΡ€ΠΎΠ»ΠΎΠ³ Π±Ρ‹Π» Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚Π°Π½ ΠΊΠΎΠ»Π»Π΅ΠΊΡ‚ΠΈΠ²ΠΎΠΌ Π²ΠΎ Π³Π»Π°Π²Π΅ с ΠšΠΎΠ»ΠΌΠ΅Ρ€Π°ΡƒΡΡ€ΠΎΠΌ ΠΏΡ€ΠΈΠ±Π»ΠΈΠ·ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎ Π² 1970 Π³ΠΎΠ΄Ρƒ. Π­Ρ‚ΠΎ Π±Ρ‹Π»Π° пСрвая ΠΏΠΎΠΏΡ‹Ρ‚ΠΊΠ° Π² Ρ€Π°Π·Ρ€Π°Π±ΠΎΡ‚ΠΊΠ΅ языка, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ позволял Π±Ρ‹ программисту ΠΎΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ свои Π·Π°Π΄Π°Ρ‡ΠΈ срСдствами матСматичСской Π»ΠΎΠ³ΠΈΠΊΠΈ, Π° Π½Π΅ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ‚Ρ€Π°Π΄ΠΈΡ†ΠΈΠΎΠ½Π½Ρ‹Ρ… для программирования конструкций, ΡƒΠΊΠ°Π·Ρ‹Π²Π°ΡŽΡ‰ΠΈΡ… Ρ‡Ρ‚ΠΎ ΠΈ ΠΊΠΎΠ³Π΄Π° Π΄ΠΎΠ»ΠΆΠ½Π° Π΄Π΅Π»Π°Ρ‚ΡŒ Π²Ρ‹Ρ‡ΠΈΡΠ»ΠΈΡ‚Π΅Π»ΡŒΠ½Π°Ρ машина. Π­Ρ‚Π° идСя нашла ΠΎΡ‚Ρ€Π°ΠΆΠ΅Π½ΠΈΠ΅ Π² Π½Π°Π·Π²Π°Π½ΠΈΠΈ языка программирования Β«ΠŸΡ€ΠΎΠ»ΠΎΠ³Β» (английскоС Π½Π°Π·Π²Π°Π½ΠΈΠ΅ Β«PrologΒ» являСтся сокращСниСм для Programming in Logic.- ΠŸΠ΅Ρ€Π΅Π².).

Π’ этой ΠΊΠ½ΠΈΠ³Π΅ основноС Π²Π½ΠΈΠΌΠ°Π½ΠΈΠ΅ Π±Ρ‹Π»ΠΎ ΡƒΠ΄Π΅Π»Π΅Π½ΠΎ вопросам, связанным с использованиСм ΠŸΡ€ΠΎΠ»ΠΎΠ³Π° Π² качСствС ΠΈΠ½ΡΡ‚Ρ€ΡƒΠΌΠ΅Π½Ρ‚Π°Π»ΡŒΠ½ΠΎΠ³ΠΎ срСдства для Ρ€Π΅ΡˆΠ΅Π½ΠΈΡ практичСских Π·Π°Π΄Π°Ρ‡. ΠŸΡ€ΠΈ этом Π½ΠΈΡ‡Π΅Π³ΠΎ Π½Π΅ Π³ΠΎΠ²ΠΎΡ€ΠΈΠ»ΠΎΡΡŒ ΠΎ путях достиТСния ΠΊΠΎΠ½Π΅Ρ‡Π½ΠΎΠΉ Ρ†Π΅Π»ΠΈ – создании систСмы логичСского программирования, шагом ΠΊ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ являСтся ΠŸΡ€ΠΎΠ»ΠΎΠ³. Π’ этой Π³Π»Π°Π²Π΅ ΠΌΡ‹ намСрСваСмся отчасти ΠΈΡΠΏΡ€Π°Π²ΠΈΡ‚ΡŒ это нСсоотвСтствиС, рассмотрСв Π²ΠΊΡ€Π°Ρ‚Ρ†Π΅ связь ΠŸΡ€ΠΎΠ»ΠΎΠ³Π° с матСматичСской Π»ΠΎΠ³ΠΈΠΊΠΎΠΉ ΠΈ вопрос ΠΎ Ρ‚ΠΎΠΌ, Π² ΠΊΠ°ΠΊΠΎΠΉ стСпСни ΠΏΡ€ΠΎΠ³Ρ€Π°ΠΌΠΌΠΈΡ€ΠΎΠ²Π°Π½ΠΈΠ΅ Π½Π° ΠŸΡ€ΠΎΠ»ΠΎΠ³Π΅ соотвСтствуСт ΠΈΠ΄Π΅Π΅ логичСского программирования.

10.1. ΠšΡ€Π°Ρ‚ΠΊΠΎΠ΅ Π²Π²Π΅Π΄Π΅Π½ΠΈΠ΅ Π² исчислСниС ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ²

Если ΠΌΡ‹ Π½Π°ΠΌΠ΅Ρ€Π΅Π½Ρ‹ ΠΎΠ±ΡΡƒΠΆΠ΄Π°Ρ‚ΡŒ связь ΠŸΡ€ΠΎΠ»ΠΎΠ³Π° с матСматичСской Π»ΠΎΠ³ΠΈΠΊΠΎΠΉ, Ρ‚ΠΎ ΠΏΡ€Π΅ΠΆΠ΄Π΅ всСго Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡƒΡΡ‚Π°Π½ΠΎΠ²ΠΈΡ‚ΡŒ, Ρ‡Ρ‚ΠΎ ΠΌΡ‹ ΠΏΠΎΠ½ΠΈΠΌΠ°Π΅ΠΌ ΠΏΠΎΠ΄ Π»ΠΎΠ³ΠΈΠΊΠΎΠΉ. ΠŸΠ΅Ρ€Π²ΠΎΠ½Π°Ρ‡Π°Π»ΡŒΠ½ΠΎ Π»ΠΎΠ³ΠΈΠΊΠ° Ρ€Π°Π·Π²ΠΈΠ²Π°Π»Π°ΡΡŒ ΠΊΠ°ΠΊ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ способ прСдставлСния ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Π½ΠΎΠ³ΠΎ класса высказываний, Ρ‚Π°ΠΊ Ρ‡Ρ‚ΠΎΠ±Ρ‹ ΠΌΠΎΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΡ Ρ„ΠΎΡ€ΠΌΠ°Π»ΡŒΠ½ΡƒΡŽ ΠΏΡ€ΠΎΡ†Π΅Π΄ΡƒΡ€Ρƒ, ΠΏΡ€ΠΎΠ²Π΅Ρ€ΠΈΡ‚ΡŒ, справСдливы ΠΎΠ½ΠΈ ΠΈΠ»ΠΈ Π½Π΅Ρ‚. Π’Π°ΠΊΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ, Π»ΠΎΠ³ΠΈΠΊΠ° ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ использована для выраТСния высказываний, ΠΎΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΠΉ ΠΌΠ΅ΠΆΠ΄Ρƒ высказываниями ΠΈ ΠΏΡ€Π°Π²ΠΈΠ» Π²Ρ‹Π²ΠΎΠ΄Π° ΠΎΠ΄Π½ΠΈΡ… высказываний ΠΈΠ· Π΄Ρ€ΡƒΠ³ΠΈΡ…. ЛогичСскоС исчислСниС ΡΠΏΠ΅Ρ†ΠΈΠ°Π»ΡŒΠ½ΠΎΠ³ΠΎ Π²ΠΈΠ΄Π°, ΠΎ ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΌ Π±ΡƒΠ΄Π΅Ρ‚ ΠΈΠ΄Ρ‚ΠΈ Ρ€Π΅Ρ‡ΡŒ Π² этой Π³Π»Π°Π²Π΅, называСтся исчислСниС ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ². Π—Π΄Π΅ΡΡŒ ΠΌΡ‹ лишь Π·Π°Ρ‚Ρ€ΠΎΠ½Π΅ΠΌ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Π΅ вопросы исчислСния ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ². Π₯ΠΎΡ€ΠΎΡˆΠΈΠΌ Π²Π²Π΅Π΄Π΅Π½ΠΈΠ΅ΠΌ Π² ΠΌΠ°Ρ‚Π΅ΠΌΠ°Ρ‚ΠΈΡ‡Π΅ΡΠΊΡƒΡŽ Π»ΠΎΠ³ΠΈΠΊΡƒ являСтся ΠΊΠ½ΠΈΠ³Π° Hodges W. Logic, Penguin Books, 1977. Π‘ΠΎΠ»Π΅Π΅ ΠΏΠΎΠ΄Ρ€ΠΎΠ±Π½ΠΎΠ΅ обсуТдСниС ΠΏΡ€Π΅Π΄ΠΌΠ΅Ρ‚Π° Π΄Π°Π½ΠΎ Π² ΠΊΠ½ΠΈΠ³Π΅ Mendelson E. Intro ductiontoMathematicalLogic, VanNostrandReinhold.[15] Π’Ρ‹ Ρ‚Π°ΠΊ ΠΆΠ΅ ΠΌΠΎΠΆΠ΅Ρ‚Π΅ ΠΎΠ±Ρ€Π°Ρ‚ΠΈΡ‚ΡŒΡΡ ΠΊ любой ΠΊΠ½ΠΈΠ³Π΅ ΠΏΠΎ матСматичСской Π»ΠΎΠ³ΠΈΠΊΠ΅. Другая ΠΊΠ½ΠΈΠ³Π°, ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡŽΡ‰Π°Ρ интСрСс, написана Chin L. Π‘, Lee R. Π‘.-Π’. Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.[16]

Для Ρ‚ΠΎΠ³ΠΎ Ρ‡Ρ‚ΠΎΠ±Ρ‹ Π΄Π΅Π»Π°Ρ‚ΡŒ высказывания ΠΎ ΠΌΠΈΡ€Π΅, Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡƒΠΌΠ΅Ρ‚ΡŒ ΠΎΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Ρ‹ этого ΠΌΠΈΡ€Π°. Π’ исчислСнии ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ² ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Ρ‹ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡŽΡ‚ΡΡ с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ Ρ‚Π΅Ρ€ΠΌΠΎΠ². Π‘ΡƒΡ‰Π΅ΡΡ‚Π²ΡƒΡŽΡ‚ Ρ‚Π΅Ρ€ΠΌΡ‹ Ρ‚Ρ€Π΅Ρ… Ρ‚ΠΈΠΏΠΎΠ²:

β€’ ΠšΠΎΠ½ΡΡ‚Π°Π½Ρ‚Π°. Π­Ρ‚ΠΎ символ, ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°ΡŽΡ‰ΠΈΠΉ ΠΈΠ½Π΄ΠΈΠ²ΠΈΠ΄ΡƒΠ°Π»ΡŒΠ½Ρ‹ΠΉ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ ΠΈΠ»ΠΈ понятиС. ΠšΠΎΠ½ΡΡ‚Π°Π½Ρ‚Ρ‹ ΠΌΠΎΠΆΠ½ΠΎ Ρ€Π°ΡΡΠΌΠ°Ρ‚Ρ€ΠΈΠ²Π°Ρ‚ΡŒ ΠΊΠ°ΠΊ Π°Ρ‚ΠΎΠΌΡ‹ языка ΠŸΡ€ΠΎΠ»ΠΎΠ³ ΠΈ Π΄Π°Π»Π΅Π΅ Π±ΡƒΠ΄Π΅Ρ‚ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ ΡΠΎΠΎΡ‚Π²Π΅Ρ‚ΡΡ‚Π²ΡƒΡŽΡ‰Π°Ρ Ρ„ΠΎΡ€ΠΌΠ° записи. Π’Π°ΠΊ, Π³Ρ€Π΅ΠΊ, Π°Π³Π°Ρ‚Π° ΠΈ ΠΌΠΈΡ€ ΡΠ²Π»ΡΡŽΡ‚ΡΡ константами.

β€’ ΠŸΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Π°Ρ. Π­Ρ‚ΠΎ символ, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΡ‹ΠΉ Π² Ρ€Π°Π·Π½ΠΎΠ΅ врСмя для обозначСния Ρ€Π°Π·Π½Ρ‹Ρ… ΠΈΠ½Π΄ΠΈΠ²ΠΈΠ΄ΡƒΠ°Π»ΡŒΠ½Ρ‹Ρ… ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ΠΎΠ². ΠŸΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ вводятся лишь ΠΎΠ΄Π½ΠΎΠ²Ρ€Π΅ΠΌΠ΅Π½Π½ΠΎ с ΠΊΠ²Π°Π½Ρ‚ΠΎΡ€Π°ΠΌΠΈ, ΠΎ ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… Π±ΡƒΠ΄Π΅Ρ‚ сказано Π΄Π°Π»Π΅Π΅. Π’Π΅Ρ€ΠΌΡ‹, ΡΠ²Π»ΡΡŽΡ‰ΠΈΠ΅ΡΡ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹ΠΌΠΈ, ΠΌΠΎΠΆΠ½ΠΎ Ρ€Π°ΡΡΠΌΠ°Ρ‚Ρ€ΠΈΠ²Π°Ρ‚ΡŒ ΠΊΠ°ΠΊ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅ языка ΠŸΡ€ΠΎΠ»ΠΎΠ³ ΠΈ Π΄Π°Π»Π΅Π΅ для ΠΈΡ… обозначСния Π±ΡƒΠ΄Π΅Ρ‚ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒΡΡ синтаксис, принятый Π² ΠŸΡ€ΠΎΠ»ΠΎΠ³Π΅. Π’Π°ΠΊΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ, X, Π§Π΅Π»ΠΎΠ²Π΅ΠΊ ΠΈ Π“Ρ€Π΅ΠΊ ΡΠ²Π»ΡΡŽΡ‚ΡΡ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹ΠΌΠΈ.

β€’ Боставной Ρ‚Π΅Ρ€ΠΌ. Боставной Ρ‚Π΅Ρ€ΠΌ состоит ΠΈΠ· Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½ΠΎΠ³ΠΎ символа ΠΈ упорядочСнного мноТСства Ρ‚Π΅Ρ€ΠΌΠΎΠ², ΡΠ²Π»ΡΡŽΡ‰ΠΈΡ…ΡΡ Π΅Π³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°ΠΌΠΈ. ИдСя состоит Π² Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ составной Ρ‚Π΅Ρ€ΠΌ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ Ρ‚ΠΎΡ‚ ΠΈΠ»ΠΈ ΠΈΠ½ΠΎΠΉ ΠΈΠ½Π΄ΠΈΠ²ΠΈΠ΄ΡƒΠ°Π»ΡŒΠ½Ρ‹ΠΉ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚, зависящий ΠΎΡ‚ Π΄Ρ€ΡƒΠ³ΠΈΡ… ΠΈΠ½Π΄ΠΈΠ²ΠΈΠ΄ΡƒΠ°Π»ΡŒΠ½Ρ‹Ρ… ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ΠΎΠ², прСдставлСнных Π΅Π³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°ΠΌΠΈ. Π€ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹ΠΉ символ описываСт Ρ…Π°Ρ€Π°ΠΊΡ‚Π΅Ρ€ зависимости. НапримСр, ΠΌΠΎΠΆΠ½ΠΎ Π±Ρ‹Π»ΠΎ Π±Ρ‹ ΠΈΠΌΠ΅Ρ‚ΡŒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹ΠΉ символ, ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°ΡŽΡ‰ΠΈΠΉ «расстояниС» ΠΈ ΠΈΠΌΠ΅ΡŽΡ‰ΠΈΠΉ Π΄Π²Π° Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°. Π’ этом случаС составной Ρ‚Π΅Ρ€ΠΌ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ расстояниС ΠΌΠ΅ΠΆΠ΄Ρƒ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π°ΠΌΠΈ, прСдставлСнными Π΅Π³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°ΠΌΠΈ. Боставной Ρ‚Π΅Ρ€ΠΌ ΠΌΠΎΠΆΠ½ΠΎ Ρ€Π°ΡΡΠΌΠ°Ρ‚Ρ€ΠΈΠ²Π°Ρ‚ΡŒ ΠΊΠ°ΠΊ структуру языка ΠŸΡ€ΠΎΠ»ΠΎΠ³, ΠΈΠΌΠ΅ΡŽΡ‰ΡƒΡŽ Π² качСствС Ρ„ΡƒΠ½ΠΊΡ‚ΠΎΡ€Π° Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹ΠΉ символ. БоставныС Ρ‚Π΅Ρ€ΠΌΡ‹ Π±ΡƒΠ΄ΡƒΡ‚ Π·Π°ΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒΡΡ ΠΏΠΎ ΠΏΡ€Π°Π²ΠΈΠ»Π°ΠΌ синтаксиса ΠŸΡ€ΠΎΠ»ΠΎΠ³Π° Ρ‚Π°ΠΊ, Ρ‡Ρ‚ΠΎ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, ΠΆΠ΅Π½Π°(Π³Π΅Π½Ρ€ΠΈ) ΠΌΠΎΠΆΠ΅Ρ‚ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Ρ‚ΡŒ ΠΆΠ΅Π½Ρƒ Π“Π΅Π½Ρ€ΠΈ, расстояниС(Ρ‚ΠΎΡ‡ΠΊΠ°1, X) ΠΌΠΎΠΆΠ΅Ρ‚ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Ρ‚ΡŒ расстояниС ΠΌΠ΅ΠΆΠ΄Ρƒ Π½Π΅ΠΊΠΎΡ‚ΠΎΡ€ΠΎΠΉ Π·Π°Π΄Π°Π½Π½ΠΎΠΉ Ρ‚ΠΎΡ‡ΠΊΠΎΠΉ ΠΈ ΠΊΠ°ΠΊΠΈΠΌ-Ρ‚ΠΎ Π΄Ρ€ΡƒΠ³ΠΈΠΌ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ΠΎΠΌ, ΠΊΠΎΡ‚ΠΎΡ€Ρ‹ΠΉ Π±ΡƒΠ΄Π΅Ρ‚ ΡƒΠΊΠ°Π·Π°Π½, Π° классы(мэри, Π½Π°_ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΉ_ дСнь_послС(Π₯)) ΠΌΠΎΠΆΠ΅Ρ‚ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Ρ‚ΡŒ классы, Π² ΠΊΠΎΡ‚ΠΎΡ€Ρ‹Ρ… ΠΏΡ€Π΅ΠΏΠΎΠ΄Π°Π²Π°Π»Π° ΠœΡΡ€ΠΈ Π½Π° ΡΠ»Π΅Π΄ΡƒΡŽΡ‰ΠΈΠΉ послС X (Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΡƒΠΊΠ°Π·Π°Ρ‚ΡŒ дСнь).

Π’Π°ΠΊΠΈΠΌ ΠΎΠ±Ρ€Π°Π·ΠΎΠΌ, способы, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΡ‹Π΅ для прСдставлСния ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ΠΎΠ² Π² исчислСнии ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ², Π² точности ΡΠΎΠΎΡ‚Π²Π΅Ρ‚ΡΡ‚Π²ΡƒΡŽΡ‚ способам, ΠΈΠΌΠ΅ΡŽΡ‰ΠΈΠΌΡΡ для этого Π² ΠŸΡ€ΠΎΠ»ΠΎΠ³Π΅.

Для Ρ‚ΠΎΠ³ΠΎ Ρ‡Ρ‚ΠΎΠ±Ρ‹ Π΄Π΅Π»Π°Ρ‚ΡŒ высказывания ΠΎΠ± ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π°Ρ…, Π½Π΅ΠΎΠ±Ρ…ΠΎΠ΄ΠΈΠΌΠΎ ΠΈΠΌΠ΅Ρ‚ΡŒ Π²ΠΎΠ·ΠΌΠΎΠΆΠ½ΠΎΡΡ‚ΡŒ ΠΎΠΏΠΈΡΡ‹Π²Π°Ρ‚ΡŒ ΠΎΡ‚Π½ΠΎΡˆΠ΅Π½ΠΈΡ ΠΌΠ΅ΠΆΠ΄Ρƒ ΠΎΠ±ΡŠΠ΅ΠΊΡ‚Π°ΠΌΠΈ. Π­Ρ‚ΠΎ дСлаСтся с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ². АтомарноС высказываниС (атомарная Ρ„ΠΎΡ€ΠΌΡƒΠ»Π°) состоит ΠΈΠ· ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚Π½ΠΎΠ³ΠΎ символа ΠΈ ΡΠΎΠΎΡ‚Π²Π΅Ρ‚ΡΡ‚Π²ΡƒΡŽΡ‰Π΅Π³ΠΎ Π΅ΠΌΡƒ упорядочСнного мноТСства Ρ‚Π΅Ρ€ΠΌΠΎΠ², ΡΠ²Π»ΡΡŽΡ‰ΠΈΡ…ΡΡ Π΅Π³ΠΎ Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π°ΠΌΠΈ. Π­Ρ‚ΠΎ ΠΏΠΎΠ»Π½ΠΎΡΡ‚ΡŒΡŽ Π°Π½Π°Π»ΠΎΠ³ΠΈΡ‡Π½ΠΎ Ρ†Π΅Π»Π΅Π²ΠΎΠΌΡƒ ΡƒΡ‚Π²Π΅Ρ€ΠΆΠ΄Π΅Π½ΠΈΡŽ ΠŸΡ€ΠΎΠ»ΠΎΠ³Π°. Π’Π°ΠΊ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊ(мэри), Π²Π»Π°Π΄Π΅Π΅Ρ‚(Π₯,осСл(Π₯)) ΠΈ нравится (ΠœΡƒΠΆΡ‡ΠΈΠ½Π°, Π²ΠΈΠ½ΠΎ) ΡΠ²Π»ΡΡŽΡ‚ΡΡ Π°Ρ‚ΠΎΠΌΠ°Ρ€Π½Ρ‹ΠΌΠΈ высказываниями (Π°Ρ‚ΠΎΠΌΠ°Ρ€Π½Ρ‹ΠΌΠΈ Ρ„ΠΎΡ€ΠΌΡƒΠ»Π°ΠΌΠΈ). Π’ языкС ΠŸΡ€ΠΎΠ»ΠΎΠ³ структура ΠΌΠΎΠΆΠ΅Ρ‚ Π±Ρ‹Ρ‚ΡŒ использована ΠΊΠ°ΠΊ Π² качСствС Ρ†Π΅Π»Π΅Π²ΠΎΠ³ΠΎ утвСрТдСния, Ρ‚Π°ΠΊ ΠΈ Π² качСствС Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚Π° для Π΄Ρ€ΡƒΠ³ΠΎΠΉ структуры. Π’ исчислСнии ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ² Π΄Π΅Π»ΠΎ обстоит ΠΈΠ½Π°Ρ‡Π΅. Π’Π°ΠΌ имССтся строгоС Ρ€Π°Π·Π΄Π΅Π»Π΅Π½ΠΈΠ΅ ΠΌΠ΅ΠΆΠ΄Ρƒ Ρ„ΡƒΠ½ΠΊΡ†ΠΈΠΎΠ½Π°Π»ΡŒΠ½Ρ‹ΠΌΠΈ символами, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΡ‹ΠΌΠΈ Π² качСствС Ρ„ΡƒΠ½ΠΊΡ‚ΠΎΡ€ΠΎΠ² для построСния Π°Ρ€Π³ΡƒΠΌΠ΅Π½Ρ‚ΠΎΠ², ΠΈ ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚Π½Ρ‹ΠΌΠΈ символами, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΡ‹ΠΌΠΈ Π² качСствС Ρ„ΡƒΠ½ΠΊΡ‚ΠΎΡ€ΠΎΠ² для построСния высказываний (Ρ„ΠΎΡ€ΠΌΡƒΠ»).

Π˜ΡΠΏΠΎΠ»ΡŒΠ·ΡƒΡ Π°Ρ‚ΠΎΠΌΠ°Ρ€Π½Ρ‹Π΅ высказывания, ΠΌΠΎΠΆΠ½ΠΎ Ρ€Π°Π·Π»ΠΈΡ‡Π½Ρ‹ΠΌΠΈ способами ΡΠΎΠ·Π΄Π°Π²Π°Ρ‚ΡŒ составныС высказывания. ИмСнно здСсь Π½Π°Ρ‡ΠΈΠ½Π°ΡŽΡ‚ ΠΏΠΎΡΠ²Π»ΡΡ‚ΡŒΡΡ понятия Π½Π΅ ΠΈΠΌΠ΅ΡŽΡ‰ΠΈΠ΅ нСпосрСдствСнных Π°Π½Π°Π»ΠΎΠ³ΠΎΠ² Π² языкС ΠŸΡ€ΠΎΠ»ΠΎΠ³. БущСствуСт нСсколько способов построСния Π±ΠΎΠ»Π΅Π΅ слоТных высказываний ΠΈΠ· Π±ΠΎΠ»Π΅Π΅ простых. ΠŸΡ€Π΅ΠΆΠ΄Π΅ всСго, ΠΌΠΎΠΆΠ½ΠΎ ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΠΎΠ²Π°Ρ‚ΡŒ логичСскиС связки. Π’Π°ΠΊΠΈΠΌ способом ΠΌΠΎΠΆΠ½ΠΎ Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚ΡŒ понятия 'Π½Π΅', 'ΠΈ', 'ΠΈΠ»ΠΈ', 'Π²Π»Π΅Ρ‡Π΅Ρ‚' ΠΈ 'являСтся эквивалСнтным'. Π”Π°Π»Π΅Π΅ ΠΏΡ€ΠΈΠ²Π΅Π΄Π΅Π½ΠΎ ΠΊΡ€Π°Ρ‚ΠΊΠΎΠ΅ описаниС этих связок ΠΈ Π²ΠΊΠ»Π°Π΄Ρ‹Π²Π°Π΅ΠΌΡ‹Ρ… Π² Π½ΠΈΡ… Π·Π½Π°Ρ‡Π΅Π½ΠΈΠΉ. Π—Π΄Π΅ΡΡŒ ? ΠΈ ? ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΡŽΡ‚ΡΡ для обозначСния ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ»ΡŒΠ½Ρ‹Ρ… высказываний (Ρ„ΠΎΡ€ΠΌΡƒΠ»). Π’ ΡΠ»Π΅Π΄ΡƒΡŽΡ‰Π΅ΠΉ Ρ‚Π°Π±Π»ΠΈΡ†Π΅ приводятся традиционная Ρ„ΠΎΡ€ΠΌΠ° записи высказываний, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΠ°Ρ Π² исчислСнии ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ², ΠΈ Ρ„ΠΎΡ€ΠΌΠ° записи, ΠΈΡΠΏΠΎΠ»ΡŒΠ·ΡƒΠ΅ΠΌΠ°Ρ Π² этой Π³Π»Π°Π²Π΅.

ЛогичСская связка Π˜ΡΡ‡ΠΈΡΠ»Π΅Π½ΠΈΠ΅ ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ² ΠžΠ±ΠΎΠ·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ Π² ΠΊΠ½ΠΈΠ³Π΅ Π—Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ ΠžΡ‚Ρ€ΠΈΡ†Π°Π½ΠΈΠ΅ βŒ‰Ξ± ~Ξ± Β«Π½Π΅ Ξ±Β» ΠšΠΎΠ½ΡŠΡŽΠ½ΠΊΡ†ΠΈΡ α∧β Ξ±&Ξ² «α ΠΈ Ξ²Β» Π”ΠΈΠ·ΡŠΡŽΠ½ΠΊΡ†ΠΈΡ α∨β Ξ±#Ξ² «α ΠΈΠ»ΠΈ Ξ²Β» Π˜ΠΌΠΏΠ»ΠΈΠΊΠ°Ρ†ΠΈΡ Ξ±βŠƒΞ² Ξ±-β€ΊΞ² «α Π²Π»Π΅Ρ‡Π΅Ρ‚ Ξ²Β» Π­ΠΊΠ²ΠΈΠ²Π°Π»Π΅Π½Ρ‚Π½ΠΎΡΡ‚ΡŒ α≑β Ξ±β€Ή-β€ΊΞ² «α эквивалСнтна Ξ²Β»

Π’Π°ΠΊ, Π½Π°ΠΏΡ€ΠΈΠΌΠ΅Ρ€, конструкция

ΠΌΡƒΠΆΡ‡ΠΈΠ½Π°(Ρ„Ρ€Π΅Π΄) # ΠΆΠ΅Π½Ρ‰ΠΈΠ½Π° (Ρ„Ρ€Π΅Π΄)

ΠΌΠΎΠ³Π»Π° Π±Ρ‹ Π±Ρ‹Ρ‚ΡŒ использована для прСдставлСния высказывания ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Π€Ρ€Π΅Π΄ являСтся ΠΌΡƒΠΆΡ‡ΠΈΠ½ΠΎΠΉ ΠΈΠ»ΠΈ Π€Ρ€Π΅Π΄ являСтся ΠΆΠ΅Π½Ρ‰ΠΈΠ½ΠΎΠΉ. ΠšΠΎΠ½ΡΡ‚Ρ€ΡƒΠΊΡ†ΠΈΡ

ΠΌΡƒΠΆΡ‡ΠΈΠ½Π°(Π΄ΠΆΠΎΠ½) -β€Ί Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊ (Π΄ΠΆΠΎΠ½)

ΠΌΠΎΠ³Π»Π° Π±Ρ‹ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡ‚ΡŒ высказываниС: Ρ‚ΠΎ, Ρ‡Ρ‚ΠΎ Π”ΠΆΠΎΠ½ являСтся ΠΌΡƒΠΆΡ‡ΠΈΠ½ΠΎΠΉ, Π²Π»Π΅Ρ‡Π΅Ρ‚ Ρ‚ΠΎ, Ρ‡Ρ‚ΠΎ ΠΎΠ½ являСтся Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊΠΎΠΌ (Ссли Π”ΠΆΠΎΠ½ ΠΌΡƒΠΆΡ‡ΠΈΠ½Π°, Ρ‚ΠΎ ΠΎΠ½ – Ρ‡Π΅Π»ΠΎΠ²Π΅ΠΊ). ΠŸΠΎΠ½ΡΡ‚ΠΈΡ ΠΈΠΌΠΏΠ»ΠΈΠΊΠ°Ρ†ΠΈΠΈ ΠΈ эквивалСнтности ΠΈΠ½ΠΎΠ³Π΄Π° ΠΏΡ€ΠΈ ΠΏΠ΅Ρ€Π²ΠΎΠΌ знакомствС с Π½ΠΈΠΌΠΈ ΠΏΡ€Π΅Π΄ΡΡ‚Π°Π²Π»ΡΡŽΡ‚ΡΡ нСсколько слоТными. ΠœΡ‹ Π³ΠΎΠ²ΠΎΡ€ΠΈΠΌ, Ρ‡Ρ‚ΠΎ Ξ± Π²Π»Π΅Ρ‡Π΅Ρ‚ Ξ², Ссли всякий Ρ€Π°Π·, ΠΊΠΎΠ³Π΄Π° Ξ± истинно, Ρ‚ΠΎ Ξ² Ρ‚Π°ΠΊΠΆΠ΅ истинно. ΠœΡ‹ Π³ΠΎΠ²ΠΎΡ€ΠΈΠΌ, Ρ‡Ρ‚ΠΎ Ξ± эквивалСнтно Ξ², Ссли Ξ± истинно Π² точности Π² Ρ‚Π΅Ρ… ΠΆΠ΅ случаях, Ρ‡Ρ‚ΠΎ ΠΈ Ξ². Π’ Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎΡΡ‚ΠΈ, эти понятия ΠΌΠΎΠ³ΡƒΡ‚ Π±Ρ‹Ρ‚ΡŒ ΠΎΠΏΡ€Π΅Π΄Π΅Π»Π΅Π½Ρ‹ Ρ‡Π΅Ρ€Π΅Π· понятия 'ΠΈ', 'ΠΈΠ»ΠΈ', 'Π½Π΅'. А ΠΈΠΌΠ΅Π½Π½ΠΎ:

Ξ±-β€ΊΞ² Π·Π½Π°Ρ‡ΠΈΡ‚ Ρ‚ΠΎ ΠΆΠ΅ самоС, Ρ‡Ρ‚ΠΎ (~Ξ±)#Ξ²

Ξ±β€Ή-β€ΊΞ² Π·Π½Π°Ρ‡ΠΈΡ‚ Ρ‚ΠΎ ΠΆΠ΅ самоС, Ρ‡Ρ‚ΠΎ ΠΈ (Ξ±&Ξ²)#(~Ξ±&~Ξ²)

Ξ±β€Ή-β€ΊΞ² Ρ‚Π°ΠΊΠΆΠ΅ Π·Π½Π°Ρ‡ΠΈΡ‚ Ρ‚ΠΎ ΠΆΠ΅ самоС, Ρ‡Ρ‚ΠΎ ΠΈ (Ξ±-β€ΊΞ²)&(Ξ±-β€ΊΞ²)

Π”ΠΎ сих ΠΏΠΎΡ€ Π½ΠΈΡ‡Π΅Π³ΠΎ Π½Π΅ Π±Ρ‹Π»ΠΎ сказано ΠΎ Ρ‚ΠΎΠΌ, Ρ‡Ρ‚ΠΎ Π·Π½Π°Ρ‡Π°Ρ‚ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Π΅, входящиС Π² состав высказывания. Π’ Π΄Π΅ΠΉΡΡ‚Π²ΠΈΡ‚Π΅Π»ΡŒΠ½ΠΎΡΡ‚ΠΈ, использованиС ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½Ρ‹Ρ… ΠΈΠΌΠ΅Π΅Ρ‚ смысл лишь Π² случаС, ΠΊΠΎΠ³Π΄Π° ΠΎΠ½ΠΈ вводятся с ΠΏΠΎΠΌΠΎΡ‰ΡŒΡŽ ΠΊΠ²Π°Π½Ρ‚ΠΎΡ€ΠΎΠ². ΠšΠ²Π°Π½Ρ‚ΠΎΡ€Ρ‹ ΠΏΠΎΠ·Π²ΠΎΠ»ΡΡŽΡ‚ Π΄Π΅Π»Π°Ρ‚ΡŒ высказывания ΠΎ мноТСствах ΠΎΠ±ΡŠΠ΅ΠΊΡ‚ΠΎΠ² ΠΈ Ρ„ΠΎΡ€ΠΌΡƒΠ»ΠΈΡ€ΠΎΠ²Π°Ρ‚ΡŒ утвСрТдСния, истинныС для этих мноТСств. Π’ исчислСнии ΠΏΡ€Π΅Π΄ΠΈΠΊΠ°Ρ‚ΠΎΠ² ΠΈΠΌΠ΅ΡŽΡ‚ΡΡ Π΄Π²Π° ΠΊΠ²Π°Π½Ρ‚ΠΎΡ€Π°. Если Ξ½ ΠΎΠ±ΠΎΠ·Π½Π°Ρ‡Π°Π΅Ρ‚ ΠΏΠ΅Ρ€Π΅ΠΌΠ΅Π½Π½ΡƒΡŽ, Π° ρ – это ΠΏΡ€ΠΎΠΈΠ·Π²ΠΎΠ»ΡŒΠ½ΠΎΠ΅ высказываниС, Ρ‚ΠΎ ΠΊΠΎΡ€ΠΎΡ‚ΠΊΠΎ Π·Π½Π°Ρ‡Π΅Π½ΠΈΠ΅ ΠΊΠ²Π°Π½Ρ‚ΠΎΡ€ΠΎΠ² ΠΌΠΎΠΆΠ½ΠΎ Π²Ρ‹Ρ€Π°Π·ΠΈΡ‚ΡŒ Ρ‚Π°ΠΊ: