De Morgan's

Stream: general

[Ken Lee]

Just proved $\neg (P \lor Q ) \iff \neg P \land \neg Q$ and $\neg P \lor \neg Q \to \neg (P \land Q)$ in Lean. I don't see why the converse would require classical logic though. Can someone please explain?

[Ken Lee]

Just proved $$\not (P \and Q ) \iff \not P \and \not Q$$ and $$\not P \or \not Q \to \not (P \and Q)$$ in Lean. I don't see why the converse would require classical logic though. Can someone please explain?

Oh no. It didn't format the inline maths.

[Kenny Lau]

$\neg (P \land Q ) \iff \neg P \land \neg Q$ and $\neg P \lor \neg Q \to \neg (P \land Q)$

[Kenny Lau]

\neg (P \land Q ) \iff \neg P \land \neg Q$$ and $$\neg P \lor \neg Q \to \neg (P \land Q)

[Ken Lee]

$\neg (P \land Q ) \iff \neg P \land \neg Q$ and $\neg P \lor \neg Q \to \neg (P \land Q)$

Thanks!

[Jean Lo]

related question: more generally, how does one go about determining whether a proof can be done constructively?

[Chris Hughes]

If it implies excluded middle then it can't be done constructively. There's an exercise somewhere proving a whole load of things imply excluded middle.

[Kenny Lau]

but that is not necessary.

[Kenny Lau]

you can't check every Kripke model though... is there some finite subset that we can check

[Mario Carneiro]

there is a completeness result that says any intuitionistically invalid statement is false on a finite kripke model

[Kenny Lau]

that makes set of intuitionstically valid theorems a Π1 set, thus a Δ1 set?

[Mario Carneiro]

yes, so it is decidable

[Kevin Buzzard]

@Jean Lo Here is a basic strategy for checking that various simple things can't be done constructively. First observe that all the rules of constructive logic apply when "truth values" are...something like...open sets in a topological space (I hope I remembered this right). You model "not" as "interior of the complement" and "implies" as "is a subset of". Then some stuff like "P or not P" simply isn't true in this interpretation, because the union of an open set and the interior of its complement might not be the whole space.

[Kenny Lau]

does this together with the 14-theorem give you a fast(er) way of determining stuff?

[Kenny Lau]

https://en.wikipedia.org/wiki/Kuratowski%27s_closure-complement_problem

[Mario Carneiro]

It's not complete, unfortunately

[Mario Carneiro]

at least not unless you consider all topologies

[Kevin Buzzard]

I don't know, but I don't know what a Kripke model is and yet I've used this way of thinking about things to convince myself that certain propositions can't be proved in classical logic and basically it's the only way I know to do such a thing.

[Kenny Lau]

just consider the Kuratowski algebra?

[Mario Carneiro]

A Kripke model is based on a kind of epistemological interpretation of the formulas. There are a bunch of points called "worlds", and at each point there are things that are known to be true at that world, but the things that are not known to be true are just unknowns. There is a "in the future" accessibility relation to other worlds where more things may be known (but previously known things are still known), and things are known to be false only if they are never known in the future

[Kenny Lau]

I don't think Kevin cares

[Mario Carneiro]

For example, suppose we have time 0 and time 1, and at time 0 nothing is known and at time 1 $p$ is known. Then at time 0 neither $p$ or $\neg p$ is known

[Mario Carneiro]

This semantics generalizes nicely to modal logic as well, where $\Box A$ means A is known now and henceforth in the future

[Kenny Lau]

$\square$ \square

[Scott Olson]

My intuition regarding ¬(p ∧ q) → ¬p ∨ ¬q is that, as my assumption, I know "p and q aren't both true", but I don't know which one is false, and the conclusion requires me to pick one of the two and prove it's false, which I cannot do

[Kenny Lau]

ah, is that the program interpretation

[Scott Olson]

yeah, interpreting ∧ as a pair type and ∨ as a sum type

[Kenny Lau]

