../
2026-01-21 Software Logic
- People think about deductive reasoning in Truth theoretical
- Lean provides a constructive environment. This is proof theoretical
Example Truth theoretical
proposition algebra is isomorphic to boolean algebra
Some proposition P
P can have two values - true, false
Similarly lets have another proposition called Q
We can construct a new proposition from these two using propositional
connectors
P |
Q |
P && Q |
|---|---|---|
| F | F | F |
| F | T | F |
| T | F | F |
| T | T | T |
In propositional logic, && is $\wedge$
We can think of $\wedge$ as a function that takes two booleans and returns boolean