Главное меню
Мы солидарны с Украиной. Узнайте здесь, как можно поддержать Украину.

Логика

Автор RawonaM, марта 10, 2011, 21:43

0 Пользователи и 1 гость просматривают эту тему.

arseniiv

Должно быть [tex]\vDash \alpha \Leftrightarrow \forall \Sigma : \Sigma \vDash \alpha[/tex], вроде бы. Из этого ваше докажется двумя подстановками вместо сигмы.

RawonaM

Цитата: arseniiv от апреля  4, 2011, 19:55
Из этого ваше докажется двумя подстановками вместо сигмы.
Не понял.

RawonaM

Вот еще интересная штука:
По индукции определено множество I высказываний, в которых есть только импликация и атом p.
Нужно доказать, что I линейно предупорядоченное.

Я думаю, что тут для начала нужно по структурной индукции показать, что [tex]\alpha \in I[/tex] может быть F только в той модели, где p=F.
Ибо каждое высказывание в форме [tex]a \rightarrow b[/tex] в итоге сводится к p и b может быть F только если p=F. В общем, рекурсия. Как это правильно сформулировать, не знаю.

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

Gerbarius

Цитата: RawonaM от апреля  4, 2011, 19:19
Цитата: Gerbarius от апреля  3, 2011, 01:54
если для любых [tex] a [/tex] и [tex] b [/tex] при условии [tex] \Sigma_1 \vDash a[/tex] и [tex]\Sigma_2 \vDash b [/tex] следует выполнимость формулы [tex] a \land b [/tex], то формулы множества [tex]\Sigma_1 \cup \Sigma_2[/tex] совместно выполнимы
А в обратную сторону это же тоже верно, правильно? Вроде как тривиально.
Да, верно. Если [tex] \Sigma_1 \vDash a [/tex] и [tex] \Sigma_2 \vDash b [/tex], то чтобы выполнить формулу [tex] a \land b [/tex], достаточно тем атомам из неё, которые встречаются в формулах из [tex] \Sigma_1 \cup \Sigma_2 [/tex] приписать те значения, которые выполняют [tex] \Sigma_1 \cup \Sigma_2 [/tex], а остальным атомам можно приписать произвольные значения.

Цитата: RawonaM от апреля  4, 2011, 19:19
Вот такой еще вопрос:
эквивалентны ли два утверждения
1) [tex]\alpha[/tex] тавтология
2) для любых [tex]\gamma, \beta[/tex] верно следующее: [tex]\{\gamma\} \vDash \beta \Leftrightarrow \{\gamma, \alpha\} \vDash \beta[/tex]

Мне кажется что да, но я не уверен почему-то. Вроде как доказал :)
Да. А если доказали, то откуда неуверенность?  :)
На самом деле здесь условие [tex]\{\gamma\} \vDash \beta \Leftrightarrow \{\gamma, \alpha\} \vDash \beta[/tex] можно заменить на [tex]\{\gamma, \alpha\} \vDash \beta \rightarrow \{\gamma\} \vDash \beta[/tex], так как [tex]\{\gamma\} \vDash \beta \rightarrow \{\gamma, \alpha\} \vDash \beta[/tex] выполняется всегда.

RawonaM

Цитата: Gerbarius от апреля  4, 2011, 20:29
Да. А если доказали, то откуда неуверенность?  :)
Из-за другой логики, точнее из теории вероятности :) Есть задание «доказать или опровернгуть», в нем два пункта. Если оба пункта нужно доказывать или оба пункта нужно опровергать, то всегда есть подозрение, что закралась ошибка. Ну что же, выходит, что в этот раз оба пункта были верны :)

arseniiv

Offtop
Цитата: RawonaM от апреля  4, 2011, 20:02
Не понял.
Что-то я и сам запутался. Подставить можно всё, а вот следует ли из этого что-нибудь...

Gerbarius

Цитата: RawonaM от апреля  4, 2011, 20:14
Вот еще интересная штука:
По индукции определено множество I высказываний, в которых есть только импликация и атом p.
Нужно доказать, что I линейно предупорядоченное.

Я думаю, что тут для начала нужно по структурной индукции показать, что [tex]\alpha \in I[/tex] может быть F только в той модели, где p=F.
Ибо каждое высказывание в форме [tex]a \rightarrow b[/tex] в итоге сводится к p и b может быть F только если p=F. В общем, рекурсия. Как это правильно сформулировать, не знаю.

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

