Soundness and completeness of a calculus. Constructing formal proofs in the calculus HK. Informal proofs. Provability and unprovability. Contradictory and consistent theories. Methods for proving completeness, quantifier elimination. Decidability. Recursive and recursively enumerable sets. Prominent axiomatic theories. Proving undecidability of strong theories (that is, proving Gödel's first incompleteness theorem) using recursively enumerable sets.
Last update: Švejdar Vítězslav, doc. RNDr., CSc. (24.09.2020)
Korektnost a úplnost kalkulu. Kalkulus HK a konstrukce důkazů. Neformální důkazy. Dokazatelnost a nedokazatelnost. Sporné a bezesporné teorie. Úplnost axiomatické teorie. Metody prokazování úplnosti, zejména eliminace kvantifikátorů. Rozhodnutelnost. Rekurzívní a rekurzívně spočetné množiny. Prominentní axiomatické teorie. Prokazování nerozhodnutelnosti silných teorií (tj. důkaz první Gödelovy věty) s využitím rekurzívně spočetných množin.
Last update: Švejdar Vítězslav, doc. RNDr., CSc. (24.09.2020)