Задачи по математической логике.

[Sdy]

epros, спасибо за ответ.

epros в сообщении #1414248 писал(а):

Я привык называть законом контрапозиции $(P \to Q) \to (\neg Q \to \neg P)$. Потому что это закон не только в классической логике, но и, например, в конструктивной. Обратное: $(\neg Q \to \neg P) \to (P \to Q)$ - в конструктивной логике не всегда верно, а потому так не называется.

Вас понял.

epros в сообщении #1414248 писал(а):

Надо сказать, что такие доказательства малоинтересны. Если Вы уж решились опираться на двузначность логики, то зачем эти пляски с бубнами? Просто подставьте вместо всех пропозициональных переменных все возможные комбинации логических значений и убедитесь, что тавтология всегда истинна.

То есть подобного вида утверждения в случае, когда я принимаю фактически за аксиомы способы работы с высказываниями посредством логических связок, тоже становятся аксиомами?
Просто именно такие доказательства корректности предоставляются в книге. Но более краткие. И я хотел для себя разобрать эти места поглубже.

beroal, спасибо за ответ.

beroal в сообщении #1414268 писал(а):

Если я правильно понял, вы с помощью доказательства от противного хотите доказать импликацию.

Нет, я хочу обосновать корректность применения метода доказательства от противного в случае, когда мое утверждение имеет вид импликации. Ведь повсеместно в анализе и алгебре приходится от противного идти доказывая утверждения вида $A \Rightarrow B$.

arseniiv, спасибо за ответ.
Вот как раз с общей схемой у меня вопросов нет. Пусть имеется утверждение. $A$. Предположим, что оно неверно, то есть верно $\neg A$. Придём к противоречию, то есть получим, что $(\neg A \Rightarrow 0) = 1$. Но тогда $\neg A = 0$, а значит $A = 1$.
То есть когда я разбираю доказательство общего вида, например, утверждение об иррациональности $\sqrt{2}$, проблем у меня нет.
И тогда я решил применить этот метод к частному типу высказываний, которые так часто приходится доказывать.

Приведу пример.
Утверждение.
Пусть $V$ - векторное пространство, $F$ - поле.
Тогда если $v \in V \wedge a \in F : av = 0 \Rightarrow a = 0 \vee v = 0$.
Докажем это утверждение от противного.
У меня есть $A = \{av = 0\}$.
Есть $B = \{a = 0 \wedge v = 0\}$.
Нужно доказать, что $A \Rightarrow B$.
Если я правильно понимаю, то я считаю $A$ уже нам данным, то есть $A = 1$.
Тогда предположим, что $A = 1 \wedge B = 0$. И все докажется.
Заскок у меня тут. Ведь в любом случае, всегда из истины ложь следовать не может. Значит тот факт что $A = 1 \Rightarrow B = 0$ ложен еще до попытки доказательства его не истинности?

[Connector]

Sdy в сообщении #1415249 писал(а):

Заскок у меня тут. Ведь в любом случае, всегда из истины ложь следовать не может. Значит тот факт что $A = 1 \Rightarrow B = 0$ ложен еще до попытки доказательства его не истинности?

А разве мы должны доказывать ложность утверждения $A = 1 \Rightarrow B = 0$ ? Мы построили противоречие к $A \Rightarrow B$; как Вы указали, оно выглядит так: $A=1 \wedge B=0$. Его ложность и следует доказать. (Действительно, при допущении $A = 1$, $B = 0$, импликация $A \Rightarrow B$ ложна, потому что из истины не может следовать ложь).

(Оффтоп)

Или я не понял, в чем именно заскок.

[epros]

Sdy в сообщении #1415249 писал(а):

когда я принимаю фактически за аксиомы способы работы с высказываниями посредством логических связок, тоже становятся аксиомами?

Что-то я не очень понял этой политической программы. "Способы работы с высказываниями посредством логических связок" - это и есть аксиомы исчисления высказываний что ли? Вот загляните в статью википедии Implicational propositional calculus, раздел Axiom system. Там указаны всего три схемы аксиом, которыми стандартно определяется классическая импликация (последней из трёх в конструктивной логике нет). Вот это и есть аксиоматический подход. До подстановки ноликов и единичек здесь пока далеко.

Sdy в сообщении #1415249 писал(а):

я хочу обосновать корректность применения метода доказательства от противного в случае, когда мое утверждение имеет вид импликации

Для какого-то специального случая метод доказательства от противного обосновывать не нужно, потому что в классической логике он обоснован для общего случая в виде $(\neg P \to \bot) \to P$ и ничто не мешает подставить вместо $P$ импликацию.

Sdy в сообщении #1415249 писал(а):

Есть $B = \{a = 0 \wedge v = 0\}$.

Может быть $B = \{a = 0 \vee v = 0\}$?

[Sdy]