Здесь потенциально возможны четыре распределения истинностных значений для каждой формулы. И если бы нашлись две формулы, одна из которых принимает значение T при p=T и F при p=F, а другая в точности противоположные значения, то ни одна из них не следовала бы из другой. То есть фактически нужно показать, что таких двух формул нет (остальные случаи "линейности" не мешают).
На самом деле любая формула в I является либо тавтологией, либо эквивалентна p, то есть принимает T при p=T и F при p=F. Это как раз легко доказывается структурной индукцией (или натуральной по "глубине" построения формулы). Можно, кстати, доказывать и то свойство, которое вы предложили, оно тоже подойдёт.
Чтобы структурной индукцией доказать, что все формулы из I обладают нужным свойством, нужно лишь показать, что p обладает этим свойством, и что [tex] \alpha \rightarrow \beta [/tex] обладает нужным свойством, коль скоро им обладают как [tex] \alpha [/tex], так и [tex] \beta [/tex]. А больше ничего и не требуется.

RawonaM

Благодарю за помощь!
Запечатал задание, почти неделю над ним сидел.
Таки курс не из простых.

Теперь надо за до конца недели сделать теорвер и дискретку, потом браться за следующее задание по логике...

RawonaM

Бесит нелогичная логика. :(

Вот смотрите: на форуме курса сказали, что [tex]\nvDash \beta[/tex] означает "нет такой модели, которая выполняет бету", а [tex]\alpha \nvDash \beta[/tex] означает «есть такая модель, которая выполняет альфу и не выполняет бету». Нелогично, по-моему.


RawonaM


RawonaM

Цитата: RawonaM от апреля 15, 2011, 20:13
на форуме курса сказали, что [tex]\nvDash \beta[/tex] означает "нет такой модели, которая выполняет бету"
Не ну это ваще беспредел...
В другом месте на форуме сказали, что это означает, что «не все модели выполняют бету»...
Что более логично, но ведь путаница страшная, иди знай, что имелось в виду.

arseniiv

Цитата: RawonaM от апреля 15, 2011, 21:33
В другом месте на форуме сказали, что это означает, что «не все модели выполняют бету»...
Скорее всего, именно это (у нас была алгебра высказываний, но алгебры предикатов не было, хотя было исчисление предикатов, как и высказываний). А для первого употребления надо писать тогда [tex]\vDash \neg \beta[/tex].

RawonaM

Цитата: arseniiv от апреля 15, 2011, 21:43
Скорее всего, именно это
Мне тоже так кажется. Тем более, что задание тут получается неправильное, если с тем вариантом.

RawonaM

Вроде контрадикцию как-то по другому обозначают.

RawonaM

Мне нужно доказать, что система выводов, включаяющая две аксиомы из системы Гильберта и единственное правило вывода Modus Ponens обладает свойством дедукции.
Мне кажется я доказал это с помощью только одной аксиомы, поэтому терзают сомнения.

Также спрашивается, если добавить к MP еще какое-то правило, то изменится ли свойство. Вот это я не врубаюсь. Система должна быть sound. Вроде кажется, что ничего не изменится, но вопрос подозрителен.

Gerbarius

Цитата: RawonaM от апреля 19, 2011, 14:51
включаяющая две аксиомы из системы Гильберта
Какие именно?
Эти что ли?
[tex] A \rightarrow (B \rightarrow A) [/tex]
[tex] (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) [/tex]
Или другие какие-то?
Цитата: RawonaM от апреля 19, 2011, 14:51
обладает свойством дедукции
Под этим имеется в виду справедливость дедукционной теоремы?
То есть, что из [tex]\Gamma, A \vdash B [/tex] следует [tex] \Gamma \vdash A \rightarrow B [/tex]?

RawonaM

Цитата: Gerbarius от апреля 19, 2011, 16:23
Цитироватьвключаяющая две аксиомы из системы Гильберта
Какие именно?
Эти что ли?
[tex] A \rightarrow (B \rightarrow A) [/tex]
[tex] (A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C)) [/tex]
Или другие какие-то?
Да, эти.

Цитата: Gerbarius от апреля 19, 2011, 16:23
Цитироватьобладает свойством дедукции
Под этим имеется в виду справедливость дедукционной теоремы?
То есть, что из [tex]\Gamma, A \vdash B [/tex] следует [tex] \Gamma \vdash A \rightarrow B [/tex]?
Точнее, что это следует в обе стороны.

Я уже пересмотрел и нашел у себя ошибку. Смотрю в доказательство дедукционной теоремы, что-то оно слишком длинное, вряд ли имеется в виду, что мне нужно его просто переписать. В общем-то, в одну сторону я доказал в пару строчек ([tex] \Gamma \vdash A \rightarrow B [/tex]  следует [tex]\Gamma, A \vdash B [/tex]).

