website/content/blog/proofdef.md

24 lines
1.3 KiB
Markdown
Raw Normal View History

2020-01-15 21:51:49 -05:00
---
title: "Theorem Proving Definitions"
date: 2019-12-29T11:21:07-05:00
draft: false
2024-01-15 19:35:59 -05:00
tags:
- Formal Methods
2020-01-15 21:51:49 -05:00
images: []
math: true
2023-01-05 14:04:45 -05:00
medium_enabled: true
2020-01-15 21:51:49 -05:00
---
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.
2021-12-15 14:07:16 -05:00
| 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. |
2021-12-15 14:10:07 -05:00
| Consistent | For any provable formula $\phi$, the negation ($\neg \phi$) cannot be provable. (Cannot derive a contradiction) |
2021-12-15 14:07:16 -05:00
| 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) |
2020-01-15 21:51:49 -05:00
Hopefully, I'll come back and add more terms as I get confused.