Önermeler mantığı (ya da sıfırıncı-derece mantık), mantığın önermelerle ilgilenen dalıdır. Birden fazla önermenin mantık bağlaçları kullanılarak bir araya getirilmesiyle oluşturulan yeni önermelerin doğruluğunun belirlenmesi için kullanılır. Önermeler mantığının niceleyiciler, eşitlik ve ait olma ilişkileriyle genişletilmesi birinci-derece mantığın konusudur.

Doğal dillerde de kullanılan "ve", "veya", "değil", "eğer" gibi bağlaçlar ile önermeler arasında ilişkiler kurulur. Bu ilişkiler kullanılarak yeni önermelerin doğruluğu çıkarsanır.

Önermeler mantığı kapsamında yapılabilecek basit bir çıkarsama örneği şu şekildedir:

Öncül 1: Eğer yağmur yağıyor ise, hava bulutludur.

Öncül 2: Yağmur yağıyor.

Sonuç: Hava bulutlu.

Burada hem öncüller hem de sonuç birer önermedir. Öncüllerin var olduğu kabul edilir ve modus ponens çıkarsama kuralı uygulanarak sonuç elde edilir.

Önermeler mantığı bağlaçlarla ayrılabilenin ötesinde önermelerin yapısıyla ilgilenmez. Doalyısıyla, yukarıdaki örnekte en temel yargılar birer harf ile gösterilerek aşağıdaki gibi yeniden yazılabilir:

Öncül 1: ${\displaystyle P\to Q}$

Öncül 2: ${\displaystyle P}$

Sonuç: ${\displaystyle Q}$

Aynısı daha kısa bir şekilde de ifade edilebilir:

${\displaystyle P\to Q,P\vdash Q}$

${\displaystyle P}$ “yağmur yağıyor” ve ${\displaystyle Q}$ “hava bulutlu” olarak anlamlandırıldığında, üstteki sembolik ifadelerin doğal dildeki esas ifadeye birebir karşılık geldiği görülür. Buna ek olarak, üstteki sembolik ifadeler bu biçime uygun diğer önermelerden benzer çıkarımlar yapılmasını da sağlar.

Önermeler mantığı izleri daha önceki felsefecilerde rastlansa da ilk defa Hrisippos tarafından MÖ 3. yüzyılda düzenli bir biçime sokuldu^[1] ve takipçisi olan Stoacılar tarafından genişletildi. Bu mantık önermeler üzerine kurulmuştu. Stoacıların mantığı terimler üzerine kululmuş olan geleneksel tasımcı mantıktan farklıydı. Ancak, daha sonraki çağlarda unutuldu. Aynı sistem 12. yüzyılda Pierre Abélard tarafından yeniden icat edildi.^[2]