proving something is false

Stream: new members

[rzeta0]

I haven't got to the point in "The Mechanics of Proof" that might deal with this, but I'm curious...

If I wanted to prove $a \neq c$, is it sufficient to write a Lean program to prove $a = c$ and observe that Lean throws an error - as long as that error is about the logic of the proof, and not a syntax error?

---

An actual example:

Given the following facts

$$\begin{align} a&>b\\b&=c\\c&\geq d \end{align}$$

I want to prove $a \not \geq d$.

How do I do this in Lean?

[Jireh Loreaux]

assuming you meant ¬ (a ≤ d) instead of ¬ (a ≥ d), you could do it like this:

import Mathlib

example {a b c d : ℝ} (hab : a > b) (hbc : b = c) (hcd : c ≥ d) : ¬ (a ≤ d) := by
  rw [not_le]
  calc
    d ≤ c := hcd
    _ = b := hbc.symm
    _ < a := hab

[Jireh Loreaux]

or if you feel like :golf: :

example {a b c d : ℝ} (hab : a > b) (hbc : b = c) (hcd : c ≥ d) : ¬ (a ≤ d) :=
  not_le_of_gt <| (hbc ▸ hcd).trans_lt hab

[Kyle Miller]

Or

example {a b c d : ℝ} (hab : a > b) (hbc : b = c) (hcd : c ≥ d) : ¬ (a ≤ d) := by
  linarith

[Kyle Miller]

observe that Lean throws an error

No, there are no errors being thrown in contradiction proofs. The key is that once you manage to reach a contradiction, you can use the "principle of explosion" to prove whatever you want (including False, which has no proof).

An intermediate step in the linarith proof is doing intro, which works here because logical negation is encoded as "implies False". What the linarith tactic does is to show that these hypotheses are contradictory, and thus able to prove False.

example {a b c d : ℝ} (hab : a > b) (hbc : b = c) (hcd : c ≥ d) : ¬ (a ≤ d) := by
  intro
  /-
  a b c d : ℝ
  hab : a > b
  hbc : b = c
  hcd : c ≥ d
  a✝ : a ≤ d
  ⊢ False
  -/
  linarith

[Jireh Loreaux]

Kyle Miller said:

(including False, which has no proof).

Maybe you mean to say "which has no constructor"? I know what you mean of course, you can't prove example : False := sorry, but example : False → False := id works, and False.elim can be used to give proofs where the goal is False, as you mention.

[Kyle Miller]

I mean that the type False is not inhabited. I'm not sure how technically precise to be here, given that the context is The Mechanics of Proof, which I'm not sure introduces inductive types or constructors until chapter 8.

[Henrik Böving]

The correct way to spell consistency for a type theory is to say that there is no inhabitant of the empty type in the empty context. Or a bit less technical "there is no proof of False in the empty context"

[Ted Hwa]

If I wanted to prove $a \ne c$, is it sufficient to write a Lean program to prove a=c and observe that Lean throws an error - as long as that error is about the logic of the proof, and not a syntax error?

No. Observing that Lean throws an error only means that your proof is wrong, not that the statement is wrong.

[Mark Fischer]

Henrik Böving said:

"there is no proof of False in the empty context"

:)

I naturally tend to think of something like the contrapositive version of this:

"A proof of False is possible only in an inconsistent context." - maybe all of Lean is inconsistent (you've chosen your axioms poorly, or there's a bug in the system somewhere), or Lean is consistent and your local assumptions are inconsistent in which case you should never be able to cash out any implications derived from this context as it should be impossible to supply the antecedent.

¬P being defined as P → False took me a quick moment to really understand when I first started, but I now really like it.

[Mario Carneiro]

"A proof of False is possible only in an inconsistent context." - maybe all of Lean is inconsistent (you've chosen your axioms poorly, or there's a bug in the system somewhere), or Lean is consistent and your local assumptions are inconsistent in which case you should never be able to cash out any implications derived from this context as it should be impossible to supply the antecedent.

With that definition, it becomes a tautology. What is an inconsistent context (broadly construed) if not one in which you can prove False?

[Mark Fischer]

Mario Carneiro said:

With that definition, it becomes a tautology.

I don't think so, though maybe you're right and my thinking is confused. I seems that in a broader context, you can show me any contradiction and I'd be convinced you have an inconsistent context. My first logic classes didn't have True and False as propositions, so you'd get to something like P ∧ ¬P ⊢ ⊥ directly from a law of non-contradiction.

Also - I may have a context and not know for certain whether it is consistent or not. Hmmmm, yeah, I'm not really sure how to reword that so it's less tautological.

[Mario Carneiro]

The point of consistency is that the empty context is consistent, or that there exists a consistent context. So I think the sentence should really have "empty context" and not "consistent context" because they aren't a priori the same and the difference is exactly consistency of the system

[Mark Fischer]

This is sort of digging into the weeds, but isn't it that for a system like Lean's, you really can't "know" there exists a consistent context.

To me, the thing worth capturing about a proof of False isn't that you suddenly know your context isn't empty (Which I think is something we just have to assume is true to move on with our lives and do more interesting things). But more specifically, something like "there's something about your assumptions such that they could never all be true or you you could never arrive in such a state from the empty context" or something like that.

[Mario Carneiro]

Of course we don't "discover the context isn't empty", this is a trivial syntactic condition we can easily determine up front

[Mario Carneiro]

if there are no assumptions then there is no way to blame them for a proof of false

[Mario Carneiro]

and P ∧ ¬P ⊢ ⊥ isn't a proof in the empty context

[Mario Carneiro]

Mark Fischer said:

This is sort of digging into the weeds, but isn't it that for a system like Lean's, you really can't "know" there exists a consistent context.

This depends on your standards of knowledge. If know is synonymous with "can prove in lean" then no we can't know it, but there is a relative consistency proof wrt ZFC with some inaccessible cardinals, and so if you believe that models of the latter exist then you can say things like "there is no proof of false in the empty context" with confidence.

In fact, even if you aren't sure about the latter, there is a "social" reason for lean (and math for that matter) to be consistent, which is that if an inconsistency was found it would be considered a bug in the axioms or implementation etc and it would be fixed until no inconsistency remains. So long term we would expect "there is no known inconsistency" to be a robust situation in mathematics, which self-corrects to ensure it remains the case.

[Mark Fischer]

We may be talking past each other a bit. Which is likely on me

Sure, the common sense way to know whether your context is empty is to just look at it. If I lost my glasses and everything was blurry, but I could somehow make out that there's a proof of False - one thing I should be pretty confident about is that the context isn't empty. Given your point that an empty context and an inconsistent context aren't a priori the same thing, if I put my glasses back on to discovery the context was empty, I'd now also know the system is inconsistent (there's a bug to fix).

I'm happy with the social reason for both Lean and Math at large. I love learning about foundations, but I'm generally not existential about the possibility that everything is based on inconsistent axioms. To be honest, I didn't mean to make my point in this thread about this at all.

The thing that I think (and this is entirely my opinion) is cool/interesting/worth noting in constructive logic or Calculus of Inductive Constructions is that as a beginner, running into a situation where you can prove False should feel interesting and significant. For me at least, when first learning Lean, seeing why False.elim doesn't break everything takes a moment. I don't think it's as straight forward as many of the intro and elim rules. Does that make sense?