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

  1. 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?

enter image description here

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

  • $\begingroup$ But the fifth axiom was a different sort of statement: 5. If two straight lines in a plane are met by another line, and if the sum of the internal angles on one side is less than two right angles, then the straight lines will meet if extended sufficiently on the side on which the sum of the angles is less than two right angles.Because this axiom was much more complicated than the previous axioms, it seemed more like a theorem than a self-evident proposition. Since all attempts to deduce it from the first four axioms had failed, Euclid simply included it as an axiom because he $\endgroup$
    – Moti
    Commented Jul 2, 2020 at 5:46
  • $\begingroup$ knew he needed it. For example, some axiom like this one was necessary for proving one of Euclid's most famous theorems, that the sum of the angles of a triangle is 180 degrees. Mathematicians found alternate forms of the axiom that were easier to state, for example: $\endgroup$
    – Moti
    Commented Jul 2, 2020 at 5:48
  • $\begingroup$ 5'. For any given point not on a given line, there is exactly one line through the point that does not meet the given line. $\endgroup$
    – Moti
    Commented Jul 2, 2020 at 5:48
  • $\begingroup$ math.brown.edu/~banchoff/Beyond3d/chapter9/section01.html $\endgroup$
    – Moti
    Commented Jul 2, 2020 at 5:48
  • $\begingroup$ Thank you, @Moti. I will check the link you provided. $\endgroup$
    – F. Zer
    Commented Jul 2, 2020 at 13:22

1 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:

  1. $L \ne K$

and assume for contradiction:

  1. $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:


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$.

  • $\begingroup$ This is amazing. I cannot thank you enough, @Mauro ALLEGRANZA. $\endgroup$
    – F. Zer
    Commented Jul 2, 2020 at 13:19
  • $\begingroup$ Could you clarify two things ? What's the additional constraint $P \notin u$? Why do I need to prove either $L=K$ or $L \nparallel U$ ? Perhaps, I am missing something obvious. $\endgroup$
    – F. Zer
    Commented Jul 2, 2020 at 13:21
  • 1
    $\begingroup$ @F.Zer - if $P \in U$, then there is no parallel to $U$ different from $U$. $\endgroup$ Commented Jul 2, 2020 at 13:30
  • $\begingroup$ Perfect. All clear, now. Thank you. $\endgroup$
    – F. Zer
    Commented Jul 2, 2020 at 13:40
  • 1
    $\begingroup$ the problem says "line L intersects line K at point P. What can you conclude about lines L and U?" Either $L = K$ or not. If $L=K$, then $L \parallel U$. If $L ≠ K$, then, due to the uniqueness of parallel, then $L \nparallel U$. $\endgroup$ Commented Jul 2, 2020 at 13:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .