I'm studying logic as part of my discrete mathematics course, and while the book does a good job at explaining propositions, connectives, quantifiers, proofs, etc, in a mechanical way, I'm trying to get a deeper understanding of how logic explains mathematics.
I've developed a personal framework as to how everything is connected, but my formal knowledge about these topics is still very limited, so I would appreciate if someone could confirm/correct the following.
First of all let's define
p, q, r,...as atomic propositions
a, b, c,...as derived propositions, i.e. propositions that can be expressed as compound statements of the atomic propositions (e.g.a ≡ p^q -> r)
Let's also ignore quantifiers for simplicity.
Now, as far as I could intuitively understand: Mathematics has been axiomatized with ZFC, which is a set of atomic and derived propositions that are assumed to be true, without any proof. Mathematics is all about finding patterns, and ZFC is powerful enough to be able to express, or rather deduce, (many of) these patterns.
What is deduction? Starting from our axioms, it's possible to find new valid propositions (tautologies), through the use of the rules of logic alone.
Looking at the connectives, in particular AND, biconditional and implication:
AND is used to "accumulate the knowledge we have": all theorems proven so far are implicitly linked by an AND (it's True that they are all True), and given a new theorem a that we have proven, we add it to the repertoire of proven theorems, i.e. our knowledge of mathematics. Let's call the original axioms of ZFC + any theorem ever proven, as linked together by the AND connective, our bag of knowledge.
Next is the biconditional: this is not used to "expand our knowledge", but rather to prove that a new proposition a is logically equivalent to one, or a set of propositions that we already know are True. It's like finding an alias: showing that a^b^c <-> d means we can replace with d every instance of a^b^c.
Now the beautiful one, the implication: this connective, if it holds, rules out the case in which p^¬q. When it is used between our bag of knowledge and a new proposition a we suppose is valid, and we prove that bag of knowledge -> a, this process can be interpreted as "refining" our knowledge. We create a new bag of knowledge_2, which is the same as bag of knowledge_1 but without the case in which ¬a, so it's more precise.
Is this framework correct so far? Few additional, final questions:
- Is it right to say that every new theorem (proposition) we will prove is either equivalent to an implication (to refine our knowledge), or a biconditional (to restate something we already know in a different form?)
- Is it right to say that the only atomic propositions in this system are the ones originally stated as axioms in ZFC, and every new proposition we could prove is a derived proposition, i.e. could be expressed as a compound statement (however complicated) of the atomic ones originally in ZFC?
- On the contrary, if a new proposition
athat we want to prove CANNOT be expressed as a compound statement of what we know so far, this proposition is "independent" of our theory ZFC (our original set of axioms), and thus unprovable?
