Eşit şekilde mantıksal tanımlama ve Destekler "Mantığa Giriş" te Kimlik Hukuku
Patrick, " Mantığa Giriş ", bölüm 8'deki biçimsel tanımlar için kurallar sağlar. Eşitliğe sahip yeni bir işlem sembolü için aşağıdaki kurallar belirtilmiştir:
Bir denklik $D$ yeni bir n-yeri işlem sembolünün tanıtımı $O$ bir teoride uygun bir tanımdır ancak ve ancak $D$ şu biçimde:
$O(v_1, ..., v_n) = w \leftrightarrow S$
ve aşağıdaki kısıtlamalar karşılandı:
(i)$v_1, ..., v_n, w$farklı değişkenlerdir.
(ii)$S$ dışında ücretsiz değişken içermez $v_1, ..., v_n, w$.
(iii)$S$tek mantıksal olmayan sabitlerin ilkel semboller ve teorinin önceden tanımlanmış sembolleri olduğu bir formüldür.
(iv) Formül$\exists !w[S]$ teorinin aksiyomlarından ve önceki tanımlarından türetilebilir.
Ayrıca Kimlik Yasası'ndan da önceden bahsedilmiş :
X herhangi bir şeyse, o zaman $x=x$.
Şimdi aşağıdaki tanıma sahip olduğunuzu varsayalım:
$$ \forall f,x,y[f_x = y \iff f \text{ is a function } \land \langle x,y \rangle \in f] $$
Ayrıca, ispatlayabileceğiniz şekilde önceden tanımlanmış fonksiyonlara ve sıralı çiftlere sahip olduğunuzu varsayalım. $\exists !y[S]$ ölçülülükle, bu nedenle kural (iv) 'e uyar.
Sorun şu: Bu kural setinin sınırları içinde , Kimlik Yasası herhangi bir değişkenle kullanılabilir gibi görünüyor , diyelim ki$A$bunu iddia etmek $A_x=A_x$ ve bunu iddia etmek için kullan $A \text{ is a function } \land \langle x,A_x \rangle \in A$, Ve böylece $A$hakkında hiçbir şey bilmesek de, bir işlevdir. Bu mantık herhangi bir değişkenle kullanılabilir, normal bir ilişki, basit bir küme veya hatta bir dürtü olabilir, bu nedenle bu çıkarım yanlış olmalıdır.
İlk başta, ifade olarak (iii) kuralı çiğnediğimi düşündüm "$A \text{ is a function } \land \langle x,A_x \rangle \in A$"içinde önceden tanımlanmamış bir sembol var, $A_x$, ifadenin kendisinde tanımlandığı için geçerli olmayacaktır.
Ancak, aşağıdaki tanımı göz önünde bulundurun: $$ \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] $$
Kapsamlılık açısından benzersizdir. Bunun net bir sonucu gibi görünüyor ki$\mset{a} = \mset{b} \lif a = b$, ancak bunu kanıtlamanın tek yolu, $\mset{a} = \mset{b}$ almak için $\forall x[x \in \mset{b} \liff x = a]$, eğer yorumum doğru olsaydı buna izin verilmezdi, bu yüzden cevabın bu olduğunu sanmıyorum.
İkinci içgüdülerim, (i) kuralının ihlal edilmesiydi, $f_x = f_x$farklı değişkenler olarak sayılmaz. Bununla birlikte, yukarıdaki tanımdan da öyle görünüyor ki$a \in \mset{a}$takip etmeli. Bunu kanıtlamanın tek yolu kullanmak$\mset{a} = \mset{a}$ tanımla, eğer durum böyle olsaydı izin verilmeyecekti, bu yüzden bunun da çözüm olduğunu düşünmüyorum.
Öyleyse sorum şu: Hatanın asıl suçlusu nedir?
Düzenleme: Uzun tartışmadan sonra, bu sorunun ne hakkında olup ne olmadığını açıklığa kavuşturmak için bazı bilgiler ekliyorum.
Bu küme teorisi ile ilgili değil . Benim sorunum, kitabın sağladığı birinci dereceden mantığın biçimsel dili ile ilgili. Küme teorisine odaklanmaktan kaçınmak için ikinci bir örnek vereceğim. Aşağıdaki ifadelere sahip olduğumuzu varsayalım:
$$ \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)] $$
İlk ifade şunu garanti eder: $x$ tanımında benzersizdir $\text{son}$.
Tanımı $\text{son}\{a,b\}$sağlanan tüm kurallara uyuyor gibi görünüyor. Herhangi bir değişkenin belirli bir yüklemi takip ettiğini belirtmek değil, sadece mantıksal ilişkilerini belirtmek amaçlanmıştır. Bununla birlikte, Kimlik Hukuku ile birlikte kullanırsanız, türetebilirsiniz:
$$ \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 }} $$
Yani bu tanımdan, herkesin bir yetişkin olduğu sonucuna varabilirsiniz. Ne söylemediğime dikkat edin. Bu argümanın sağlam olduğunu veya savunmadığını söylemiyorum, kitapta verilen kuralların buna izin verdiğini söylüyorum (Muhtemelen izin vermiyor, ancak mantıksal çıkarım kuralının ihlal edildiğini görmüyorum). Tartışmanın mantıksız olduğunu biliyorum ama resmi kurallara uyuluyor . Sorum argümanın sağlamlığıyla ilgili değil, kitapta verilen sistemin sağlamlığıyla ilgili.
Ayrıca iddianın küme teorisi veya "aile teorisi" ile ilgili olmadığını, mantığın kendisiyle ilgili olduğunu unutmayın . Benim iddiam, verilen resmi sistem içinde (görünüşe göre), aşağıdaki formdaki herhangi bir ifadenin geçerli olduğudur:
$$ \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)] $$
Tanımın sonucu gerektirmediğini anlıyorum. Bununla birlikte, sistem içinde, sonuç bundan çıkarılabilir görünüyor.
Yalnızca üç seçenek var. Ya sağlam olmayan biçimsel sistem, tanım aslında sonucu gerektirir ya da Kimlik Yasası / Tanım için Kurallar / Nicelik Belirleyicileri için Kurallar ile ilgili bazı kuralları eksik / yanlış yorumluyorum.
Kitap 50 yıldan daha eski, sistemdeki olası herhangi bir eksiklik bu noktada fark edilmiş olacaktı (aynı zamanda Suppes tarafından yazılmıştır, bu yüzden var olduğundan şüpheliyim), bu yüzden ilk olmadığına eminim. Tanımlar da iyi biçimlendirilmiş görünüyor ve doğrudan sonuca götürmemeleri gerektiğini düşünüyor, bu yüzden muhtemelen ikincisi de değil. Bu argümanı geçersiz kılacak bazı koşulları / kuralları muhtemelen kaçırdığım veya yanlış yorumladığım sonucuna götürür. Soru şu ki, hangisi?
Soruyu cevaplamayacak şey:
- "Küme teorisinde, işlevlerin belirli bir alanı vardır ve [bazı ayarlı özelliklere] sahip olmaları gerekir, bu nedenle tüm değişkenlerin işlev olması mümkün değildir."
- "Ebeveynlik tanımınız, ebeveyn fikrini doğru bir şekilde tanımlamıyor çünkü bu, tüm çocukların ebeveynlere ve [bazı ebeveynlik özelliklerine] sahip olduğu anlamına gelmez, bu nedenle tanımlar doğru tanımlar değildir."
Çözüm, sorunun kökenine inmeyecek belirli bir teorideki argümanın yetersizliği hakkında olamaz. Örnek olarak belirli bir bağlam kullanılabilir, ancak çözüm resmi dil düzeyinde olmalıdır.
Sorunun cevabı ne olabilir:
- "Kitapta verilen kural seti aslında eksiktir, çünkü [bazı sözdizimsel nitelikleri] içeren eşitliğe sahip bir tanım yanılgıya yol açabilir. Ancak, tanımınızda [yeni tanım çelişkisi] olmasını gerektiren yeni bir kural ekleyerek bundan kaçınabilirsiniz. "
- "Tanımlarınız mantıksal olarak sonucu gerektirir. Bir düşünün, eğer tanımınız [bu] ise, o zaman [tanımın neden mantıksal olarak sonuca götürmesi gerektiğinin açıklaması], yani argüman ve sonuç geçerli. Bunu yapmak istediğinizden şüpheliyim Yine de tanımınızla sonuçlandırın. Bence aslında demek istediğiniz [iyi davranışlı tanım]. " $^{\dagger}$
- "[N] kuralını yanlış yorumladınız, belki de aslında [farklı yorumlama] derken [yorumlama] anlamına geldiğini düşünüyorsunuz. Bunu hesaba katarsanız, argümanınızın [x] satırı geçerli değildir."
- "Değişkenler gibi tanımlı terimlerin yerini alamayacağınızı unutuyorsunuz. Tanımlanmış bir terimi yalnızca [bazı sözdizimsel koşullar] geçerliyse değiştirebilirsiniz, bu nedenle adım $3$ kesintiniz geçersiz. "
- "Kimlik Yasası yalnızca benzersizliği değil, aynı zamanda [bazı değişken özellikleri] de gerektirdiğinden, onu aynı hizada kullanmayabilirsiniz. $5$, çünkü tanımınızdaki değişken bu kısıtlamaya uymuyor. "
Cevabınızın yukarıdakilerden herhangi biri olması gerekmez . Sadece büyük olasılıkla yararlı olacağını düşündüğüm cevap türlerini sunuyorum: Biçimsel dile odaklanan cevaplar.
Sonuna kadar okuduğunuz için teşekkür ederim ve umarım bu, çözmek istediğim sorunu yeterince açık hale getirir.
$\dagger$Mauro ALLEGRANZA'nın işaret ettiği gibi, bu durum özellikle mantıklı. Dediği gibi:
Bir düşünün: teorinizde her nesnenin bir Yetişkin olmadığını söyleyen bazı aksiyomlar var mı?
Ben de katılıyorum. Ancak bir sorun var: Kural seti buna izin vermemelidir .
Aynı bölümün başlarında, kurallar belirlenmeden önce hedefleri ortaya konmuştur. " Uygun tanımlamalar için kriterler ". Amaç, bir aksiyomu bir tanımdan ayırmaktır. İlki ( Ortadan Kaldırılabilirlik Kriteri ) bu tartışma için önemli değil, ancak ikincisi önemli.
Olmayan Yaratıcılık Kriter bir tanım belirtiyor$S$ şu durumlarda yaratıcı değildir:
Formül yok $T$ yeni sembolün meydana gelmediği $S \rightarrow T$ teorinin aksiyomlarından ve önceki tanımlarından türetilebilir, ancak $T$ o kadar türetilemez.
Kural setinin amacı, tanımlarımızın bu kriterlerin her ikisine de uymasını sağlamaktır. 155. sayfada belirtildiği gibi: "[...] ortadan kaldırılabilirlik ve yaratıcı olmama kriterlerinin karşılanmasını garanti edecek tanım kurallarını belirleme görevine dönüyoruz "
Ebeveynlik örneğimde, bir aksiyom olarak ilk ifadeye ve bir tanım olarak ikinciye sahibiz. Bununla birlikte, bu teori içinde ifade$\forall a [\text{isAdult}(a)]$ yeni sembolü içermez ve yeni tanımdan türetilebilir, ancak tek başına tanımı yaratıcı kılacak aksiyomlardan türetilemez.
Öyleyse bu durumda, sorum şu oluyor: Kural kümesinin yaratıcı olmayışı garanti etmesi beklendiğinde tanım nasıl oluyor da yaratıcı oluyor?
Yanıtlar
Kitabın verdiği kurallar eksik değil. Verdiğiniz örnek türetme de incelemeye dayanır. (Görünüşte) paradoksal sonuçlar elde edersiniz çünkü kısıtlama (iv) gerçekte örneklerinizin hiçbirinde geçerli değildir.
İlk örneğinizde formül $S$ şu anlama gelir: "$v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2$". Dolayısıyla, aşağıdakiler incelenen teorinin bir teoremi olmadığı sürece kısıtlama (iv) yerine getirilmez:
$$\exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
o zamandan beri $v_1,v_2$ farklı serbest değişkenlerdir, tam olarak şu durumlarda geçerlidir:
$$\forall v_1. \forall v_2. \exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
aynı zamanda teorinizin bir teoremidir. Söylemeye gerek yok, bu ikinci cümle, herhangi bir makul küme teorisinin teoremi değildir. Özellikle "$\forall v. v \text{ is a function }$" kendi kendine.
İkinci örneğinizde formül $S$ şu anlama gelir: "$\text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w)$". Yukarıda olduğu gibi, aşağıdakiler incelenen teorinin bir teoremi olmadığı sürece, kısıtlama (iv) yerine getirilmez:
$$ \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) $$
Fakat yukarıda verilen cümle teorinizin bir teoremiyse, o zaman zaten ispatlayabilirsiniz (doğrudan yukarıdaki cümleden bir öncül olarak başlayarak ve $\forall E$, $\wedge E$ ve $\forall I$) bu $\forall v_1. \text{isAdult}(v_1)$ teorinizin bir teoremidir.