Bir resmi sistem bir olan matematiksel modelleme genel uzmanlaşmış dil. Dilsel öğeler, sözcükler , cümleler , konuşmalar vb., sonlu nesnelerle (tamsayılar, diziler, ağaçlar veya sonlu grafikler vb.) temsil edilir. Biçimsel bir sistemin özelliği, öğelerinin gramer anlamındaki doğruluğunun algoritmik olarak doğrulanabilir olmasıdır, yani özyinelemeli bir küme oluşturmalarıdır .
Biçimsel sistemler , işleme algoritmalarının son derece karmaşık olduğu ve her şeyden önce dil dönüşümlerine uyum sağlamak için zaman içinde gelişmesi gereken doğal dillere karşıdır .
Biçimsel sistemler , matematiksel dil ve matematiksel akıl yürütmeyi temsil etmek için matematiksel mantıkta ortaya çıktı , ancak başka bağlamlarda da bulunabilir: bilgisayar bilimi, kimya, vb.
Biçimsel sistemler, matematik diliyle ilgili belirli problemleri ortaya koymak ve matematiksel olarak incelemek için mantıkçılar tarafından tasarlanmıştır. Bu açıdan onları genel metateoriler, (matematiksel) teoriler üzerine teoriler olarak değerlendirebiliriz.
Matematiksel dili modellemeyi amaçlayan mantık sistemleri üç problemi çözer:
Biçimsel sistemler , sonunda matematiğin katı kurallara göre sembollerin manipülasyonu oyunu olarak görünen, ancak a priori anlamdan yoksun görünen biçimci bakış açısı adı verilen bir matematik epistemolojisinin ortaya çıkmasına izin vermiştir ; formüllerin anlamı, akıl yürütme kuralları aracılığıyla birbirleriyle sürdürdükleri etkileşimlerle a posteriori olarak yeniden inşa edilir.
Bir aksiyomatik teori, matematiksel bir teoriyi temsil eden mantıksal bir sistemdir, yani hepsi aynı tür nesneyle ilgili bir dizi sonuç. Bir aksiyomatik teori, teorinin temel nesnelerini ve ilişkilerini tanımlayan formüller olan bir dizi aksiyom üzerine kuruludur ; bu aksiyomlardan ve muhakeme kurallarını kullanarak teorinin teoremlerini elde ederiz . Örneğin, küme teorisi , aksiyomları küme kavramını tanımlayan resmi bir sistemdir. Bir aksiyom, bu nedenle, akıl yürütme için bir başlangıç noktası olarak hizmet eden kanıtlanmamış bir önermedir: örneğin, “iki noktadan geçen bir ve yalnızca bir düz çizgi vardır”, Öklid geometrisinin bir aksiyomudur.
Aksiyomların veya formüllerin doğruluğu, bir modele , formüllerin yorumlandığı olası bir evrene göre tanımlanır .
Yukarıda söylediğimiz gibi formal sistemler özyinelemeli kümelerdir yani bir elemanın (formül, terim, tümdengelim) sisteme ait olup olmadığını algoritmik olarak kontrol edebiliriz. Aksiyomlarının kümesi olarak görülen bir aksiyomatik teori, bu kuraldan kaçmaz, yani bir aksiyomun teoriye ait olup olmadığını bilme sorunu kararlaştırılabilir .
Öte yandan, gelenek olduğu gibi, aksiyomlarının sonuçları kümesi, yani teoremleri kümesi olarak bir aksiyomatik teori düşünülürse, bu, nadir istisnalar dışında, özyinelemeli değildir. ancak yalnızca yinelemeli olarak numaralandırılabilir : mantıksal kuralları mekanik olarak ve tüm olası şekillerde uygulayarak aksiyomların tüm sonuçlarını sıralayacak bir program yazabilirsiniz. Öte yandan, bir formül F verildiğinde , bunun teorinin bir teoremi olup olmadığını nasıl yanıtlayacağını bilecek bir program yoktur ; veya daha doğrusu, önceki program aracılığıyla teorinin tüm teoremlerini sıralamaktan daha iyisi yapılamaz: eğer F bir teorem ise, o zaman sonlu bir zamanın sonunda numaralandırmada görünecektir, ancak değilse aksiyomların sonucu değil, program asla bitmez.
Bir aksiyom teorisi, aksiyomlarının sonucu olmayan formüller varsa tutarlıdır. Örneğin, Peano'nun aritmetiği tutarlıdır çünkü "0 = 1" formülünü kanıtlamaz. Tutarlılığı aynı şekilde bir çelişki göstermeme olgusu olarak tanımlayabiliriz.
Kurt Gödel , aritmetiği temsil edecek kadar güçlü herhangi bir aksiyomatik teorinin kendi tutarlılığını biçimsel bir şekilde gösteremeyeceğini gösterdi (bkz. Gödel'in eksiklik teoremi ).
Yukarıda söylediğimiz gibi, programlama dilleri biçimsel sistemlerdir: mantıksal sistemler matematiksel dili (teorem, gösterimler) biçimselleştirmek için kullanıldığından, programlama dilleri algoritmaları biçimselleştirir . Programlama dilleri en az iki bileşenden oluşur:
Buna bazen üçüncü bir bileşen eklenir:
Programlama dillerinden ayrı olarak, bilgisayar bilimi birkaç başka biçimsel sistem türünü tanımlar: bir programın istenen davranışını tanımlamaya hizmet eden belirtim dilleri , böylece daha sonra test edilebilir, doğrulanabilir veya belirli bir uygulamanın belirtimi karşıladığını gösterebilir; iletişim protokolleri kesinlikle bir ağda bilgisayarlar (veya cep telefonları) arasında bilgi alışverişini tanımlamak ...
Altıncı Hilbert problemi Alman matematikçi tarafından 1900 yılında yarattığı David Hilbert axiomatize fiziğine amaçları.
konulu bir konferansta 11 Eylül 1917 Zürih'te David Hilbert, herhangi bir fiziksel teorinin aksiyomlarının bütünün (matematikte olduğu gibi) bağımsızlığı ve çelişkisizliği kriterlerine uyması gerektiğini belirtir, buna ikinci nokta için başka bir bilimsel alanınkilerle çelişmeme zorunluluğu eklenir. .