e.g.0:
A or not A is a theorem
Proof:
if not ( A or not A ):
not( A or not A ). [If-sub]
if A:
not( A or not A ). [if-repeat]
A. [If-sub]
A or not A. [or-create]
not A. [contradiction]
A or not A. [or-create]
not not( A or not A). [contradiction]
A or not A. [not-destroy]
e.g.1:
Q := A or ( A => B ) [short-hand]
Q is a theorem
Proof:
If not Q:
If A:
If not B:
Q.
not Q.
not not B.
B.
A => B.
Q.
not not Q.
Q.
@bat_of_doom Roughly, the idea is to show that you can construct a proof based on the fact that the tautology is true for every truth assignment of its atoms.
And to construct the proof one way (as I chose in the linked conversation) is to first use LEM (separately proven) for each atom to repeatedly split cases for all the atoms involved, and then inside each case construct a subproof.
And constructing the subproof is recursive, or as I presented it via structural induction on the propositions.
@bat_of_doom: The key structural induction is here:
I studied a bit of logic in my discrete mathematics course. It just covered the basics. I was always interested to study further, but there is no course in my department (mathematics) that covers logic. The closest thing that exists is a course in logic for computer science from the C.S. department. However I never did that as I suspected it would be mostly application based and won't cover much theory.
@LastIronStar Not quite. I am pursuing a BTech degree in mathematics and computing. Though it does cover some of the theoretical part of C.S., most of the electronics courses are replaced with mathematics courses like analysis, func. analysis, algebra, etc.
