Given a premise and ten axioms about a world with three shapes T, C, and D, how to prove that either all objects are T, all are C or all are D?

Question

I'd like to prove the following argument:

Premise: ∀x SameShape(x,c)

Conclusion: ∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x)

From the following axioms

The following axioms say that any object can be exactly one of the shapes: a Tet, a Cube, or a Dodec.

The following axioms tell us that if two objects x and y are the same shape then SameShape(x,y) is true, for each of the shapes Tet, Cube, and Dodec.

The following axioms tell us that if given two objects x and y we have SameShape(x,y) is true, and we know what the shape of one of the objects is, then we know the shape of the other object.

These axioms are all pretty clear and intuitively true.

The argument to be proved also seems pretty simple, but I am not sure about the exact steps.

Here is my first attempt:

Let c be any object.

Let d be any object.

From premise 1, we infer SameShape(c,d).

From Axiom 4, we infer Tet(c) | Cube(c) | Dodec(c).

Consider each case in this disjunction.

Case 1: Tet(c)

From Axiom 10 we infer Tet(d).

& Intro: Tet(c) & Tet(d)

| Intro: (Tet(d) & Tet(c)) | (Cube(d) & Cube(c)) | (Dodec(d) & Dodec(c))

Case 2: Cube(c)

From Axiom 8 we infer Cube(d)

& Intro: Cube(c) & Cube(d)

| Intro: (Tet(d) & Tet(c)) | (Cube(d) & Cube(c)) | (Dodec(d) & Dodec(c))

Case 3: Dodec(c)

From Axiom 9 we infer Dodec(d)

& Intro: Dodec(c) & Dodec(d)

| Intro: (Tet(d) & Tet(c)) | (Cube(d) & Cube(c)) | (Dodec(d) & Dodec(c))

| Elim (Tet(d) & Tet(c)) | (Cube(d) & Cube(c)) | (Dodec(d) & Dodec(c))

∀ Elim: ∀x (Tet(x) & Tet(c)) | (Cube(x) & Cube(c)) | (Dodec(x) & Dodec(c))

∀ Elim: ∀x ∀y (Tet(x) & Tet(y)) | (Cube(x) & Cube(y)) | (Dodec(x) & Dodec(y))

Which isn't the conclusion. Is this proof incorrect?

Alternatively, I could do the following

Let c be any object.

From Axiom 4, we infer Tet(c) | Cube(c) | Dodec(c).

Consider each case in this disjunction.

Case 1: Tet(c)

Let d be any object.

From premise 1, we infer SameShape(c,d).

From Axiom 10 we infer Tet(d).

& Intro: Tet(c) & Tet(d)

∀ Elim: ∀x Tet(x) & Tet(c)

The other two cases in the disjunction are analogous and result in:

∀x Cube(x) & Cube(c)

∀x Dodec(x) & Dodec(c)

We actually end each case with a disjunction introduction:

∀x (Cube(x) & Cube(c)) | ∀x (Tet(x) & Tet(c)) | ∀x (Dodec(x) & Dodec(c))

Therefore, by disjunction elimination we infer

∀x (Cube(x) & Cube(c)) | ∀x (Tet(x) & Tet(c)) | ∀x (Dodec(x) & Dodec(c))

Then, by ∀ Elim (from when we introduced the constant c):

∀x ∀y (Cube(x) & Cube(y)) | ∀x (Tet(x) & Tet(y)) | ∀x (Dodec(x) & Dodec(y))

This looks like it is correct, but it isn't in the form that we see in the original argument.

What is the inference rule that allows me to conclude that ∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x)?

Answer 1

I have two proofs for this, written pretty messily. Hopefully, you'll be able to make heads or tails of this.

---

Proof by Contradiction:

Assume not ∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x).

That translates to not ∀x Cube(x) & not ∀x Tet(x) & not ∀x Dodec(x) (by De Morgan's laws. I think you can take this as a given, but if not it's provable by contradiction).

From this, we get 3 existential statements: exists x not Cube(x), exists x not Tet(x), exists x not Dodec(x) (I think you might have to prove these with a further proof by contradiction in fitch, but they should be easy to do so from the previous step).

Now let us take an object 'a'. By axiom 4 it must be one of the three shapes. You will have to prove all three cases. I will only do the first.

Case 1: Cube(a). We know that exists x not Cube(x). Let that object be 'b'. Since it is an object, it must be one of the three shapes by (4). (You have to do three cases here again, I'm sorry)

However, by definition, it cannot be a cube.

Therefore, either Tet(b) or Dodec(b).

Take the first case. Object 'c' from the premise can either be a Cube, or not a Cube. If it is a cube, then 'b' contradicts the premise. If it is not a cube, then 'a' contradicts the premise.

No matter what we do, we get a contradiction. This will be true for all 3 cases of 'a'.

Therefore, we can introduce the universal quantifier, and conclude that for all x we get a contradiction. Since we have at least one object in the world -- 'c' -- that simplifies to simply being a contradiction.

Since we've proven that the assumption results in a contradiction, we have proven our original conclusion.

---

Direct Proof:

Let us take some arbitrary object 'a' in the world. By axiom 4, we know that it must be one of the three shapes.

Let us suppose that it is a cube. If it is a cube, then by 8, 'c' must be a cube as well. Let's take another arbitrary object in the world 'b'. Since 'c' is a cube, 'b' must be a cube as well. Therefore, we can conclude ∀x Cube(x). Since we can always introduce a disjunction, we can form ∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x). You can do similarly for the other two shapes as well and get the same conclusion.

Therefore, since you chose an arbitrary object 'a', ∀y(∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x)). Applying 'c' to that statement, we can conclude that ∀x Cube(x) | ∀x Tet(x) | ∀x Dodec(x).