Working on the book: Lang, Serge & Murrow, Gene. "Geometry - Second Edition" (p. 18)
- 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