Вторую сторону затрудняюсь. Написано примечание, что для начала рекомендуется доказать [tex]\vdash A \rightarrow A [/tex]. Доказал, но не пойму куда его притулять.

То есть, я догадываюсь, что из этих трех аксиом и В мне нужно написать доказательство [tex] \Gamma \vdash A \rightarrow B [/tex]. Однако не затрудняюсь и не вижу просвета.

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

Gerbarius

Тут нужно рассмотреть все случаи, как может быть получен вывод [tex] \Gamma, A \vdash B [/tex].
Их всего три.
1) [tex] B [/tex] входит в [tex] \Gamma [/tex] или [tex] B [/tex] - аксиома. Тогда по определению [tex] \Gamma \vdash B [/tex]. Отсюда и из [tex] \Gamma \vdash B \rightarrow (A \rightarrow B) [/tex]  получаем [tex] \Gamma \vdash A \rightarrow B [/tex].
2) [tex] B [/tex] - это [tex] A [/tex]. В этом случае как раз и нужно [tex] \vdash A \rightarrow A [/tex], а точнее,
что [tex] \Gamma \vdash A \rightarrow A [/tex], что впрочем следует из первого.
Этот случай к предыдущему, если что, не сводится, так как [tex] A [/tex] может не быть аксиомой и может
не входить в [tex] \Gamma [/tex], а потому [tex] \Gamma \vdash B [/tex] может быть неверно (а именно на этом основаны рассуждения в предыдущем случае).
3) [tex] \Gamma, A \vdash B [/tex] получено по правилу modus ponens из [tex] \Gamma, A \vdash P \rightarrow B [/tex] и [tex] \Gamma, A \vdash P [/tex]. Допускаем, что мы можем построить выводы [tex] \Gamma \vdash A \rightarrow (P \rightarrow B) [/tex] и [tex] \Gamma \vdash A \rightarrow P [/tex]. Тогда вывод [tex] \Gamma \vdash A \rightarrow B [/tex] строится при помощи этих выводов и аксиомы [tex] (A \rightarrow (P \rightarrow B)) \rightarrow ((A \rightarrow P) \rightarrow (A \rightarrow B)) [/tex].
Отсюда дедукционная теорема следует в силу обычной математической индукции по длине вывода (или в силу дедуктивной индукции, если она вам знакома).
Можно привести  и вполне конкретный алгоритм построения нужного вывода. [tex] \Gamma, A \vdash B [/tex] означает, что у нас есть вполне конкретный вывод, который можно, например, представить в виде дерева (в данном случае бинарного). В узлах дерева мы записываем утверждения вида [tex] \Gamma, A \vdash C [/tex]. Утверждения во внутренних узлах получаются из утверждений в дочерних узлах по правилу modes ponens, а утверждения в конечных узлах получаются как в случаях 1 и 2. Затем мы просто последовательно преобразуем это дерево в другое, где  поддеревья с корневым узлом [tex] \Gamma, A \vdash C [/tex] преобразуются в поддеревья с корневым узлом [tex] \Gamma \vdash A \rightarrow C [/tex]. Сначала преобразуются поддеревья, состоящие из конечных узлов, по алгоритму, рассмотренному в случаях 1 и 2, а затем и все остальные, для которых уже преобразованы оба дочерних поддерева, по алгоритму, описанному в случае 3, пока не будет преобразовано всё дерево.

Цитата: RawonaM от апреля 19, 2011, 14:51
Также спрашивается, если добавить к MP еще какое-то правило, то изменится ли свойство. Вот это я не врубаюсь. Система должна быть sound. Вроде кажется, что ничего не изменится, но вопрос подозрителен.
Аксиомы можно добавлять какие угодно. То рассуждение, которое я привёл выше, не изменится никак. Но если добавить новое правило вывода, то появляется ещё один случай, который нужно рассматривать отдельно. В этом случае справедливость дедукционной теоремы может быть нарушена. Например, если добавить правило подстановки, что из [tex] \Gamma \vdash P [/tex] можно вывести [tex] \Gamma \vdash P^* [/tex], где [tex] P^* [/tex] получено из [tex] P [/tex] подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в [tex] P [/tex]), то дедукционая теорема уже не будет верна. Например, из [tex] p \vdash p [/tex] подстановкой можно получить [tex] p \vdash q [/tex], но [tex] \vdash p \rightarrow q [/tex] получить нельзя. Хотя дедукционная теорема может и в таких случаях всё же оказаться справедливой, если наложить соответствующие ограничения на выводы, с которыми мы имеем дело.

RawonaM

Цитата: Gerbarius от апреля 19, 2011, 19:34
Отсюда дедукционная теорема следует в силу обычной математической индукции по длине вывода
У вас получилось так компактно это написать...
Наши почему-то всегда пишут доказательство по индукции в полной форме, т.е. базис индукции (доказательтво в одну строку) и шаг индукции (доказательтво в n строк), хотя по сути они в основном повторяют друг друга.

Спасибо, вроде теперь стало понятно, а то я совсем не в ту сторону копал.

RawonaM

Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы [tex] \Gamma \vdash A \rightarrow (P \rightarrow B) [/tex] и [tex] \Gamma \vdash A \rightarrow P [/tex].
Как же вы это можете допустить? Вы же это доказываете...
Или я чего-то недопонял.

Gerbarius

Цитата: RawonaM от апреля 21, 2011, 21:33
Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы [tex] \Gamma \vdash A \rightarrow (P \rightarrow B) [/tex] и [tex] \Gamma \vdash A \rightarrow P [/tex].
Как же вы это можете допустить? Вы же это доказываете...
Или я чего-то недопонял.
Доказывается-то всё индукцией, а это фактически индуктивное предположение, которое используется при обосновании шага индукции. Правда, в случае обычной математической индукции всё выглядит несколько сложнее по форме. То есть в этом случае нужно сначала явно рассмотреть базис индукции, который включает в себя случаи 1 и 2 (только они возможны для выводов длины 1), а затем, допустив, что дедукционная теорема справедлива для всех выводов длины [tex] \le n [/tex], показать что она справедлива и для выводов длины [tex] n + 1 [/tex] (шаг индукции). Обоснование шага индукции включает в себя повторное рассмотрение случаев 1 и 2 и случай 3. При рассмотрении случая 3 длина каждого из выводов [tex] \Gamma, A \vdash P \rightarrow B [/tex] и [tex] \Gamma, A \vdash P [/tex] будет меньше длины рассматриваемого вывода [tex] \Gamma, A \vdash B [/tex], а значит, к ним применимо индуктивное предположение. То есть фразу
Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы [tex] \Gamma \vdash A \rightarrow (P \rightarrow B) [/tex] и [tex] \Gamma \vdash A \rightarrow P [/tex].
нужно понимать в том смысле, что эти выводы можно построить в силу индуктивного предположения.

Но в случае дедуктивной индукции всё несколько проще, хотя и не принципиально. Попробую рассказать про неё. Допустим, у нас есть класс высказываний, (в нашем случае это выражения вида [tex] \Gamma \vdash A [/tex]), и из них выделен класс "теорем" следующим образом:
1) Выделен класс "аксиом", то есть высказываний, которые "автоматически" считаются теоремами. В нашем случае это выражения вида [tex] \Gamma \vdash A [/tex], где [tex] A [/tex] либо входит в [tex] \Gamma [/tex], либо является аксиомой в рассматриваемой нами системе гильбертовского типа.
2) Выделен ряд правил вывода, каждое из которых из заданного числа посылок-"теорем" строит заключение-"теорему". В нашем случае есть единственное правило [tex] \frac{\Gamma \vdash A, \Gamma \vdash A \rightarrow B}{\Gamma \vdash B} [/tex].
3) "Теоремы" - это те и только те высказывания, которые могут быть "выведены" из "аксиом" при помощи конечного числа применений правил вывода.
Тогда, чтобы доказать, что некоторое свойство справделиво для всех "теорем", достаточно доказать, что
оно справедливо для всех "аксиом", и что для всякого правила вывода его заключение обладает этим свойством, коль скоро им обладают его посылки. В этом и состоит принцип дедуктивной индукции.
В нашем случае применение дедуктивной индукции просто сводится к рассмотрению случаев 1, 2, 3 буквально в том виде, как я написал. В этом случае
Цитата: Gerbarius от апреля 19, 2011, 19:34
Допускаем, что мы можем построить выводы [tex] \Gamma \vdash A \rightarrow (P \rightarrow B) [/tex] и [tex] \Gamma \vdash A \rightarrow P [/tex].
это просто (индуктивное) предположение, что доказываемое свойство справедливо для посылок применения правила modus ponens.

RawonaM