Connector, спасибо за ответ.
Я вычитал, что, в той системе, где я нахожусь (с неба сыпятся таблицы истинности), я могу руководствоваться таким рассуждением:
1.$A \Rightarrow B \Leftrightarrow \neg A \vee B$.
При доказательстве от противного мы предполагаем, что верно утверждение, противоположное $\neg A \vee B$. Но это утверждение имеет вид $A \wedge \neg B$.
То есть мы как раз говорим, пусть $A$ верно, в то время как $B$ - нет.
Приходим к противоречию. Но тогда верно исходное высказывание. А оно эквивалентно верности импликации. И тогда (пока что по крайне мере) в моей голове это укладывается.

epros, спасибо за ответ.

epros в сообщении #1415349 писал(а):

Может быть $B = \{a = 0 \vee v = 0\}$?

Да, конечно, опечатался.

epros в сообщении #1415349 писал(а):

Там указаны всего три схемы аксиом, которыми стандартно определяется классическая импликация (последней из трёх в конструктивной логике нет)

А modus ponens не входит в это определение? Там это правило вывода идёт четвёртым пунктом. Как я понимаю, оно и позволяет мне из того что $P$ верно по условию, $P \Rightarrow Q$ верно по доказанному с помощью метода от противного, сделать вывода, что $Q$ - верно.

[arseniiv]

Правило вывода — не аксиома. (Хотя аксиомы наоборот можно понимать как частный случай правил вывода, у которых нет посылок.)

[epros]

Sdy в сообщении #1416788 писал(а):

Как я понимаю, оно и позволяет мне из того что $P$ верно по условию, $P \Rightarrow Q$ верно по доказанному с помощью метода от противного, сделать вывода, что $Q$ - верно.

arseniiv сказал, что modus ponens - правило вывода (по крайней мере, в Гильбертовской аксиоматизации). Я добавлю, что его применение - это ещё не метод от противного. Метод от противного, это применение классической тавтологии $(\neg P \to \bot) \to P$. "Классической" - это значит, что в некоторых других логиках, в частности, в конструктивной, это не тавтология, а поэтому метод от противного не применим.

[Sdy]

Хотел бы уточнить по литературе.
Так как с наскока преодолеть эти затруднения не получается.
То видимо стоит какое-то время уделить разбору математической логики выше уровня "падения с небес правил и таблиц истинности".
Можно ли за основу взять вот эту книгу (для изучения математической логики)?
R. Cori and D. Lascar, Mathematical Logic: A Course with Exercises (Part I) (Oxford University Press, 2001)
Она идёт как основная для курса логики в Оксфорде, но привлекает меня в ней скорее то, что там есть упражнения и решения к ним.
Учиться без решения задач не получается.
А в книге Верещагин Н.К., Шень А. Лекции по математической логике и теории алгоритмов, к сожалению, нет решений и обычно нет указаний. Конечно, что-то из нее есть уже решённое в интернете, но отсутствие решений в самой книге очень сильно затрудняет изучение материала.
Поэтому желательно, чтобы в литературе были упражнения и крайне хорошо, если там будут и решения к ним. Мне вообщем-то всё равно на каком языке читать книгу - на английском или русском.

[beroal]

Sdy в сообщении #1416874 писал(а):

R. Cori and D. Lascar, Mathematical Logic: A Course with Exercises (Part I) (Oxford University Press, 2001)

Для ваших целей она точно не годится. Там только теоретическая логика, ещё и с уклоном в теорию моделей. Здесь мой список литературы по практической логике и основам теории множеств. Дополнение к нему:

• George66. Теория категорий [Электронный ресурс] / George66. — Электрон. текстовые дан. — 2017. — 420 с. — Режим доступа: https://github.com/George66/Textbook/bl ... 8F%209.pdf, свободный.
  15 Исчисление высказываний.
• Hrbacek, Karel, and Thomas Jech. Introduction to Set Theory. 3rd ed., rev. and expanded. New York: Marcel Dekker, 1999. Print. Pure and Applied Mathematics 220.
• Верещагин Н. К. Лекции по математической логике и теории алгоритмов. Часть 1. Начала теории множеств / Николай Константинович Верещагин, Александр Шень. — 4-е изд., доп. — М.: МЦНМО, 2012. — 112 c.

[Sdy]

beroal, спасибо за ответ.
А что если взять её вкупе с одной из тех, которые есть в Вашем списке? Просто к теории моделей там вроде как подводится только в конце, по крайне мере такой вывод могу сделать по ее содержанию, а темы там затрагиваются как раз для меня актуальные, тот же propositional calculus, о котором говорил epros, идёт как первая рассматриваемая тема.
Потому что меня интересует не только такие вещи, как методы доказательства и их корректность, но и вещи, касающиеся индукции, порядка, равенства. Всего, незнание о чем у меня выскочило при попытке понять, откуда всё это берется умолчательно в книгах по анализу, по которым я этот самый анализ изучаю. Просто я задаю вопросы, Вы отвечаете, отвечают в других темах и arseniiv,epros, mihaild, george66,Someone, но я банально не имею представления о тех терминах (те же языки разного порядка, перевод между ними), в которых они отвечают, а поверхностное знакомство с ними по ресурсам типа Википедии разобраться помогает несильно. Хотелось бы говорить об этом на одном языке. (Тирада была к тому, зачем мне это всё нужно).

