Can I justify removing a universal quantifier in this proof?

Question

I am trying to prove that the connex property implies reflexivity.

$\vdash (\forall x,\forall y : (xRy \lor yRx)) \Rightarrow (\forall x : xRx)$

Here is my attempt

\begin{align*} &~~~~~(1)~~(\forall x,\forall y : (xRy \lor yRx))\\ &~~~~~~~~~~~\text{\{Justification ?? \}} \\ &\Rightarrow(2)~~(\forall x : (xRx \lor xRx)) \\ &~~~~~~~~~~~\text{\{ Idempotency of disjunction in (2) \}}\\ &\equiv (3)\forall x : (x R x)\\ \end{align*} I am stuck for a justification between steps (1) and (2). The step seems intuitively valid. Do I need a sub-proof or is there some general rule that permits this step?

Answer 1

Your error is that you're trying to prove that the conclusion is equivalent to the premise, whereas you're actually just asked to prove that it follows from the premise.

In a typical formal proof system (here natural deduction) this can be done by almost what you're doing, except without the spurious $\equiv$ signs.

1. Assume $\forall x \forall y (xRy \lor yRx)$.
2. Universal instantiation, setting $x=x$, gives $\forall y (xRy \lor yRx)$.
3. Universal instantiation, setting $y=x$, gives $xRx\lor xRx$.
4. Propositional equivalece gives $xRx$.
5. Universal generalization gives $\forall x(xRx)$.
6. Discharge the assumption from step 1, giving $\forall x\forall y (xRy\lor yRx)\to \forall x(xRx)$.

Answer 2

You can't justify the passage from $(1)$ to $(2)$. Let $R$ be the equality relation in a set with more than one element. Then $(1)$ is false (that is, there are distinct elements), whereas $(2)$ holds (each element is equal to itself).

Going from $(2)$ to $(3)$ is correct, since $P\vee P\iff P$.

Answer 3

Your attempt fails, because you try to prove the equality, not implication.

$$\forall x\in X \forall y\in X :(xRy \vee yRx)$$ $$\Rightarrow \forall x\in X \exists y=x\in X :(xRy \vee yRx)$$ $$\Rightarrow \forall x\in X :(xRx \vee xRx)$$ $$\Rightarrow \forall x\in X :(xRx )$$

Answer 4

$\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2 \end{array}}\def\R{\operatorname{R}}$The justification is that: if a predicate is true for any $(x,y)$, then it is true for any $(x,x)$.

Should idempotence be a theorem you may use that; alternatively it may quickly be proven with disjunction elimination.

$$\fitch{}{\fitch{\forall x\forall y:x\R y\vee y\R x }{\fitch{[a]}{\forall y:a\R y\vee y\R a\\a\R a\vee a\R a\\\fitch{a\R a}{}\\a\R a\to a\R a\\a\R a}\\\forall x: x\R x} &\raise{12ex}{\textsf{Assumption}\\[0.5ex] \textsf{Arbitrary Witness}\\[0.5ex]\textsf{Universal Elimination}\\[0.75ex]\textsf{Universal Elimination}\\[0.75ex]\textsf{Assumption}\\[1ex]\textsf{Conditional Introduction}\\[1ex]\textsf{Disjunction Elimination}\\[2ex]\textsf{Universal Introduction}}\\ (\forall x\forall y:x\R y\vee y\R x)\to(\forall x:x\R x)& \textsf{Conditional Introduction}}$$