Мат. логика: импликация

[Nurzery[Rhymes]]

Хочу получше разобраться в матлогике и использовать ее как инструмент для выведения новых утверждений и определения их истинности. Иначе зачем она нужна?

Из определения импликации следует, что:
1) Импликация с ложной посылкой всегда истинна
2) Импликация с истинным заключением всегда истинна
3) Импликация ложна тогда и только тогда, когда из истинной посылки вытекает ложное заключение.

Я решил, что изучать логику будет полезнее на примере каких-нибудь теорем. Вот например:
Теорема. Если часть системы векторов линейно зависима, то вся система векторов линейно зависима.
Утверждения:
$a$: Часть системы векторов линейно зависима.
$b$: Вся система векторов линейно зависима.
Теорема имеет вид: $a \to b$

Рассмотрим все истинные импликации:
1) $0\to 0$: Если неверно, что часть системы векторов линейно зависима, то вся система векторов линейно независима. Ошибка. Дополним базис векторного пространства лишним вектором и получим опровержение.

2) $0 \to 1$: Если неверно, что часть системы векторов линейно зависима, то вся система линейно зависима. Может быть да, а может быть нет. Ничего однозначного сказать нельзя. Тем не менее правила логики вынуждают нас считать это утверждение однозначно истинным.

3) $1 \to 1$: Очевидный случай. Истинность теоремы совпала с истинностью импликации.

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

[ИСН]

Логика не нужна.

[Nurzery[Rhymes]]

ИСН в сообщении #981737 писал(а):

Логика не нужна.

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

[Mitrius_Math]

Nurzery[Rhymes], посмотрите книжки Игошина - Математическая логика и теория алгоритмов, Задачи по математической логике и теории алгоритмов. Очень рекомендую.

[Nurzery[Rhymes]]

Mitrius_Math в сообщении #981743 писал(а):

Nurzery[Rhymes], посмотрите книжки Игошина - Математическая логика и теория алгоритмов, Задачи по математической логике и теории алгоритмов. Очень рекомендую.

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

[svv]

Вы приписываете импликации некую разумность, которая позволяет ей знать о том, какие комбинации значений истинности $a$ и $b$ вообще могут встречаться, а какие нет. Но импликация знает не больше того, что в неё заложено: что $a$ и не-$b$ вместе — ложь.

Откажитесь от идеи «что-то из чего-то следует». Импликация всего лишь заявляет: когда $a$, то и $b$. Никакая логическая взаимосвязь между $a$ и $b$ здесь не постулируется. Что может опровергнуть это заявление? Только ситуация «$a$ и не-$b$».

При этом импликации неизвестно, совместимы ли остальные комбинации. Допустим, реально не-$a$ и $b$ тоже не могут встречаться, а импликация $a\to b$ всё равно истинна. Почему? Её подход:
Я не знаю, возможны или нет не-$a$ и $b$ одновременно, но если такое случится, это не нарушит моё утверждение «когда $a$, то и $b$».

Nurzery[Rhymes] в сообщении #981732 писал(а):

1) $0\to 0$: Если неверно, что часть системы векторов линейно зависима, то вся система векторов линейно независима. Ошибка. Дополним базис векторного пространства лишним вектором и получим опровержение.

Импликация не об этом. Она говорит: если и часть, и вся система независимы, то утверждение «когда часть зависима, то вся система зависима» не лжет.

Между прочим, добавляя один вектор, Вы меняете содержание термина «вся система» по ходу рассуждения.

[Expresss]

ИСН в сообщении #981737 писал(а):

Логика не нужна.

(Оффтоп)

Цитируете моего деда!

[provincialka]

Вы просто не умеете их готовить правильно употреблять. Начнем с того, что это по сути не высказывания, а предикаты. Они верны не сами по себе, а по отношению к некоторым "системам векторов". Если вы хотите убрать свободные переменные, нужно навесить кванторы. А еще четко связать переменные первого и второго высказывания.
Правильная формальная запись теоремы будет выглядеть совсем не так.

[ex-math]

Теорема утверждает, что импликация истинна, то есть не может быть ложного $b $ при истинном $a $. Она не утверждает, что обязаны реализоваться все варианты истинностных значений $a $ и $b $, при которых импликация истинна.

-- 23.02.2015, 23:22 --

Может проще будет для начала рассмотреть такую теорему: если натуральное число делится на четыре, то оно четно.

[gefest_md]

Nurzery[Rhymes] в сообщении #981732 писал(а):

1) . . . : Если неверно, что часть системы векторов линейно зависима, то вся система векторов линейно независима. Ошибка. Дополним базис векторного пространства лишним вектором и получим опровержение.

$\neg a\to\neg b$
Отрицание $b$ построено правильно?

[Nurzery[Rhymes]]

Цитата:

Может проще будет для начала рассмотреть такую теорему: если натуральное число делится на четыре, то оно четно.

