Yes. Given every tautology, it has finitely many atoms, and we can construct the case splitting for those atoms, and then all we need to show is that we can prove that tautology in each case.
@LastIronStar There is no context involved in the definition of a tautology.
Remember we defined the semantics of each boolean operation by saying for example that "A or B" is true if "A" is true or "B" is true and is false otherwise.
So we can talk about the truth value of any propositional sentence given the truth-values assigned to the atoms.
We need to show that the tautology can be proven. This is where we invoke structural induction. Let P be the property on propositions that if it is true in that case then it is provable in that case.
was simply a natural attempt to get what we wanted.
Because we already know that a tautology is supposed to be true no matter what truth values are assigned to its atoms. So it is supposed to be true in every context.
First observe that P is satisfied by every proposition of size 0, because it is just some atom A. If it is true in that case then that case is governed by some context-header "If A:", so of course we can prove it. If it is false in that case then that case is governed by some context-header "If not A:", so we can prove "not A".
So the base case works.
Next consider any proposition Z with at least one boolean operation. Z will have one main/final boolean operation, and hence is of the form "not X" or "X or Y" or "X and Y" or "X implies Y" for some propositions X,Y. Note that X,Y are both smaller than Z.
By structural induction we can assume that X,Y both satisfy P to show that Z satisfies P.
Okay so far?
Let's just use C to denote that case (in the proof we wish to construct) that we are looking at now.
If Z is of the form "not X" then... If Z is true in C then X is false in C and hence "not X" is provable in C. If Z is false in C then X is true in C and hence provable in C, and so we can insert the following proof after that (within C):
If Z is of the form "X and Y" then... If Z is true in C then "X" and "Y" are both true in C and hence provable in C, and so of course we can prove "X and Y" in C in 1 extra step (And-Intro). If Z is false in C then either "X" or "Y" is false in C and hence either "not X" or "not Y" is provable in C. By symmetry it suffices to deal with the first possibility. Write the following (within C):
Remember we defined the semantics of each boolean operation by saying for example that "A or B" is true if "A" is true or "B" is true and is false otherwise.
The definition of tautology only makes sense after we have defined the semantics for each boolean operation.
Great! Now on to "or", which is similar but just a little longer.
If Z is of the form "X or Y" then... If Z is true in C then either "X" or "Y" is true in C and hence provable in C, and so of course we can prove "X or Y" in C in 1 extra step (Or-Intro). If Z is false in C then both "X" and "Y" are false in C and hence both "not X" and "not Y" are provable in C. Write the following (within C):
...
not A.
...
not B.
If A or B:
If A:
not A.
false.
If B:
not B.
false.
false.
not ( A or B ).
Here I used "false", which I know you don't like. It gives a taste of why it is very useful. Here is what the proof would look like if we couldn't use "false":
...
not A.
...
not B.
If A or B:
If A:
If A or B:
A.
not A.
not ( A or B ).
If B:
If A or B:
B.
not B.
not ( A or B ).
not ( A or B ).
not ( A or B ).
Okay with this one? Only one left to go after this.
If Z is of the form "X implies Y" then... If Z is true in C then either "X" is false in C or "Y" is true in C. For the former we would have "not X" provable in C so write the following proof:
...
not X.
If X:
If not Y:
X.
not X.
not not Y.
Y.
X implies Y.
For the latter we would have "Y" is provable in C so write the following proof:
...
Y.
If X:
Y.
X implies Y.
Finally, if Z is false in C then "X" is true in C but "Y" is false in C. So "X" and "not Y" are provable in C so write the following proof:
...
X.
...
not Y.
If X implies Y:
X.
Y.
not Y.
not ( X implies Y ).
Therefore Z satisfies P.
We're done! You may be curious to check that in the above subproofs we have utilized all the rules in our deductive system. This is no coincidence, because none of them are redundant. But it will be too difficult and tedious for me to prove this curious fact!
Also, I kept accidentally saying "write the following proof" when I should just say "write the following (within C)".
Because I'm used to thinking about those inner portions as subproofs, but technically it conflicts with how I defined "proof". =)
Great job! You understood the semantic-completeness theorem for propositional logic. This means you know why the deductive system is sufficiently powerful to prove every (propositional) tautology.
And it's nearly time for me to go. Any last questions for now? =)
@LastIronStar Saw a comment of yours regarding scouting books besides boolos. I actually have boolos' computability and logic and I quite like it. Would most definitely reccomend
The Tennenbaum phenomenon is amazing, and that is totally correct, but let me give a direct proof using the idea of computable inseparability.
Theorem. There is no computable model of ZFC.
Proof: Suppose to the contrary that M is a computable model of ZFC. That is, we assume that the underlying...
