Rachunek zdań to dział logiki matematycznej badający związki między zdaniami lub funkcjami zdaniowymi utworzonymi za pomocą spójników zdaniowych ze zdań lub funkcji zdaniowych prostszych. Rachunek zdań określa sposoby stosowania spójników zdaniowych w poprawnym wnioskowaniu. w klasycznym rachunku zdań przyjmuje się założenie, że każdemu zdaniu można przypisać jedną z dwu wartości logicznych - prawdę lub fałsz, które umownie przyjęto oznaczać 1 lub 0. Dlatego klasyczny rachunek zdań nazywa się dwuwartościowym rachunkiem zdań. W rachunku zdań treść rozpartywanych zdań nie ma znaczenia, ważna jest jedynie ich wartość logiczna. Wartość logiczna zdań złożonych powstałych przez zastosowanie spójników zdaniowych określa funkcja prawdziwościowa, związana z każdym spójnikiem zdaniowym. Wartość ta zależy wyłącznie od prawdziwości lun fałszywości zdań składowych, nie zależy natomiast od ich treści. Szczególną rolę w rachunku zdań odgrywają takie zdania złożone, których wartość logiczna jest równa jeden, niezależnie od tego, jakie wartości logiczne mają zdania proste, z których są one zbudowane. Takie zdania nazywa się prawami (tautologiami) rachunku zdań. Wiele praw klasycznego rachunku zdań znano w starożytności. Rachunkiem zdań zajmowano się również w średniowieczu. Współczesne, sformalizowane ujęcie rachunku zdań po raz pierwszy podał w 1879 roku logik niemiecki G.L. Frege. Niemałą rolę w rozwoju rachunku zdań odegrali też logicy polscy, a wśród nich głównie J. Łukasiewicz.

Sformalizowany język rachunku zdań to ściśle zdefiniowany język, w którym sformułowany jest współczesny rachunek zdań. Znakami alfabetu sformalizowanego języka rachunku zdań są symbole zmiennych zdaniowych (p, q, r, ...), symbole spójników logicznych (\/, /\, ¬, =>, <=>) oraz nawiasy. Zmienne zdaniowe są wyrażeniami zerowego stopnia sformalizowanego języka rachunku zdań, wyrażeniami stopnia n+1 są wyrażenia mające postać: α\/β, α/\β, ¬α, α=>β, α<=>β, gdzie α, β są wyrażeniami stopnia co najwyżej n lub takimi wyrażeniami wziętymi w nawias. Na przykład wyrażenie (¬p)=>q jest wyrażeniem drugiego stopnia, a wyrażenie ¬(p\/q)/\(p\/r) jest wyrażeniem trzeciego stopnia. Sformalizowany język rachunku zdań nazywa się językiem zerowego rzędu. Na szczególną uwagę zasługuje beznawiasowa symbolika logiczna, wprowadzona przez logika polskiego J. Łukasiewicza i nazwana od nazwiska jej twórcy symboliką Łukasiewicza albo symboliką polską lub odwrotną notacją polską. Zgodnie z tą symboliką spójnik zdaniowy (oznaczony symbolem literowym: A - alternatywa, K - koniunkcja, N - negacja, C - implikacja, E - równoważność) umieszcza się zawsze przed argumentem lub argumentami tego spójnika. Na przykład zdanie p\/q w symbolice Łukasiewicza ma postać Apq. Podobnie zamiast p/\q można napisać Kpq. Zdanie ¬(p/\q)<=>(¬p\/¬q) w symbolice Łukasiewicza ma postać ENKpqANpNp. Symbolika Łukasiewicza jest stosowana w programowaniu elektronicznych maszyn cyfrowych.

Prawa rachunku zdań, tautologie rachunku zdań to zdania sformalizowanego języja rachunku zdań, których wartość logiczna, niezależna od wartości logicznych występujących w nich zdań prostych, jest równa 1. Istnieje ogólna metoda sprawdzania, czy dane zdanie jest prawem rachunku zdań. Jest to tzw. metoda zerojedynkowa, która polega na rozpatrzeniu wszystkich możliwych przypadków logicznych zdań prostych. Jeśli w jakimś przypadku okaże się, że wartość logiczna rozpatrywanego zdania będzie równa zero, to nie jest ono prawem rachunku zdań. W przeciwnym razie zdanie jest prawem rachunku zdań.