[Boards: 3 / a / aco / adv / an / asp / b / biz / c / cgl / ck / cm / co / d / diy / e / fa / fit / g / gd / gif / h / hc / his / hm / hr / i / ic / int / jp / k / lgbt / lit / m / mlp / mu / n / news / o / out / p / po / pol / qa / qst / r / r9k / s / s4s / sci / soc / sp / t / tg / toy / trash / trv / tv / u / v / vg / vip /vp / vr / w / wg / wsg / wsr / x / y ] [Search | Home]
>tfw can't do Hilbert style proofs...
If images are not shown try to refresh the page. If you like this website, please disable any AdBlock software!

You are currently reading a thread in /sci/ - Science & Math

>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.