[Boards: 3 / a / aco / adv / an / asp / b / bant / biz / c / can / cgl / ck / cm / co / cock / d / diy / e / fa / fap / fit / fitlit / g / gd / gif / h / hc / his / hm / hr / i / ic / int / jp / k / lgbt / lit / m / mlp / mlpol / mo / mtv / mu / n / news / o / out / outsoc / p / po / pol / qa / qst / r / r9k / s / s4s / sci / soc / sp / spa / t / tg / toy / trash / trv / tv / u / v / vg / vint / vip / vp / vr / w / wg / wsg / wsr / x / y ] [Search | Free Show | Home]

>tfw can't do Hilbert style proofs in propositional logic

This is a blue board which means that it's for everybody (Safe For Work content only). If you see any adult content, please report it.

Thread replies: 6
Thread images: 1

>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.
Thread posts: 6
Thread images: 1


[Boards: 3 / a / aco / adv / an / asp / b / bant / biz / c / can / cgl / ck / cm / co / cock / d / diy / e / fa / fap / fit / fitlit / g / gd / gif / h / hc / his / hm / hr / i / ic / int / jp / k / lgbt / lit / m / mlp / mlpol / mo / mtv / mu / n / news / o / out / outsoc / p / po / pol / qa / qst / r / r9k / s / s4s / sci / soc / sp / spa / t / tg / toy / trash / trv / tv / u / v / vg / vint / vip / vp / vr / w / wg / wsg / wsr / x / y] [Search | Top | Home]

I'm aware that Imgur.com will stop allowing adult images since 15th of May. I'm taking actions to backup as much data as possible.
Read more on this topic here - https://archived.moe/talk/thread/1694/


If you need a post removed click on it's [Report] button and follow the instruction.
DMCA Content Takedown via dmca.com
All images are hosted on imgur.com.
If you like this website please support us by donating with Bitcoins at 16mKtbZiwW52BLkibtCr8jUg2KVUMTxVQ5
All trademarks and copyrights on this page are owned by their respective parties.
Images uploaded are the responsibility of the Poster. Comments are owned by the Poster.
This is a 4chan archive - all of the content originated from that site.
This means that RandomArchive shows their content, archived.
If you need information for a Poster - contact them.