Логическое определение с равным и законом тождества в «Введение в логику» Suppes
Патрик Суппес « Введение в логику » предоставляет правила для формальных определений в главе 8. Правила ниже указаны для нового символа операции с равенством:
Эквивалентность $D$ введение нового n-значного символа операции $O$ является правильным определением в теории тогда и только тогда, когда $D$ имеет вид:
$O(v_1, ..., v_n) = w \leftrightarrow S$
и выполняются следующие ограничения:
(i)$v_1, ..., v_n, w$- разные переменные.
(ii)$S$ не имеет свободных переменных, кроме $v_1, ..., v_n, w$.
(iii)$S$это формула, в которой единственными нелогическими константами являются примитивные символы и ранее определенные символы теории.
(iv) Формула$\exists !w[S]$ выводится из аксиом и предыдущих определений теории.
Также есть предварительное упоминание о Законе идентичности :
Если x - это что угодно, тогда $x=x$.
Теперь предположим, что у вас есть следующее определение:
$$ \forall f,x,y[f_x = y \iff f \text{ is a function } \land \langle x,y \rangle \in f] $$
Предположим также, что вы ранее определили функции и упорядоченные пары, так что вы можете доказать $\exists !y[S]$ с экстенциональностью, поэтому он следует правилу (iv).
Вот проблема: в рамках этого набора правил кажется, что можно использовать Закон идентичности с любой переменной, скажем$A$, чтобы утверждать, что $A_x=A_x$ и используйте это, чтобы заявить, что $A \text{ is a function } \land \langle x,A_x \rangle \in A$, и так, что $A$это функция, хотя мы ничего о ней не знаем. Эта логика может использоваться с любой переменной, будь то нормальное отношение, простой набор или даже элемент, поэтому этот вывод должен быть неправильным.
Сначала я подумал, что нарушаю правило (iii), поскольку утверждение "$A \text{ is a function } \land \langle x,A_x \rangle \in A$"содержит не определенный ранее символ, $A_x$, который определен в самом заявлении, поэтому он не будет действительным.
Однако рассмотрим следующее определение: $$ \newcommand\liff{\leftrightarrow} \newcommand\lif{\rightarrow} \newcommand\lfi{\leftarrow} \newcommand\ordp[2]{\langle #1,#2 \rangle} \newcommand\mset[1]{\{ #1 \}} \newcommand\isRel[1]{#1 \text{ is a relation}} \newcommand\isFunc[1]{#1 \text{ is a function}} \newcommand\isOneOne[1]{#1 \text{ is one-one}} \mset{a} = p \iff \forall x[x \in p \liff x = a] $$
Он уникален по своей протяженности. Кажется очевидным следствием этого, что$\mset{a} = \mset{b} \lif a = b$, но единственный способ доказать это - использовать $\mset{a} = \mset{b}$ получить $\forall x[x \in \mset{b} \liff x = a]$, который был бы запрещен, если бы моя интерпретация была правильной, поэтому я не думаю, что это ответ.
Вторым моим инстинктом было то, что правило (i) нарушается, что $f_x = f_x$не считается отдельными переменными. Однако из приведенного выше определения также кажется, что$a \in \mset{a}$должен следовать. Единственный способ доказать это - использовать$\mset{a} = \mset{a}$ с определением, которое было бы запрещено, если бы это было так, поэтому я тоже не считаю, что это решение.
Итак, мой вопрос: что является действительным виновником заблуждения?
Изменить: после расширенного обсуждения я добавляю некоторую информацию, чтобы, надеюсь, прояснить, о чем этот вопрос, а о чем нет.
Дело не в теории множеств . Моя проблема связана с формальным языком логики первого порядка, представленным в книге. Чтобы не заострять внимание на теории множеств, я приведу второй пример. Предположим, у нас есть следующие утверждения:
$$ \forall a,b,x,y[\text{isSingleChild}(x) \land \text{parentsOf}(a,b,x) \land \text{parentsOf}(a,b,y) \Rightarrow x = y] \\ \forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentsOf}(a,b,x) \land \text{isSingleChild}(x)] $$
Первое утверждение гарантирует, что $x$ уникален в определении $\text{son}$.
Определение $\text{son}\{a,b\}$похоже, соблюдает все предоставленные правила. Он не предназначен для утверждения, что любая переменная следует за каким-либо конкретным предикатом, а просто указывает их логическую взаимосвязь. Однако, если вы используете его вместе с Законом идентичности, вы можете получить:
$$ \newcommand{\fitch}[1]{\begin{array}{rlr}#1\end{array}} \newcommand{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \newcommand{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn \newcommand{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn \newcommand{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn \newcommand{\subproof}{\\[-0.25em]} %adjusts line spacing slightly \newcommand{\fendl}{\\[0.037em]} %adjusts line spacing slightly \small \fitch{ \fcol{1:\fendl 2:\fendl 3:\fendl\fendl 4:\fendl 5:\fendl 6:\fendl 7:\fendl 8:\fendl } & \scol { \forall a,b,x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\ \forall x[\text{son}\{a,b\} = x \iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,x) \land \text{isSingleChild}(x)] \\ \text{son}\{a,b\} = \text{son}\{a,b\} \\\quad\iff \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\ \forall x[x = x] \\ \text{son}\{a,b\} = \text{son}\{a,b\} \\ \text{isAdult}(a) \land \text{isAdult}(b) \land \text{parentOf}(a,b,\text{son}\{a,b\}) \land \text{isSingleChild}(\text{son}\{a,b\}) \\ \text{isAdult}(a) \\ \forall a [\text{isAdult}(a)] \\ } & \tcol{ \text{P} \fendl 1\ \forall\text{E}\ \fendl 2\ \forall\text{E}\ \fendl\fendl \text{T}\ \fendl 4\ \forall\text{E}\ \fendl 3,5\ {\liff}\text{E}\ \fendl 6\ {\land}\text{E}\ \fendl 7\ \forall\text{I}\ \fendl }} $$
Итак, из этого определения вы можете сделать вывод, что все взрослые. Обратите внимание на то, что я не говорю. Я не говорю, что этот аргумент здравый, и не защищаю его, я говорю, что набор правил, приведенный в книге, допускает это (вероятно, нет, но я не вижу, чтобы какое-либо правило логического вывода было нарушено). Я знаю, что этот аргумент нелогичен, но формальные правила соблюдаются . Мой вопрос не в обоснованности аргументации, а в обоснованности системы, представленной в книге.
Также обратите внимание, что утверждение касается не теории множеств или «теории семьи», а самой логики . Я утверждаю, что (очевидно) в рамках данной формальной системы применимо любое утверждение следующей формы:
$$ \forall a,b,x[\text{entityFrom}\{a,b\} = x \iff \text{hasSomeProperty}(a) \land \text{uniqueRelation}(a,b,x)] \vdash \forall a[\text{hasSomeProperty}(a)] $$
Я понимаю, что определение не влечет за собой заключения. Тем не менее, внутри системы вывод, кажется, можно сделать из нее.
Вариантов всего три. Либо формальная система, представленная в неадекватной, определение фактически влечет за собой вывод, либо я упускаю / неверно истолковываю какое-то правило закона идентичности / правила определения / правила для квантификаторов.
Книге более 50 лет, любые возможные упущения в системе были бы замечены к этому моменту (она также была написана Suppes, поэтому я сомневаюсь, что есть), поэтому я уверен, что это не первая книга. Определения также кажутся хорошо сформированными и не должны приводить непосредственно к заключению, так что это, вероятно, тоже не второе. Приводя к выводу, что я, вероятно, упускаю или неверно истолковываю некоторую оговорку / правило, которые сделали бы этот аргумент недействительным. Вопрос в том, какой именно?
На что не ответишь на вопрос:
- «В теории множеств функции имеют определенную область и должны иметь [некоторые свойства набора], поэтому невозможно, чтобы все переменные были функциями».
- «Ваше определение отцовства неверно описывает идею родителей, так как оно не подразумевает, что все дети имеют родителей и [некоторые свойства отцовства], поэтому определения не являются правильными описаниями».
Решение не может заключаться в несостоятельности аргумента в одной конкретной теории, который не сможет добраться до корня проблемы. В качестве примера можно использовать конкретный контекст, но решение должно быть на уровне формального языка.
Что может ответить на вопрос:
- "Набор правил, приведенный в книге, на самом деле неполный, потому что определение с равенством, содержащее [какое-то синтаксическое свойство], может привести к ошибке. Однако вы можете избежать этого, добавив новое правило, которое требует, чтобы ваше определение содержало [ограничение нового определения] "
- "Ваши определения логически влекут за собой вывод. Подумайте об этом, если ваше определение [это], то [объяснение того, почему определение должно логически вести к заключению], так что аргумент и вывод действительны. Я сомневаюсь, что вы намеревались сделать это тем не менее, завершите свое определение. Я думаю, что на самом деле вы имеете в виду [хорошее определение] ". $^{\dagger}$
- «Вы неверно истолковали правило [n], возможно, вы думаете, что оно означает [интерпретацию], когда оно на самом деле говорит [другое толкование]. Если вы примете это во внимание, строка [x] вашего аргумента неверна».
- "Вы забываете, что вы не можете заменять определенные термины, как переменные. Вы можете заменять определенный термин только в том случае, если применяется [какое-то синтаксическое условие], поэтому шаг $3$ вашего вычета недействительны ".
- "Закон тождественности требует не только уникальности, но и [некоторого переменного свойства], поэтому вы не можете использовать его в качестве строки $5$, поскольку переменная в вашем определении не подчиняется этому ограничению. "
Ваш ответ не обязательно должен быть одним из вышеперечисленных. Я просто представляю типы ответов, которые, по моему мнению, будут наиболее полезными: ответы, в которых основное внимание уделяется формальному языку.
Спасибо, что дочитали до конца, и я надеюсь, что это достаточно ясно проясняет проблему, которую я хочу решить.
$\dagger$Как отмечает Мауро АЛЛЕГРАНЗА, этот случай имеет особый смысл. Как он выразился:
Подумайте об этом: есть ли в вашей теории аксиомы, говорящие о том, что не каждый объект является Взрослым?
С чем я согласен. Однако есть одна проблема: набор правил не должен допускать этого .
Ранее в той же главе, до того, как правила будут установлены, изложена их цель . « Критерии правильных определений ». Цель состоит в том, чтобы отделить аксиому от определения. Первый ( критерий исключения ) не важен для данного обсуждения, а второй важен.
Критерий Non-Творчество утверждает , что определение$S$ не является творческим тогда и только тогда, когда:
Нет формулы $T$ в котором новый символ не встречается, так что $S \rightarrow T$ выводится из аксиом и предыдущих определений теории, но $T$ не так выводимо.
Цель набора правил - гарантировать, что наши определения соответствуют обоим этим критериям. Как сказано на странице 155: «[...] мы переходим к задаче формулирования правил определения, которые будут гарантировать выполнение двух критериев устраняемости и отсутствия творчества »
В моем примере с отцовством первое утверждение является аксиомой, а второе - определением. Однако в рамках этой теории утверждение$\forall a [\text{isAdult}(a)]$ не содержит нового символа и выводится из нового определения, но не только из аксиом, которые сделали бы определение творческим.
Итак, в этом случае у меня возникает вопрос: почему определение является творческим, если набор правил должен гарантировать отсутствие творчества?
Ответы
Набор правил, изложенный в книге, не является неполным. Приведенный вами пример вывода также заслуживает внимательного изучения. Вы получаете (казалось бы) парадоксальные выводы, потому что ограничение (iv) фактически не выполняется ни в одном из ваших примеров.
В вашем первом примере формула $S$ обозначает следующее: "$v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2$". Таким образом, ограничение (iv) не выполняется, если следующее не является теоремой рассматриваемой теории:
$$\exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
который, поскольку $v_1,v_2$ - различные свободные переменные, выполняется в точности, если
$$\forall v_1. \forall v_2. \exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
это тоже теорема вашей теории. Излишне говорить, что это последнее утверждение не является теоремой какой-либо разумной теории множеств. В частности, это будет означать "$\forall v. v \text{ is a function }$"само по себе.
Во втором примере формула $S$ обозначает следующее: "$\text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w)$". Как и выше, ограничение (iv) не выполняется, если следующее не является теоремой рассматриваемой теории:
$$ \forall v_1. \forall v_2. \exists! w. \text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w) $$
Но если приведенное выше предложение является теоремой вашей теории, то вы уже можете доказать (напрямую, начиная с предложения выше в качестве предпосылки и используя $\forall E$, $\wedge E$ и $\forall I$) который $\forall v_1. \text{isAdult}(v_1)$ это теорема вашей теории.