I think the corresponding model is where at time 0 nothing is known, at time 1a we know q, and at time 1b we know p.

[Mario Carneiro]

The kripke model for this one has three points, with time 0 where nothing is known and a branching future. In world 1, p is known, and in world 2 q is known. Then since $p\land q$ is true in no world, $\neg(p\land q)$ is true in every world, but neither $\neg p$ nor $\neg q$ is true in world 0

[Kenny Lau]

:)

[Scott Olson]

Interesting, I've never heard of that stuff but it lines up really well with what I did in my head

[Kenny Lau]

I think you can consider the more general ((p ∧ q) → r) → (p → r) ∨ (q → r) and use the same model

[Mario Carneiro]

yes

[Kenny Lau]

cool

[Mario Carneiro]

There is no single finite model complete for intuitionistic logic though, or equivalently there is an infinite family of truth values over one proposition

[Kenny Lau]

or maybe "truth values" just don't make sense

[Scott Olson]

h : (p ∧ q) → false
⊢ (p → false) ∨ (q → false)

(expanding the \not to the function to false)

I can either assume p or assume q (the two worlds) and then prove false, but I can't apply the function h with just one of them

[Mario Carneiro]

https://upload.wikimedia.org/wikipedia/commons/5/5c/Rieger-Nishimura.svg

[Kenny Lau]

what is thsi

[Reid Barton]

I saw this image for the first time like three days ago and I was very confused about how I had never seen it before

[Mario Carneiro]

it is the lattice of propositions over one variable

[Mario Carneiro]

up to equivalence

[Mario Carneiro]

in classical logic it is much less interesting, $\bot < p,\neg p < \top$

[Kenny Lau]

interesting

[Kenny Lau]

the program interpretation is to let p to mean X contains 1 and q to mean X contains no 1 where X is an arbitrary (computable) binary sequence, right?

[Mario Carneiro]

that's one way to do it

[Mario Carneiro]

But if you like the program (aka BHK) formulation of intuitionistic semantics, then you might like the computational interpretation of peirce's law as call with continuation

[Kenny Lau]

I never understood what call/cc means

[Mario Carneiro]

The type is callcc : ((p -> q) -> p) -> p. Suppose we are building something of type N, say, and in the course of it we want to do double negation elimination on some proposition p, like say "this TM halts". Then that means we are going to do something with this value of type p, so that's a function p -> N, and so callcc steals this "continuation" and passes it to the enclosed function of type (p -> N) -> p

[Mario Carneiro]

For example, consider the following implementation of em:

constant callcc {p q : Type} : ((p -> q) -> p) -> p

def em (p : Type) : p ⊕ (p → empty) :=
@callcc _ empty $ λ H,
show p ⊕ (p → empty), from sum.inr $ λ hp, H $
show p ⊕ (p → empty), from sum.inl hp

This function looks like magic when you see it for the first time. It's a computational interpretation of EM! So we can just put in our favorite nondecidable proposition to this oracle, like the Riemann hypothesis, and find out the answer. It calls callcc at this point, which remembers our position in the code, and then calls the sum.inr constructor. So the oracle says: RH is false! We are happy until we find out maybe that RH is actually true, and in justified anger return to our function to prove a contradiction. When we call the function though, it calls H with sum.inl hp. What happened? The function H remembers when we called callcc the first time, and "rewinds time" with our proof of RH in hand. So the oracle says: RH is true! and it stole our proof.

[Kenny Lau]

our favorite nondecidable proposition to this oracle, like the Riemann hypothesis

hmm...

[Mario Carneiro]

I guess this is like "innocent until proven guilty", we have "false until proven true"

[Kenny Lau]

I still don't understand what it does... thanks for your lengthy explanation though

[Mario Carneiro]

The semantics is a bit tricky to explain without a notion of "continuation"

[Mario Carneiro]

the idea is that every expression exists in a context, where you are evaluating an expression in order to pass it to something else