[beroal]

Sdy в сообщении #1417382 писал(а):

А что если взять её вкупе с одной из тех, которые есть в Вашем списке?

Не стоит. Читая её, вы выучите много того, что вам не нужно на данном этапе. Например, логика с кванторами вводится только в главе 3 со страницы 112, а правила вывода только в главе 4 со страницы 193. Вам это нужно с самого начала.

Sdy в сообщении #1417382 писал(а):

вещи, касающиеся индукции, порядка, равенства

Индукция для натуральных чисел и равенство излагаются в теории множеств. Разные виды порядков в теории множеств или теории порядков. Учебников именно по теории порядков мало, я знаю ровно один. Так что эту тему пихают или в логику, или в теорию множеств. Если вам нужен элементарный материал, который обычно изучают после логики, то он есть в учебниках по дискретной математике. Ниже я привёл пару книг, но искать сейчас нет времени.
Velleman, Daniel J. How to Prove It: A Structured Approach. 2nd ed. Cambridge: Cambridge UP, 2006. Print.
Rosen, Kenneth H. Discrete Mathematics and Its Applications. 8th ed. New York: McGraw-Hill, 2019. Print.
Davey, B. A., and Priestley H. A. Introduction to Lattices and Order. 2nd ed. Cambridge: Cambridge UP, 2002. Print.

[epros]

beroal в сообщении #1417397 писал(а):

Например, логика с кванторами вводится только в главе 3 со страницы 112, а правила вывода только в главе 4 со страницы 193. Вам это нужно с самого начала.

А я бы посоветовал всем начинать изучение логики именно с пропозициональной. Почему вообще возникает необходимость в кванторах - до этого вопроса ещё нужно правильно созреть. А многие учебники вообще начинают с семантики, подразумевающей двузначность логики. По-моему, это методически неверно, начинать нужно с понятий о языке, аксиомах и логическом выводе. Теория множеств - тоже частая и неудачная, как я полагаю, точка старта.

[beroal]

epros в сообщении #1417512 писал(а):

А я бы посоветовал всем начинать изучение логики именно с пропозициональной. Почему вообще возникает необходимость в кванторах - до этого вопроса ещё нужно правильно созреть.

Мне кажется, не стоит затягивать. Любое мало-мальски интересное математическое утверждение требует кванторов. Коммутативность сложения натуральных чисел:

$$\forall n\forall m(n+m=m+n).$$

Конечно, можно спрятать кванторы всеобщности, как это обычно делают. Тогда стандартный порядок натуральных чисел:

$$n\leq m := \exists d(m = d+n).$$

Тут уже не спрячешь. А что можно высказать с помощью логики высказываний? «Если солнце светит, то мы идём на пляж». По-моему, это максимум.

[epros]

beroal в сообщении #1417514 писал(а):

Любое мало-мальски интересное математическое утверждение требует кванторов.
...
А что можно высказать с помощью логики высказываний?

Это да, логика высказываний недостаточно богата. Но не потому, что в ней нет кванторов, а потому, что она имеет дело с грамматически законченными высказываниями, которым неоткуда взяться, если нет отдельных частей речи. Т.е. понятия об объектах, свойствах и отношениях в ней отсутствуют.

А кванторы - это всего лишь расширение понятий конъюнкции и дизъюнкции, каковые в логике высказываний есть.

Но важно то, что ключевое понятие - о логическом выводе - происходит из логики высказываний. И уже там полно нюансов его определения. Если, не осознав их, попытаться сразу перескочить на исчисление предикатов, ничего хорошего не выйдет.

[arseniiv]

epros в сообщении #1417512 писал(а):

А многие учебники вообще начинают с семантики, подразумевающей двузначность логики. По-моему, это методически неверно, начинать нужно с понятий о языке, аксиомах и логическом выводе.

Можно ещё начинать с интерпретации БГК, хоть и неформальной, но ей самое место как раз будет. Доказательства простых тавтологий и общезначимых формул с кванторами превращает в конфетку.

[beroal]

arseniiv в сообщении #1417567 писал(а):

Можно ещё начинать с интерпретации БГК, хоть и неформальной, но ей самое место как раз будет. Доказательства простых тавтологий и общезначимых формул с кванторами превращает в конфетку.

Вы не найдёте литературы, обучающей логике на основе теории типов, или учебников по математике, которые опираются на теорию типов, а не на теорию множеств. И ученик так же, как в этой теме, будет блуждать в потёмках. А так да, теория типов хороша, как чужая жена.