Brandon Rozek

Photo of Brandon Rozek

PhD Student @ RPI studying Automated Reasoning in AI and Linux Enthusiast.

Theorem Proving Definitions

Published on

Updated on

Warning: This post has not been modified for over 2 years. For technical posts, make sure that it is still relevant.

When I look into a new field, sometimes I get confused by the whole new set of vocab terms I need to encounter. This post will serve to keep me straight with the terms involved in theorem proving.

Word Definition
Modus Ponens If $P$ implies $Q$ and $P$ is asserted to be true, then $Q$ must be true.
Complete If every formula having the property can be derived using the system. (i.e The system does not miss a result)
Negation-Complete Either $\phi$ or $\neg \phi$ can be proved in the system.
Consistent For any provable formula $\phi$, the negation ($\neg \phi$) cannot be provable. (Cannot derive a contradiction)
Decidable An effective method exists for deriving the correct answer in a finite time.
Sound Every formula that can be proved in the system is logically valid with respect to the semantics of the system. (i.e The system does not produce a wrong result)

Hopefully, I’ll come back and add more terms as I get confused.

Reply via Email Buy me a Coffee
Was this useful? Feel free to share: Hacker News Reddit Twitter

Published a response to this? :