Line $K$ is parallel to line $U$, and line $L$ intersects line $K$ at point $P$. Show $L \nparallel U$.

Question

Working on the book: Lang, Serge & Murrow, Gene. "Geometry - Second Edition" (p. 18)

6. In Figure 1.11, line $K$ is parallel to line $U$, and line $L$ intersects line $K$ at point $P$. What can you conclude about lines $L$ and $U$? Why?

PAR 2. Given a line $L$ and a point $P$, there is one and only one line passing through $P$, parallel to $L$.

Conclusion: $L \nparallel U$

Proof (using Fitch-style natural deduction):

I will assume $L \mathbb{\parallel} U$ and reach a contradiction.

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

$ \fitch{1.\,K \parallel U\\ 2.\,K \neq L\\ 3.\,P \in L \land P \in K\\ 4.\,\exists!l(P\in l \land l \parallel U) \qquad \text{[PAR 2]} }{ \fitch{5.\,L \parallel U}{ \fitch{6.\,P \in l_0 \land l \parallel U}{ \vdots\\ }\\ k.\,\bot }\\ m.\,L \nparallel U } $

The point of this proof is showing that is not possible that there are two lines parallel to line $U$ passing through point $P$. I have a problem on line 6 when I need to make a substitution instance of PAR 2. The variable used (where I wrote $l_0$) need to be "fresh", i.e. not appear in any undischarged assumptions.

How can I overcome that problem and continue the proof ?

P.D.: rules of inference can be found in Appendix C of this book: http://forallx.openlogicproject.org/forallxyyc.pdf

Answer 1

Sketch of a proof

We have Parallel axioms.

We have Premises:

1. $P \in K$,
2. $P \in L$,
3. $K \parallel U$.

We have to prove that: either $L=K$ or $L \nparallel U$, i.e. :

$L \ne K \to L \nparallel U$.

Thus, assume:

4. $L \ne K$

and assume for contradiction:

5. $L \parallel U$.

Now we have to unwind the parallel axiom: $\forall u \forall P \exists ! l (P \in l \land l \parallel u)$ [omitting for simplicity the additional constraint: $P \notin u)$]:

$\exists l [(P \in l \land l \parallel U) \land \forall l' ((P \in l' \land l' \parallel U) \to l'=l)]$.

Your strategy of using $\exists$-elim is correct; we will use a fresh variable $Z$ to get:

$(P \in Z \land Z \parallel U) \land \forall l' ((P \in l' \land l' \parallel U) \to l'=Z)$, from which:

$\forall l' ((P \in l' \land l' \parallel U) \to l'=Z)$.

We have to instantiate it twice, with $K$ and $L$ respectively to have:

$K=Z$, from 1) and 3), as well as:

$L=Z$, from 2) and 5).

Using transitivity of equality, we get:

$L=K$.

In it, the variable $Z$ does not occur; thus we may close the $\exists$-elim subproof concluding with: $L=K$.

This contradicts 4) and we can conclude by $\lnot$-intro discharging assumption 5):

$L \nparallel U$.