Propositional logic is a simplified model of what it means to prove things. The statements that propositional logic can work with are called propositions. Propositions consist of the primitives as well as anything of the form where and are propositions. Note for pedants, this description allows the existence of propositions that can't be broken down into a finite number of primitives, we don't want such propositions.
Let be the set of all propositions formed by taking any arbitrary propositions , and , in any of the following three arrangements.
The set is the set of axioms, and the three forms shown above are the infinite axiom schema. For example, taking and then applying the first schema gets . So this is an axiom.
We say that a set of propositions implies another proposition , when there exists a proof of from . Write this as .
A proof of a proposition form is a list of propositions of length such that and for each , fulfills at least one of the following 3 conditions.
3) This is called Modus ponens
For example, here is a proof of
Formed using the second axiom schema.
Is then created using the first axiom schema
Can be produced by modus ponens because .
Is allowed by using axiom schema 1 again.
Follows by modus ponens again because .
Philosophically Important Takeaways
The notion of mathematical proof is fully formalized. There is an entirely mechanical, and fairly fast, method of verifying proofs. Proofs can be generated in a finite amount of time, by brute force search, but this can be much slower.
The proof framework only believes things that you have actually proved in it. From our point of view outside the framework, the proof of also shows that , but to actually prove that within the framework, you have to go through all the steps again.