Я уже читал некоторые книги. Учебник Никольской, например, и видел там абсурдные высказывания, которые тем не менее истинны. Похоже, я просто возлагал на импликацию то, чего она не умеет.

-- 24.02.2015, 00:28 --

gefest_md в сообщении #981760 писал(а):

Nurzery[Rhymes] в сообщении #981732 писал(а):

1) . . . : Если неверно, что часть системы векторов линейно зависима, то вся система векторов линейно независима. Ошибка. Дополним базис векторного пространства лишним вектором и получим опровержение.

$\neg a\to\neg b$
Отрицание $b$ построено правильно?

Вроде да. Вместо "Неверно, что система линейно зависима" написал, что она линейно независима, потому что высказывание с обилием "неверно, что" сознание отказывается быстро распарсить.

[arseniiv]

Короче, как тут уже сказали, запись вашей теоремы будет совсем не $a\to b$, ибо $a, b$ обе содержат свободную переменную (систему векторов, а они разные бывают). Вот если записать такое:

$$\begin{aligned} a &= \text{часть }s\text{ линейно зависима}, \\ b &= s\text{ линейно зависима}, \\ u &= s\text{ — система векторов}, \end{aligned}$$

то $\forall s.\; u\to(a \to b)$ будет правильным (если правильно формализовать $a,b,u$). И для получения интерпретации вы просто так приписывать истинностные значения $a,b,u$ не можете. Если бы они были нульместными предикатами — да, можно выбрать 0 или 1. Но это не так, и надо задать по значению для каждой возможной системы — и вот тут может появиться зависимость, т. к. не любая интерпретация нас удовлетворит, а удовлетворят только некоторые, в которых определённые формулы истинны. В данном случае это такие формулы, из которых выводятся важные нам свойства систем векторов. Если их выкинуть, то и претензии на бессмысленность некоторых интерпретаций, в которых $\forall s.\; u\to(a \to b)$ ложна, тоже надо выкинуть.

P. S. $u$ можно убрать и писать $\forall s.\; a \to b$, если объектами теории являются только системы векторов.

[grizzly]

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

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

Я хотел бы уточнить один момент в мат.логике. Речь идёт об оценочных суждениях. Например, вот эти "важные нам свойства". Могут ли они быть определены чисто синтаксически (желательно -- для чистоты эксперимента -- машинным выводом)? Если да, то всегда ли это осуществимо конечным образом?

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

[arseniiv]

grizzly в сообщении #981885 писал(а):

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

В матлогике под интерпретацией понимается алгебраическая система, в которой есть по операции на каждый функциональный символ и отношению на каждый предикатный, вместе с отображением, какой куда. Это отображение порождает отображение из замкнутых (т. е. в которых нет свободных переменных) формул в значения истинности. Интерпретаций может, конечно, быть много. Если в какой-то интерпретации множество формул $\mathcal F$ одновременно истинны, её называют моделью $\mathcal F$. Моделей у одного и того же $\mathcal F$ тоже может быть много.

grizzly в сообщении #981885 писал(а):

Например, вот эти "важные нам свойства". Могут ли они быть определены чисто синтаксически (желательно -- для чистоты эксперимента -- машинным выводом)? Если да, то всегда ли это осуществимо конечным образом?

Тут я немного перестарался в словах, наверно. Если мы рассматриваем какую-нибудь систему вывода $A$ и не принимаем $F\equiv\forall s.\; u\to(a \to b)$ за аксиому (вполне естественно в контексте), то не любая модель $F$ будет моделью всех теорем $A$; именно потому что среди теорем много чего ещё неупомянутого. В $A$ есть какие-то аксиомы, гарантирующие те теоремы, которые отрезают «неправильные» модели $F$. В данном случае это (такая $A$, которая нам нравится) возможно, но может быть по-всякому, тут я особо не разбираюсь.

Вообще же я не имел в виду никакого вывода, а только то, что нечего удивляться, что у множества формул может быть меньше моделей, чем у его подмножества (в данном случае из одной $F$), и не важно, откуда то множество взялось — навыводилось из аксиом или примерещилось со сна.

Кстати о примерещившемся:

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

Если их выкинуть, то и претензии на бессмысленность некоторых интерпретаций, в которых $\forall s.\; u\to(a \to b)$ ложна, тоже надо выкинуть.

Это написано неправильно. Надо было так:
«Если их выкинуть, то и претензии на бессмысленность некоторых интерпретаций, в которых $\forall s.\; u\to(a \to b)$ истинна, но (скажем) $\forall s.\;u\to(\neg a\wedge b)$ тоже истинна, тоже надо выкинуть.» Теперь это что-то более осмысленное.

-- Вт фев 24, 2015 21:06:23 --

(Оффтоп)

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

[grizzly]

arseniiv
Спасибо за разъяснения -- я смог увидеть у себя большие проблемы в понимании взаимоотношений синтаксиса, семантики и оценочных суждений. Зато теперь я смогу над этим поработать.