Цитата: Gerbarius от апреля 19, 2011, 19:34
Например, если добавить правило подстановки, что из [tex] \Gamma \vdash P [/tex] можно вывести [tex] \Gamma \vdash P^* [/tex], где [tex] P^* [/tex] получено из [tex] P [/tex] подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в [tex] P [/tex]), то дедукционая теорема уже не будет верна. Например, из [tex] p \vdash p [/tex] подстановкой можно получить [tex] p \vdash q [/tex], но [tex] \vdash p \rightarrow q [/tex] получить нельзя.
P* ведь должен следовать логически из P, да? Иначе же система не будет sound.
Например [tex]P|(P \lor P)[/tex] вроде сойдет.

А точно из этого нельзя получить [tex]\vdash P \rightarrow (P \lor P)[/tex]?
Это же тавтология...

Gerbarius

Цитата: RawonaM от апреля 22, 2011, 09:27
Цитата: Gerbarius от апреля 19, 2011, 19:34
Например, если добавить правило подстановки, что из [tex] \Gamma \vdash P [/tex] можно вывести [tex] \Gamma \vdash P^* [/tex], где [tex] P^* [/tex] получено из [tex] P [/tex] подстановкой некоторой формулы вместо некоторого атома (во всех вхождениях этого атома в [tex] P [/tex]), то дедукционая теорема уже не будет верна. Например, из [tex] p \vdash p [/tex] подстановкой можно получить [tex] p \vdash q [/tex], но [tex] \vdash p \rightarrow q [/tex] получить нельзя.
P* ведь должен следовать логически из P, да? Иначе же система не будет sound.
Например [tex]P|(P \lor P)[/tex] вроде сойдет.

А точно из этого нельзя получить [tex]\vdash P \rightarrow (P \lor P)[/tex]?
Это же тавтология...

Я забыл добавить, что мой контрпример относится к обычному классическому исчислению высказываний, но надеюсь, это не вызвало недоразумений.
[tex] P^* [/tex] не обязано ни из чего следовать. Оно просто получается из [tex] P [/tex] некоторым формальным преобразованием. Нас ведь спрашивают, что будет, если добавить ещё одно правило, но в выборе этого правила нас никто не ограничивает, а потому для построения контрпримера можно взять любое удобное правило. Опять-таки для контрпримера достаточно указать ровно один случай, когда дедукционная теорема не выполняется. Конечно, [tex] \vdash p \rightarrow (p \lor p) [/tex] можно получить, но [tex] \vdash p \rightarrow q [/tex] уже нет, и одного этого только достаточно, чтобы заключить, что дедукционая теорема при добавлении к классическому исчислению высказываний правила подстановки справедлива не будет. Замечу, кстати, что под невыводимостью  [tex] \vdash p \rightarrow q [/tex], конечно, имеется в виду невыводимость в системе, к которой добавлено правило подстановки. Строго говоря, это не совсем очевидно, но можно показать, что в классическом исчислении высказываний с единственным правилом modus ponens, из [tex] \vdash P [/tex] следует [tex] \vdash P^* [/tex], а потому добавление правила подстановки не увеличивает множество доказуемых формул. Тогда  [tex] \vdash p \rightarrow q [/tex] невыводимо (даже с правилом подстановки) просто потому, что это не тавтология.

RawonaM

В задании требуется чтобы система была sound, т.е. чтобы все, что можно вывести, следовало логически.

Gerbarius

Цитата: RawonaM от апреля 22, 2011, 17:14
В задании требуется чтобы система была sound, т.е. чтобы все, что можно вывести, следовало логически.
Сначала нужно понять, что именно под этим подразумевается. Вы, видимо, это условие понимаете в том смысле, что и после добавления нового правила [tex] \Gamma \vdash A [/tex] должно выводиться только в том случае, если [tex] A [/tex] логически следует из [tex] \Gamma [/tex]. Но мне почему-то кажется, что здесь требуется всего лишь, чтобы в рассматриваемой системе гильбертовского типа после добавления нового правила [tex] \vdash A [/tex] выводилось только тогда, когда [tex] A [/tex] тавтология, но никаких особых ограничений на выводы типа [tex] \Gamma \vdash A [/tex] нет. Но вам это лучше уточнить.

Быстрый ответ

Обратите внимание: данное сообщение не будет отображаться, пока модератор не одобрит его.

Имя:
Имейл:
Проверка:
Оставьте это поле пустым:
Наберите символы, которые изображены на картинке
Прослушать / Запросить другое изображение

Наберите символы, которые изображены на картинке:

√36:
ALT+S — отправить
ALT+P — предварительный просмотр