[Mario Carneiro]

and this something else can be thought of as a function from the type of the expr to the "final output"

[Mario Carneiro]

which can be whatever, it doesn't really matter

[Mario Carneiro]

it's like an expression with a hole in it where our expr goes

[Mario Carneiro]

and callcc saves this expr-with-hole that surrounds the callcc f expression itself, and calls f on it

[Mario Carneiro]

This enables bizarre behavior like returning twice from a function or functions that call each other as coroutines, or exception handling

[Mario Carneiro]

lots of control flow can be expressed using continuations

[Kenny Lau]

what kind of thing is call/cc?

[Kenny Lau]

is it a function that we can implement? is it a function that only exists in some alternate programming language?

[Mario Carneiro]

it isn't a function you can implement in lean, but it is a function that could conceivably be supported in the VM as a primitive

[Kenny Lau]

Could you write your RH thing in say Scheme?

[Mario Carneiro]

yes

[Mario Carneiro]

I think they are the pioneers of callcc

[Kenny Lau]

then what would it return?

[Mario Carneiro]

like I said, "false" until you prove it wrong

[Mario Carneiro]

and then it goes back in time with your proof and says "true"

[Kenny Lau]

do you have actual Scheme code?

[Mario Carneiro]

no, but you should just be able to use callcc in a term like I've shown

[Mario Carneiro]

the lean code should translate without issue to scheme

[Mario Carneiro]

there is also the matter of scheme not being a typed language

[Mario Carneiro]

if the time travel is the part that is surprising, a more pedestrian explanation is that it just saves the current state of the VM - the call stack and values of the variables, then we can later "reset" to this execution state

[Kenny Lau]

how does the program "take" our proof?

[Mario Carneiro]

you pass it to the function in an attempt to derive false

[Mario Carneiro]

and rather than producing a proof of false, it abandons the entire execution of the rest of the program and resets with this proof in hand

[Kenny Lau]

does callcc have any equational lemmas?

[Mario Carneiro]

yes, but they are a bit weird because they depend on the execution context

[Mario Carneiro]

You have to set up the idea of a dynamic semantics. Let's say we want to evaluate e1 + e2, we can write this as e1 + e2 < Kwhere K is the call stack. It is expecting a value of type nat say, here. So we first evaluate e1, that is, e1 < _ + e2, K where we have pushed _ + e2 on the stack. We get to a value v > _ + e2, K (the arrow is reversed to indicate that the value is done computing) which steps to e2 < v + _, K. That is we are evaluating e2 now. This finishes to v2 > v + _, K which steps to v' > K where v' is the actual result of adding numbers v and v2

[Kenny Lau]

I don't understand how you can pass the proof to the function

[Kenny Lau]

the function doesn't accept things of type p right

[Kenny Lau]

it wants a thing of type (p -> q) -> p

[Mario Carneiro]

In the em example I define a particular function of type (p -> false) -> p

[Mario Carneiro]

or rather (p + not p -> false) -> p + not p

[Mario Carneiro]

so when the callcc is called it evaluates this function giving it a kind of magic function which has type p + not p -> false

[Mario Carneiro]

this function should not ever be called, because it "destroys the universe" rather than producing a proof of false

[Mario Carneiro]

Here's another example. If f : (N -> false) -> N is the constant function 42, then callcc f just returns 42. Nothing special happens as long as f never uses its argument

[Mario Carneiro]

But if f = \lam g, false.elim (g 12), then callcc f returns 12

[Kenny Lau]

how?

[Kenny Lau]

and if f = \lam g, false.elim (g 12) + false.elim (g 13)?

[Mario Carneiro]

returns 12

[Mario Carneiro]

the rest of the computation is abandoned once g is called

[Kenny Lau]

hmm...

[Mario Carneiro]

The function g given to f is actually the expr-with-hole that callcc f is situated in

[Mario Carneiro]

it might make more sense if g is called throw instead

[Mario Carneiro]

and callcc is catch