0
$\begingroup$

For at least four disjuncts. For example, it should follow immediately that any two disjunctions of seven formulas are equivalent. There are 132 cases to check without this general result.

Prove using axioms, rules of inference, theorems of first-order logic. You may assume that disjunction is commutative and associative.

$\endgroup$
  • $\begingroup$ The proof must be general, i.e. for $n$ disjuncts whatever and must be by induction, and thus in the meta-theory. Of course, it must rely on the basis cases, i.e. $A \lor B \equiv B \lor A$ and $(A \lor B) \lor C \equiv A \lor (B \lor C)$. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '18 at 7:24
  • $\begingroup$ The last ones can be axioms of the calculus or tehy are easily derivable from propositional calculus; of courese, the details depend on thechosen axiomatization. $\endgroup$ – Mauro ALLEGRANZA Apr 23 '18 at 7:25
1
$\begingroup$

Probably the best way of getting at this problem is to prove that disjunction is associative (so that the parentheses no longer matter) and that it is commutative (so that the order no longer matters). If you have those two properties, then you can simply place any of your disjunctions in increasing order by index to check equivalence.

EDIT: The original statement has been edited, so there are no longer indices to order by, but I think the spirit of the solution is clear.

EDIT 2: As per one of my comments, see this post as to why I think this problem is impossible as stated: Why can't we quantify over propositional functions/open formulas in first order languages?

$\endgroup$
  • $\begingroup$ Not what I'm looking for. See edit. I'm looking for a formal proof. $\endgroup$ – Randy Randerson Mar 25 '18 at 9:24
  • $\begingroup$ @RandyRanderson This is the formal proof; if a binary operation is associative then it is actually generally associative (that is to say that for any number of terms it does not matter where the parentheses are), and if it is commutative and generally associative then you can place the terms in any order. $\endgroup$ – Valborg Mar 25 '18 at 9:27
  • $\begingroup$ This is hand-waving, not a formal proof. It is intuitively obvious but I don't see how you would (for example) translate it into first-order language. $\endgroup$ – Randy Randerson Mar 25 '18 at 9:35
  • 2
    $\begingroup$ @RandyRanderson I think then you might run into problems. First order logic can't quantify over logical objects, like formulae (in this case the disjunctions we care about), so I doubt that you will get a formal proof using only first order logic that first order logical disjunctions are independent of their representations. I could be wrong, so if someone out there knows better than I they are welcome to post an answer. $\endgroup$ – Valborg Mar 25 '18 at 9:49
  • 1
    $\begingroup$ @RandyRanderson Valborg is right: you are asked to prove a result about logic statements; you cannot prove that within a formal proof system that uses those very expressions, but you need some kind of 'meta-proof' $\endgroup$ – Bram28 Mar 25 '18 at 11:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.