Formalismus je jedním z přístupů k filozofii matematiky , snažící se redukovat problém základů matematiky na studium formálních systémů . Spolu s logicismem a intuicionismem byl ve 20. století považován za jeden ze směrů fundamentalismu ve filozofii matematiky.
Formalismus vznikl na počátku 20. století v Hilbertově matematické škole jako součást pokusu spojit rigorózní zdůvodnění různých oblastí matematiky do jediného systému. Vyvinuli Hilbertovi spolupracovníci (učedníci) Ackerman , P. Bernays , von Neumann .
Na rozdíl od logicismu si formalismus nečinil nárok na vybudování formální teorie, která by byla jednotná pro celou matematiku, jako je teorie množin nebo teorie typů . Na rozdíl od intuicionismu formalismus neodmítal konstruovat teorie s „pochybnými“ základy z hlediska intuice, pokud v nich byla přísně podložena pravidla pro odvozování teorémů. Formalisté věřili, že matematika by měla studovat co nejvíce formálních systémů.
Formální axiomatické teorie postavené na základě klasické logiky má smysl uvažovat pouze tehdy, pokud v nich nejsou žádné rozpory , protože jinak se jakýkoli úsudek teorie ukáže jako „prokázaný“. Pokud je v takovém formálním systému možné prokázat logickou lež , pak je nekonzistentní a „zamítnutá“, což znehodnocuje všechny teorémy dokázané v rámci tohoto systému. Matematiky samozřejmě znepokojovala otázka, zda je možné nějak dokázat konzistenci teorie. K nelibosti formalistů se ukázalo, že otázka nekonzistence teorie nemá adekvátní řešení v žádném z formálních systémů používaných v matematice .
Nic nebrání studiu jedné formální teorie s pomocí jiné; tento přístup se nazývá metamatematický . Nutí nás však používat nejspolehlivější základy pro konstrukci metateorií, které formalisté považovali opět za klasickou logiku a formální aritmetiku .
Od počátku 90. let 20. století zájem o formalismus (v aplikovanějším smyslu) opět vzrostl v souvislosti s problémy automatického dokazování vět (viz např. manifest QED ).