Лингвофорум

Цитата: RawonaM от мая 23, 2011, 16:36
Не понимаю, когда можно использовать универсальное обобщение?

Например дано .
По какой причине нельзя построить доказательство:

?

То есть вы хотите из сначала вывести , а затем из вывести ?  Но, вообще говоря, из никакое не выводится.

Цитата: Gerbarius от мая 24, 2011, 12:43
То есть вы хотите из сначала вывести , а затем из вывести ? 

Именно. Что мне мешает?

Цитата: Gerbarius от мая 24, 2011, 12:43
Но, вообще говоря, из никакое не выводится.

Почему это? Если есть такой х, то мы можем его взять и будет Р(с) (с — тот самый х который есть).
Забыл как это называется. instantiation, что ли. Что я тут напутал?

Вот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/exist_inst.html

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/univ_gen.html

Цитата: RawonaM от мая 24, 2011, 12:57
http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/exist_inst.html

http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/inference/univ_gen.html

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

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

Цитата: RawonaM от мая 24, 2011, 12:53
Вот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms

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

Цитата: Gerbarius от мая 24, 2011, 15:42

ЦитироватьВот, Q7 тут меня смущает:
(wiki/en) Hilbert-style_deductive_system#Logical_axioms

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

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

Цитата: Gerbarius от мая 24, 2011, 15:42
Но это не совсем традиционный подход. В более традиционных логических системах используются только переменные, обозначающие произвольные элементы.

У нас обозначают буквами a,b,c конкретные элементы, а x,y,z — переменные.

Цитата: Gerbarius от мая 24, 2011, 15:42
Прокомментирую ваши ссылки. Тут дело вот в чём. В первом случае в обозначает некоторый конкретный, хотя, возможно, и неизвестный элемент (но ни в коем случае не произвольный). Во втором случае в обозначает произвольный элемент из заданной области. То есть у символа в этих двух случаях просто разные значения, которые смешивать нельзя, иначе получится какой-то софизм. То есть здесь фактически используются два рода переменных, но используемый символизм не очень хорошо позволяет их различать.

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

Цитата: RawonaM от мая 24, 2011, 15:54
Такое правило вывода не википедисты придумали, нас тоже этому учат. К каждому правилу поставляется определенное ограничение.

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

Цитата: RawonaM от мая 24, 2011, 15:54
Что формально мне мешает такой бредовый вывод сделать?

Скажем так, у нас есть два рода формальных переменных, одни из которых обозначают конкретные объекты (a, b, c), а другие произвольные (x, y, z). Однако в формулировках правил к ним не относится. Это на самом деле содержательня переменная, которая обозначает некоторый формальный объект. И лучше её было бы обозначить как-нибудь по-другому, чтобы не путать её с формальными переменными, например, греческой буквой . Тогда правила станут выглядеть как и с теми ограничениями, что в первом случае обозначает формальную переменную, обозначающую конкретный объект, а во втором случае - формальную переменную, обозначающую произвольный объект. При применении каждого правила вместо содержательной переменной подставляется соответствующий формальный объект. Из при помощи первого правила можно вывести (при заданном ограничении) , но не . А при помощи второго правила можно получить из , но не из . И бредовый вывод не получается. Единственная, на мой взгляд, здесь трудность, что формализм описан недостаточно ясно, что и приводит к недоразумениям.

Цитата: Gerbarius от мая 24, 2011, 17:03
В исчислении предикатов действительно справеделиво , но уже в общем случае неверно.

А это не следует по дедукции?

Цитата: RawonaM от мая 25, 2011, 10:10

Цитата: Gerbarius от мая 24, 2011, 17:03
В исчислении предикатов действительно справеделиво , но уже в общем случае неверно.

А это не следует по дедукции?

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

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

Цитата: Gerbarius от мая 25, 2011, 12:08
Если допустить ,  то отсюда можно получить

Я просто не понимаю, как вот это допустимо? Чем это отличается от ? Т.е. по-моему нужно очень конкретно оговаривать, чтобы сделать такой вывод.

В том то и дело, что из нельзя получить .

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

Из группы утверждений K не обязательно же следует A или ~A, правильно?

В общем, запутался вообще. У меня есть:






Для каждого из следующих утверждений нужно сказать, следует ли из утверждений 1-4:





Как к этому подходить?
Методом тыка нашел для 6 модель, которая показывает, что 6 не следует из 1-4.

Есть язык L={c, R} (c — константа, R — тринарное отношение). Формула p верна в некоей модели M. Почему у М обязательно есть минимальная модель?
Я так понимаю, что минимальная модель имеет область {c}, но все-таки неясно.

Цитата: RawonaM от июня 18, 2011, 17:40
тринарное

Тернарное!

Что-то я не могу врубиться: если модель Гербанда доказывает, что определенное высказывание верно, то она ведь опирается на определенную модель. Как можно сделать вывод, что она логически верна? Замучился уже...

Робот замучился выводить выводы... Жєсть...