>tfw can't do Hilbert style proofs in propositional logic
Kill me now.
Can someone give me some tips? How do I "see" what sort of wffs to plug into the schema when doing a proof? Here's an example (> for if..then):
Prove that A > A
1. A > ((A > A) > A) /// instance of H1
2. (A > ((A > A) > A)) > ((A > (A > A)) > (A > A)) /// instance of H2
I'm not gonna type the rest of the proof, but you get the idea. How do I figure out that I need to substitute (A > A) for B? Whenever the texts show the proof in full, I can follow it no problem, I just cannot fathom how I'm supposed to figure out what to substitute into the schema.
Should I even bother learning axiomatic proofs when natural deduction exists?
>>7813432
bump for 90's powerpoint template
what is mp? are each of these statements "bar"d?
>>7813530
Modus ponens. Not sure what you mean by bar'd.
>>7813432
As a logician, formal proofs give logic a bad name.
No real mathematician cares about the formal proofs themselves. All that's important is that there is a sound and complete proof system. This is very important theoretically, and also finds application in computer-verified proofs.
Trying to formally prove something in a particular axiom system is absolutely tedious and unenlightening.
>>7813673
>Trying to formally prove something in a particular axiom system is absolutely tedious and unenlightening.
But it's fun. I just suck absolute dick at coming up with substitution instances and need help figuring out how to come up with useful ones.