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 ⊥,p1,p2,p3,⋯ as well as anything of the form (X⟹Y) where X and Y 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 A be the set of all propositions formed by taking any arbitrary propositions X, Y and Z, in any of the following three arrangements.
1) (X⟹(Y⟹X))
2) ((X⟹(Y⟹Z))⟹((X⟹Y)⟹(X⟹Z)))
3) (((X⟹⊥)⟹⊥)⟹X)
The set A is the set of axioms, and the three forms shown above are the infinite axiom schema. For example, taking X=p1 and Y=(p2⟹⊥) then applying the first schema gets (p1⟹((p2⟹⊥)⟹p1))∈A. So this is an axiom.
We say that a set of propositions S implies another proposition p, when there exists a proof of p from S. Write this as S⊢p.
A proof of a proposition p form S is a list L of propositions of length n∈N such that Ln=p and for each i≤n, Li fulfills at least one of the following 3 conditions.
Can be produced by modus ponens because L1=(L2⟹L3).
L4=(pX⟹(pY⟹pX))
Is allowed by using axiom schema 1 again.
L5=(p⟹p)
Follows by modus ponens again because L3=(L4⟹L5).
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 (p⟹p) also shows that (q⟹q), but to actually prove that within the framework, you have to go through all the steps again.
Propositional Logic
Some Definitions
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 ⊥,p1,p2,p3,⋯ as well as anything of the form (X⟹Y) where X and Y 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 A be the set of all propositions formed by taking any arbitrary propositions X, Y and Z, in any of the following three arrangements.
1) (X⟹(Y⟹X))
2) ((X⟹(Y⟹Z))⟹((X⟹Y)⟹(X⟹Z)))
3) (((X⟹⊥)⟹⊥)⟹X)
The set A is the set of axioms, and the three forms shown above are the infinite axiom schema. For example, taking X=p1 and Y=(p2⟹⊥) then applying the first schema gets (p1⟹((p2⟹⊥)⟹p1))∈A. So this is an axiom.
We say that a set of propositions S implies another proposition p, when there exists a proof of p from S. Write this as S⊢p.
A proof of a proposition p form S is a list L of propositions of length n∈N such that Ln=p and for each i≤n, Li fulfills at least one of the following 3 conditions.
1) Li∈S
2) Li∈A
3) ∃j,k<i:Lj=(Lk⟹Li) This is called Modus ponens
Example Proof
For example, here is a proof of (p⟹p)
Formed using the second axiom schema.
Is then created using the first axiom schema
Can be produced by modus ponens because L1=(L2⟹L3).
Is allowed by using axiom schema 1 again.
Follows by modus ponens again because L3=(L4⟹L5).
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 (p⟹p) also shows that (q⟹q), but to actually prove that within the framework, you have to go through all the steps again.