## Stream: general

### Topic: De Morgan's

#### Ken Lee (Oct 22 2018 at 22:10):

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 (Oct 22 2018 at 22:11):

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 (Oct 22 2018 at 22:12):

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

#### Kenny Lau (Oct 22 2018 at 22:12):

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

#### Ken Lee (Oct 22 2018 at 22:13):

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

Thanks!

#### Jean Lo (Oct 22 2018 at 22:40):

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

#### Chris Hughes (Oct 22 2018 at 22:43):

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 (Oct 22 2018 at 22:45):

but that is not necessary.

#### Kenny Lau (Oct 22 2018 at 22:46):

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

#### Mario Carneiro (Oct 22 2018 at 22:51):

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

#### Kenny Lau (Oct 22 2018 at 22:52):

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

#### Mario Carneiro (Oct 22 2018 at 22:53):

yes, so it is decidable

#### Kevin Buzzard (Oct 22 2018 at 22:53):

@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 (Oct 22 2018 at 22:54):

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

#### Kenny Lau (Oct 22 2018 at 22:54):

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

#### Mario Carneiro (Oct 22 2018 at 22:54):

It's not complete, unfortunately

#### Mario Carneiro (Oct 22 2018 at 22:54):

at least not unless you consider all topologies

#### Kevin Buzzard (Oct 22 2018 at 22:55):

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 (Oct 22 2018 at 22:55):

just consider the Kuratowski algebra?

#### Mario Carneiro (Oct 22 2018 at 22:57):

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 (Oct 22 2018 at 22:58):

I don't think Kevin cares

#### Mario Carneiro (Oct 22 2018 at 22:58):

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 (Oct 22 2018 at 23:01):

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

#### Kenny Lau (Oct 22 2018 at 23:02):

$\square$ \square

#### Scott Olson (Oct 22 2018 at 23:02):

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 (Oct 22 2018 at 23:03):

ah, is that the program interpretation

#### Scott Olson (Oct 22 2018 at 23:05):

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

#### Kenny Lau (Oct 22 2018 at 23:05):

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 (Oct 22 2018 at 23:06):

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

:)

#### Scott Olson (Oct 22 2018 at 23:07):

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

#### Kenny Lau (Oct 22 2018 at 23:07):

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

yes

cool

#### Mario Carneiro (Oct 22 2018 at 23:08):

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 (Oct 22 2018 at 23:08):

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

#### Scott Olson (Oct 22 2018 at 23:08):

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

what is thsi

#### Reid Barton (Oct 22 2018 at 23:09):

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 (Oct 22 2018 at 23:09):

it is the lattice of propositions over one variable

#### Mario Carneiro (Oct 22 2018 at 23:09):

up to equivalence

#### Mario Carneiro (Oct 22 2018 at 23:10):

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

interesting

#### Kenny Lau (Oct 22 2018 at 23:11):

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 (Oct 22 2018 at 23:12):

that's one way to do it

#### Mario Carneiro (Oct 22 2018 at 23:14):

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 (Oct 22 2018 at 23:14):

I never understood what call/cc means

#### Mario Carneiro (Oct 22 2018 at 23:18):

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 (Oct 22 2018 at 23:34):

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 (Oct 22 2018 at 23:39):

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

hmm...

#### Mario Carneiro (Oct 22 2018 at 23:41):

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

#### Kenny Lau (Oct 22 2018 at 23:41):

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

#### Mario Carneiro (Oct 22 2018 at 23:41):

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

#### Mario Carneiro (Oct 22 2018 at 23:42):

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 (Oct 22 2018 at 23:42):

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

#### Mario Carneiro (Oct 22 2018 at 23:42):

which can be whatever, it doesn't really matter

#### Mario Carneiro (Oct 22 2018 at 23:43):

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

#### Mario Carneiro (Oct 22 2018 at 23:43):

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

#### Mario Carneiro (Oct 22 2018 at 23:45):

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

#### Mario Carneiro (Oct 22 2018 at 23:45):

lots of control flow can be expressed using continuations

#### Kenny Lau (Oct 22 2018 at 23:47):

what kind of thing is call/cc?

#### Kenny Lau (Oct 22 2018 at 23:47):

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

#### Mario Carneiro (Oct 23 2018 at 00:21):

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 (Oct 23 2018 at 06:19):

Could you write your RH thing in say Scheme?

yes

#### Mario Carneiro (Oct 23 2018 at 06:24):

I think they are the pioneers of callcc

#### Kenny Lau (Oct 23 2018 at 06:26):

then what would it return?

#### Mario Carneiro (Oct 23 2018 at 06:27):

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

#### Mario Carneiro (Oct 23 2018 at 06:27):

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

#### Kenny Lau (Oct 23 2018 at 06:28):

do you have actual Scheme code?

#### Mario Carneiro (Oct 23 2018 at 06:28):

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

#### Mario Carneiro (Oct 23 2018 at 06:29):

the lean code should translate without issue to scheme

#### Mario Carneiro (Oct 23 2018 at 06:30):

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

#### Mario Carneiro (Oct 23 2018 at 06:34):

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 (Oct 23 2018 at 06:35):

how does the program "take" our proof?

#### Mario Carneiro (Oct 23 2018 at 06:35):

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

#### Mario Carneiro (Oct 23 2018 at 06:36):

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 (Oct 23 2018 at 06:37):

does callcc have any equational lemmas?

#### Mario Carneiro (Oct 23 2018 at 06:37):

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

#### Mario Carneiro (Oct 23 2018 at 06:42):

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 (Oct 23 2018 at 06:42):

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

#### Kenny Lau (Oct 23 2018 at 06:42):

the function doesn't accept things of type p right

#### Kenny Lau (Oct 23 2018 at 06:42):

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

#### Mario Carneiro (Oct 23 2018 at 06:43):

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

#### Mario Carneiro (Oct 23 2018 at 06:43):

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

#### Mario Carneiro (Oct 23 2018 at 06:44):

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 (Oct 23 2018 at 06:46):

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

#### Mario Carneiro (Oct 23 2018 at 06:50):

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 (Oct 23 2018 at 06:51):

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

how?

#### Kenny Lau (Oct 23 2018 at 06:52):

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

returns 12

#### Mario Carneiro (Oct 23 2018 at 06:53):

the rest of the computation is abandoned once g is called

hmm...

#### Mario Carneiro (Oct 23 2018 at 06:53):

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

#### Mario Carneiro (Oct 23 2018 at 06:55):

it might make more sense if g is called throw instead

#### Mario Carneiro (Oct 23 2018 at 06:55):

and callcc is catch

Last updated: May 06 2021 at 22:13 UTC