OP, aşağıdakilerin resmi bir kanıtını ister:
Öncelik: A ∨ (B ∧ C)
Öncelik: ¬B ∨ ¬C ∨ D
Hedef: A ∨ D
Unutulmaması gereken ilk şey, ikinci öncül gibi görünmekle birlikte, bir şeyin sembolize edilmesidir, geçerli bir cümle değildir. Bu sadece bir ifadedir. Bağlantıların "∨" kapsamı belirsizdir. Bunu resmi olarak kullanabileceğimiz bir cümle yapmak için yeniden yazılması gerekiyor.
(¬B ∨ ¬C) ∨ D
veya olarak
¬B ∨ (¬C ∨ D)
Bunu görmek için ¬B ∨ ¬C expression D ifadesini bir kanıt denetleyicisine koymaya çalışın. Biri bile başlayabilir mi? Bu, doğal kesinti ve ispat kontrolünü kullanmayı denediğimde oldu. //forallx.openlogicproject.org/ "rel =" nofollow noreferrer "> forall x: Calgary Remix :
“∨” bağını “ya da” olarak algıladığımız insan anlayışımıza dayanarak, ifadeyi olduğu gibi kullanmak için gayri resmi olarak devam edebiliriz ve vakalar yaptığımızı düşünürüz. Öncelikle "¬B", daha sonra da ""C" ve daha sonra da D olayını ele alacağız ve her durumda "A ∨ D" hedefine ulaşıp ulaşamayacağımızı göreceğiz.
Ancak, resmi kanıt istediğimizden, bu şekilde devam edemeyiz. Bize ne kadar bariz olursa olsun, cümleleri, keyfi ifadeleri kullanmalıyız ve resmi kanıtın her bir satırını haklı çıkarmak için resmi kurallar kullanmamalıyız (yani “∨”). Kanıt denetleyici, cümleler kullandığımızı ve kuralları izlediğimizi doğrulamamıza yardımcı olur.
Eğer cümle olarak ~ B v (~ C v D) seçerseniz, aşağıdaki gibi bir kanıt elde edebiliriz.
Bu kanıt, binaların her ikisinde de subaplar yoluyla "V" bağını resmen ortadan kaldırarak durumları ele almanın bir yolunu göstermektedir.
İlk öncülündeki iki vakayı düşünün. Varsayalım ki, hat 3'teki varsayım olarak "A" ile bir alt-kaplamayı başlat ve 4. satırda istenen hedefe ulaşırım ve 5. satırda "(B ∧ C)" almayı ve hat 18'de istenen hedefe ulaşmayı kabul ediyorum. Hedefe ulaşan "V" bağlayıcının her iki tarafı da "V" yi ortadan kaldırabilir ve kanıtı tamamlayabilirim. Bu eleme, her dava için bir tane olmak üzere iki sub-proof tarafından temsil ettiğim iki varsayımı boşaltır.
Yukarıdaki ikinci durum daha fazla satır gerektirdi. Bu detayları düşünelim. İkinci dava için hedefe ulaşmak için, "(B ∧ C)", ikinci önermeyi kullanmam gerekiyordu. "¬B" harfini, 7 numaralı satırda bir varsayım olarak "¬B" ile bir subproof oluşturarak ve 9. satırdaki hedefe ulaşarak aldım ve 10 numaralı satırdaki "∨C ∨ D" durumunu aldım ve sonuçta sonuca ulaştı 17. “∨C ∨ D” nin aynı zamanda bir “∨” cümlesi olduğunu ve bu yüzden de vakalara, yani sub-proof'lere de ihtiyaç duyduğumu unutmayın. Bunu 10 ile 17 arasındaki satırlarda yaptım.
OP'deki şartlardan biri şuydu:
DeMorgan Yasasını kullanmadan resmi olarak kanıtlayın
Yukarıdaki kanıtta DeMorgan Yasasını kullanmadığımı not edin. DeMorgan Yasası'nın nasıl kullanıldığını görmek için aşağıdaki kanıtı "(¬B ∨ ¬C) ∨ D" kullanarak düşünün.
