Propositions and Proofs "not propositions"

[lovettchris]

I don't like your examples of what is not a proposition. Everything you list there could be made into legal Lean proposition given the right declaration of types that can describe those things, for example:

inductive City
| London
| Paris
| NewYork
| Woodinville
| Tokyo
| Springwood
| Beijing

def isBig : City → Bool
| City.London => true
| City.Paris => true
| City.NewYork => true
| City.Woodinville => false
| City.Tokyo => true
| City.Springwood => false
| City.Beijing => true

def cityToNat : City → Nat
| City.London => 1
| City.Paris => 2
| City.NewYork => 3
| City.Woodinville => 4
| City.Tokyo => 5
| City.Springwood => 6
| City.Beijing => 7

def isPrime (i : Nat) := i > 1 ∧ ∀ j, j > 1 ∧ j < i → ¬ (i % j = 0)

theorem BigCitiesArePrime (c : City) : (isPrime (cityToNat c)) ∧ (isBig c) := by
  ...

So perhaps you should instead list terms that are not in the proposition format like "6 + 9" is not a proposition because it cannot be turned into a boolean value?

[david-christiansen]

These sentences are intended to be English sentences, rather than formal mathematical statements in Lean, which is why they're not in code font. The idea is that the three sentences are not even false because they make no sense whatsoever - there's no point asking if they're true because they are just nonsense. Cf. "Das ist nicht nur nicht richtig; es ist nicht einmal falsch!", supposedly uttered by Pauli.

It's certainly the case that we can redefine terms to make wrong or even nonsense things be accepted by the computer. For example, I could shadow the definition of Int as follows:

inductive Int where
  | one | two | lots

I could then prove all sorts of false things, like "there exist exactly three integers", because my definition was wrong and did not actually capture the mathematical idea that I was thinking about. Similarly, while it really doesn't make sense to add a Boolean to a pair of strings, I can go ahead and write some silly instance like:

instance : HAdd Bool (String × String) Unit where
  hAdd _ _ := Unit.unit

That doesn't mean I've captured any meaningful notion of addition, however.

The kinds of things in those three sentences are actually type errors if I were to translate them into Lean, which cause the resulting statement to not even be a Prop.

I'll try to modify the sentence to make it clear that they're "not even wrong".