propositional proof

[chrislav]

Given the following equivalence :

[(p^q)=>r] <=>[p=>(q=>r)]

Can we prove it formaly without using the law of conditional proof (deduction theorem)?

 

[Steven G]

Try it yourself and post back your work

 

[logistic_guy]

Try it yourself and post back your work

I have been on this forum for just over 10 years and have decided to not be a helper anymore as long as this logistic_guy is still around. I enjoyed my time here, but as I said it's time to say goodbye.
Steven

You are a liar as I am still here.

 

[chrislav]

i think that there is not another solution except that where we use the conditional proof.
I tried.

 

[blamocur]

I can't think of a simpler solution than building truth tables for both sides.

 

[Aion]

Given the following equivalence :

[(p^q)=>r] <=>[p=>(q=>r)]

Can we prove it formaly without using the law of conditional proof (deduction theorem)?

You can also prove it purely by equivalence transformations (no conditional proof). Use only the truth-functional laws for [imath]\to,\neg,\land,\lor[/imath].

 

[xamidi]

This thread bothered me so much that I registered in order to make this reply.

I can't think of a simpler solution than building truth tables for both sides.

The request is to "prove formally". A truth table is no formal proof.
Here's some good read about this (and more): https://www.hedonisticlearning.com/posts/the-pedagogy-of-logic-a-rant.html

Given the following equivalence :

[(p^q)=>r] <=>[p=>(q=>r)]

Can we prove it formaly without using the law of conditional proof (deduction theorem)?

You, and apparently everyone so far in this thread, seem not to know what a formal proof is.
Otherwise, the absence of rules and axioms of the proof system you're supposed to use would've been marked as a major issue.
I encourage everyone wishing to learn the basics of formal logic to read the article I linked above.

I'll add a few basics and search results.

1) Formal logic is not concerned with meaning but form, i.e. the shape/structure, which is exactly what makes a formula.
For example, your "[(p^q)=>r] <=>[p=>(q=>r)]", which logicians would rather denote "((p∧q)→r)↔(p→(q→r))" or "ECKpqrCpCqr" (Polish notation ; well-googleable), is simply the following abstract tree (in this case called a syntax tree).


2) There are several kinds of formal proof systems, most popular (a) Hilbert systems, (b) Natural deduction, and (c) Sequent calculi.
And for each of these types there are infinitely many different systems that work according to propositional logic and are thus able to prove the above formula.
It doesn't make sense for us to guess which system you are using. If the question was so broad that you may choose any popular* system of propositional logic by yourself (which you should've mentioned in that case), then I'd suggest using something very easy, like this natural deduction calculus . (web tool, exemplary proof).

*Something like that.. to avoid the possibility of designing a system in which the target theorem is super easy to prove.

3) Your language apparently supports at least three different operators (∧, →, and ↔), all of which must either be defined by some inference rules and/or axioms, or there must be aliases, like "p∧q is shorthand for ¬(p→¬q)". For example, under {→,¬}-pure languages, your formula would be an alias of "¬(((¬(p→¬q)→r)→(p→(q→r)))→¬((p→(q→r))→(¬(p→¬q)→r)))" (I have a tool which calculated this for me. I personally deal with {→,¬}-pure Hilbert systems when it comes to propositional logic.)

4) I searched Metamath's database "set.mm" for your formula, and it turns out they have proven it with modus ponens from three axioms (CpCqp,CCpCqrCCpqCpr,CCNpNqCqp) (a widespread Hilbert system, which I call "Frege's calculus simplified by Łukasiewicz" for historical reasons), but Metamath additionally used what they call "definitions", which are in fact two more axioms (NCCEpqNCCpqNCqpNCNCCpqNCqpEpq,EKpqNCpNq) that introduce (↔,∧).
They called the theorem impexp (click this link to browse their proof).
It is generally called the import-export theorem.

5) I searched in Metamath's pmproofs.txt (which is a {→,¬}-pure proof database optimized for short derivations) with the corresponding syntax "((P ^ Q) -> R) <-> (P -> (Q -> R))", and interestingly the import-export-theorem is not given there, but it makes a subformula of another theorem (*4.87).

 

[Agent Smith]

It's an equivalence rule in natural deduction.
If you kiss the girl and she smiles then that's love <=> If you kiss the girl then if the girl smiles then that's love.

Intuitive proof